completed

MLabs - Spec DSL for dApp Security

$72,000.00 Received
$72,000.00 Requested
Ideascale logo View on ideascale
Community Review Results (1 reviewers)
Addresses Challenge
Feasibility
Auditability
ソリューション

We are building a spec language for formally describing dApp behavior and generating tests to validate an implementation against its design.

Problem:

Cardano was designed to support secure smart contracts. Yet, testing, auditing, and even designing Cardano dApps involve serious challenges.

Yes Votes:
₳ 120,881,105
No Votes:
₳ 4,396,242
Votes Cast:
390

チーム

This proposal was approved and funded by the Cardano Community via Project F8: Open Source Development Ecosystem Catalyst funding round.

[IMPACT]

Market

Cardano dApp developers building mission-critical applications such as DeFi protocols.

Problem Space

Numerous dApps began building on Cardano following the introduction of the Plutus smart contract programming language. This is hardly surprising given the rich features offered by the blockchain’s EUTXO ledger and Ouroboros consensus mechanism: atomic transactions, predictable fees, and the potential to mathematically verify a smart contract's design.

These aspects are a natural extension of Cardano’s design which borrows heavily from formal methods. This architecture lends itself to functional programming, which can be noted in Plutus, a smart contract DSL built on Haskell.

These features of Cardano make it suitable for supporting mission-critical applications, such as DeFi dApps securing millions of dollars of value. Yet, this same unique design also presents key challenges to developers. Testing, auditing, and even designing Cardano smart contracts remains challenging, and tools are needed to simplify the process.

A specification language for sound dApp design

Smart contracts within Cardano consist of scripts that control how UTXOs, pieces of value with an associated piece of data (the datum), can be consumed by transactions. Unlike the global nature of smart contracts on Ethereum, a Cardano script can only perform a local inspection of the consuming transaction. This means that the implementation of a contract (i.e., the script) is often divorced from the desired semantics of its operation.

Moreover, it is generally non-trivial to decipher the intention of a smart contract from its raw implementation. This has reaching consequences for a smart contract blockchain like Cardano. Here, all smart contract code is public and endpoints can be evoked by anyone, at any time, to irrevocably change the state of the ledger. This open nature inadvertently creates massive incentives to exploit poorly designed applications.

Our goal is to create a specification language, an embedded DSL, in which we can describe the semantics of a dApp system in its entirety, from an inter-transaction perspective rather than an intra-transaction perspective. More concretely, our specification language consists of a way of specifying transactions (e.g., changes to the state of the ledger) and combinations of transactions as well as the conditions under which they should validate. In general, this involves delineating subsets of transaction types (transaction families) as well as defining the way tokens can flow between UTXOs and the sequence of events upon which their transfer is predicated.

How does formal specification help Cardano?

A major selling point of Cardano is that its core language and smart contract language are amenable to formal verification. This means smart contracts can be, more or less, mathematically proven to be secure. As noted in the Cardano documentation, “specification derived from white papers looks a lot like Haskell code, and connecting the two is considerably easier than doing so with an imperative language.”

It is also useful to recall Cardano's multi-asset ledger lends itself to a wide range of use cases for tokens in comparison to single-asset ledgers such as Ethereum. Developers will be able to use our specification to delineate the properties and legal state transitions that govern their applications.

Such a specification can then be translated to program code which can be tested to behave as intended per the properties encoded using our specification language. For properly designed smart contracts, users will have a high degree of assurance that the dApps they interact with behave as intended and are unable to enter undesirable states where value may be inadvertently lost.

Just as important, however, our DSL will streamline dApp designs and generate tests to ensure an implementation functions as intended. This will dramatically reduce auditor and developer time while significantly reducing costs.

Plutus and the Cardano blockchain obviously support a wide variety of use cases. This is readily seen in the current dApp ecosystem. Because of this, we expect some difficulties designing a DSL that sufficiently covers this wide scope of use cases and incorporates 'edge-case' protocol designs. We expect that improvements will be ongoing.

[FEASIBILITY]

Our Proposal

We aim to deliver a DSL to expedite the specification of a system and the definition of an application’s axiomatic semantics. Developers will be able to incorporate our DSL throughout the development process. More specifically, our DSL will provide dApp developers building on Cardano with a high-level and cost-effective way of ensuring dApp implementations match their designs.

Developers will be able to use our specification language to:

• cut costs by reducing auditor and developer time

• build dApps that interoperate securely with others, a prerequisite of a vibrant DeFi ecosystem

• configure the value types their smart contracts can handle

• test assertions based on pre and postconditions

• employ automated or human-directed proofs of application function

• define the types of transactions (transaction families) a system can handle

• automate code generation in some cases

• design applications that cannot enter unsound states

• expedite the design of a system’s architecture

