MLabs - Spec DSL for dApp Security

[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.