Last updated a year ago
Cardano was designed to support secure smart contracts. Yet, testing, auditing, and even designing Cardano dApps involve serious challenges.
We are building a spec language for formally describing dApp behavior and generating tests to validate an implementation against its design.
This is the total amount allocated to MLabs - Spec DSL for dApp Security.
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.
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.
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
-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.
NB: Monthly reporting was deprecated from January 2024 and replaced fully by the Milestones Program framework. Learn more here
Mathematicians with advanced degrees, logicians trained in formal proofs, experienced Haskell / Plutus developers.