• have greater confidence in testing

Funding:

Engineering hours: 900

Total: $72,000

Breakdown:

Feature……………………………………………………………………………………………………………Total Time

Initial Exploration, Notation, and Analysis of Problem Domain……………………………60

Classification and Automated Delineation of Tx Families…………………………………..120

Design of Syntax and Generalized Type Systems……………………………………………..120

Integration / Implementation into Current dApp Ecosystem………………………………80

Optimization (e.g. Fine-tuning Data Structure Traversals)…………………………………80

Documentation and Training Materials……………………………………………………………..40

General Testing……………………………………………………………………………………………….80

Audit Prep……………………………………………………………………………………………………….80

Spec……………………………………………………………………………………………………………….80

Subtotal………………………………………………………………………………………………………….740

Change Budget……………………………………………………………………………………………….160

Total Time………………………………………………………………………………………………………900 hours

Total Cost………………………………………………………………………………………………………$72,000

MLabs: MLabs has quickly become one of the premier development firms in the Cardano Ecosystem. We are an IOG Plutus Partner and work regularly with IOG to develop the Cardano blockchain and ecosystem. We employ over 80 developers and have helped build community projects such as:

• Liqwid

• SundaeSwap

• Ardana

• CardStarter

• Optim

• Many others

Through our work with early-stage projects, we have one of the largest groups of Haskell / Plutus developers in the community. Developers working on our specification language will bring their collective experience to the project and ensure a successful launch.

Website: <https://mlabs.city/>

Core Team

Compilers and Formal Methods

Las Safin

Las is a software engineer and formal methods specialist who is experienced with dependently typed languages such as Idris and Agda and who is interested in Cedille. At MLabs, he helps manage Nix environments for use in development and writes application specifications as well as compilers.

Las has also made significant contributions to Cardano tooling. Most notably, he is the creator of Plutarch. Plutarch is a typed eDSL in Haskell for writing efficient Plutus Core validators. Plutarch significantly lowers the resource demands of validators written in the eDSL while providing developers more fine-grained control of the Plutus Core generated. See the GitHub link for more information.

Plutarch: <https://github.com/Plutonomicon/plutarch>

GitHub: <https://github.com/L-as>

Ecosystem and Formal Methods

Maksymilian Brodowicz

Maksymilian does a lot of research, both technical and product-wise, financial and user-experience related. Specifying and creating innovations in protocols, his designs have been used in a variety of efforts.

By education a Mathematician and a Computer Scientist, HoTT enthusiast, and five-year Haskell practitioner.

<https://github.com/zygomeb>

Delivery Manager

George Flerovsky

George manages a portfolio of projects at MLabs including decentralized exchanges, governance, auctions, yield optimization, and on-chain analytics. He completed his Master of Arts degree in Economics in 2017 and has five years of professional experience in data science and engineering. Before joining MLabs, George was involved with designing the streaming merge algorithm for concurrency in the Cardax decentralized exchange.

George has developed in and loved Haskell since 2015, and has been involved with Cardano since 2018. He has carefully studied the Cardano research papers and specifications, developing a deep knowledge of the Cardano consensus protocol, smart contract framework, and network stack. He participated in the first cohort of the Plutus Pioneers Program in summer 2021, and actively contributed to the Alonzo Blue, White, and Purple testnets.

GitHub: <https://github.com/GeorgeFlerovsky>

Formal Methods

Maciej Bendkowski

Maciej completed his Ph.D. in 2017 in the Theoretical Computer Science group at the Jagiellonian University in Kraków, Poland. His research interests include lambda calculus, formal verification, and random generation of large combinatorial structures. He is an author or co-author of 15 peer-reviewed research papers in theoretical computer science and combinatorics. Throughout his career, Maciej focuses on finding practical applications to his theoretical findings. His recent projects include a Haskell-based combinatorial sampler compiler implementing the idea of multiparametric Boltzmann samplers.

GitHub: <https://github.com/maciej-bendkowski>

Compilers and Formal Methods

Fraser Dunlop

Fraser is a software engineer experienced in Haskell development and compiler design for constraint modeling languages. At MLabs he has developed specification tools for generating property test suites from formal specifications.

apropos: <https://github.com/MLabs/apropos>

Github: <https://github.com/delicious-lemon>

Formal Methods

Peter Dragos:

Peter holds an undergraduate degree in Mathematics from the University of Rochester. His professional interests include applied category theory, foundational mathematics, and modeling of political and economic systems.

<https://github.com/peter-mlabs>

[AUDITABILITY]

Auditability

-Commits to our open-source GitHub repo

-Testing and benchmark suite

-Documentation and ease of use

-Number of projects incorporating our DSL

Definition of Success After 3, 6, and 12 Months (Milestones)

3 Months: Finish the initial exploratory phase of development and realize a functional specification language usable by advanced users.

6 Months: Checking against production EUTXO scripts and expanding the number of use cases covered by our DSL. We expect to have backtested many working dApps throughout development and have several early-stage dApps designing with and incorporating our product throughout their development process.

12 Months: A fully functional, audited, and flexible DSL suitable for specifying any project type. At the 12-month mark, we anticipate the majority of our attention will be focused on exploring "edge-cases" and filling out the scope of design types supported by our DSL.

This is a new proposal.

コミュニティ・アドバイザー・レビュー (1)

Comments

Monthly Reports

This is our first report - We are currently putting together our team of developers and dealing with any legal issues that need to be taken care of.

Disbursed to Date
$72,000
Status
Still in progress
Completion Target
2/1/2023
Comments 0

Login or Register to leave a comment!

no

Disbursed to Date
$72,000
Status
Still in progress
Completion Target
5/1/2023
Attachment(s)
Comments 0

Login or Register to leave a comment!

no thank you

Disbursed to Date
$72,000
Status
Still in progress
Completion Target
4. After 6 months
Attachment(s)
Comments 0

Login or Register to leave a comment!

We are close do finishing

Disbursed to Date
$72,000
Status
Still in progress
Completion Target
2. In the next 3 months
Comments 0

Login or Register to leave a comment!

PSL development last month focused on improving usability - particularly, diagram support. Bugs in diagram generation were resolved and formatting was improved. Transactions were also given the ability to provide greater clarity (e.g., displaying lists of relevant UTxOs).

Along these lines, improvements were made to the documentation and the project's approachability. By this, we mean the repo was marginally reconfigured for ease of use and streamlining new project onboarding.

Of note, the PSL has been used to largely spec a client project with the intention of building out the language to cover the project in its entirety. With this underway, the PSL team is currently deliberating on integrating with a second project. Once decided, work with a second project will be used to generalize the PSL - a major goal outlined in the original Catalyst proposal.

Disbursed to Date
$72,000
Status
Still in progress
Completion Target
3. In the next 6 months
Comments 0

Login or Register to leave a comment!

Work continued over the last month with generalizing the PSL. Towards this end, the formal methods team began work specifying a second DApp, Seabug. Seabug is an internal MLabs project that produces cNFT derivatives with enhanced ownership values. The minting derivative minting scheme of the protocol is somewhat complex, making it a good second use case for the PSL. Details on the Seabug minting scheme can be found here: https://drive.google.com/file/d/1F7a0lOWKJhEuYZxcK90qN2UN1rVePXRX/view

The formal methods team was able to specify the complicated transactions of Seabug, providing a greater degree of confidence in the eDSL approach of the PSL and its usefulness for other Cardano DApps, especially when combined with other formal methods tools. Naturally, with transactions specified transaction diagrams were straightforward to generate - a major secondary use case of the project.

Finally, a number of maintenance commits occurred over the last month. These include fixing and updating library dependencies, updating tags, and so on. Finally, some diagramming errors concerning edge-case were addressed and largely resolved.

Disbursed to Date
$72,000
Status
Still in progress
Completion Target
3. In the next 6 months
Attachment(s)
Comments 0

Login or Register to leave a comment!

As mentioned in our August and July monthly updates, our Plutus Specification Language incorporates Plutarch and is increasingly integrating this eDSL's type scheme and codebase over time. Towards this end, a significant portion of PSL work involved updating Plutarch to reflect Plutus changes and to make the Nix build more reliable.

That said, other type adjustments were made to Plutarch that support use cases addressed by our Specification Language. For instance:

  • fixing V1 script types being re-exported in the V2 API
  • correcting the pif operator
  • support for generating type class instances
  • syntactical plugin to improve ergonomics
Disbursed to Date
$72,000
Status
Still in progress
Completion Target
2. In the next 3 months
Comments 0

Login or Register to leave a comment!

close

Playlist

  • EP2: epoch_length

    Authored by: Darlington Kofa

    3分 24秒
    Darlington Kofa
  • EP1: 'd' parameter

    Authored by: Darlington Kofa

    4分 3秒
    Darlington Kofa
  • EP3: key_deposit

    Authored by: Darlington Kofa

    3分 48秒
    Darlington Kofa
  • EP4: epoch_no

    Authored by: Darlington Kofa

    2分 16秒
    Darlington Kofa
  • EP5: max_block_size

    Authored by: Darlington Kofa

    3分 14秒
    Darlington Kofa
  • EP6: pool_deposit

    Authored by: Darlington Kofa

    3分 19秒
    Darlington Kofa
  • EP7: max_tx_size

    Authored by: Darlington Kofa

    4分 59秒
    Darlington Kofa
0:00
/
~0:00