Please describe your proposed solution

The smart contract system of Cardano was designed with formal verification in mind. Its architecture and programming language paradigm were deliberately chosen for their compatibility with formal verification. In the original whitepaper for Plutus, the ability to easily apply formal methods to reason about the behavior of UPLC smart contracts was one of the most critical features of the smart contract system and one of the main advantages it has over other smart contract platforms.

Formal methods can be applied to mathematically prove the correctness and security of smart contract protocols with respect to their formal specification. Formal methods can also be applied to Cardano smart contract protocols (DApps) to prove that the protocols posses certain security properties that are extremely important from the perspective of users. For instance, a property that would be interesting to users of a DEX would be that their funds cannot be stolen or locked even by permissioned agents of the platform.

In theory all of this is great! All the DApps on Cardano must be extremely secure relative to those on other networks because they are all employing formal methods right? Unfortunately, in-practice because there is no open-source framework to facilitate this, the vast majority of DApps on Cardano do not leverage formal methods at all. A few auditing firms in the ecosystem offer formal verification services; however, they come at a premium compared to their regular auditing services and they use closed-source proof frameworks. As a result these smart contract verification solutions are completely inaccessible to the vast majority developers on Cardano.

Our proposed framework seeks to provide smart contract developers on Cardano with the tools needed to easily define a formal specification of their smart contracts and then prove that those contracts are correct with respect to that specification.

We acknowledge that some developers might not have the capacity to define a formal specification of their smart contracts. For such cases, we seek to offer built-in support for detecting a number of protocol agnostic vulnerabilities.

There are certain common security vulnerabilities that Plutus scripts can be subject to. Our proposed formal verification framework aims to provide smart contract developers on Cardano with a tool that allows them to mathematically prove that their smart contract are secure from those common vulnerabilities. Out of the box, we aim to include support for:

1. Double Satisfaction
2. Unbounded Datum
3. Unbounded Value
4. Staking Control Theft
5. Other Token Name Minting Attack

Our proposed framework consists of two sub-frameworks. The first component, Coq-UPLC, as the name implies is designed to work directly on UPLC. The second component, Coq-Plutus, does not operate directly on any given smart contract language. Instead, it provides a Coq implementation of all the relevant Plutus types, their true representation (Data encoding), and a library of utilities for common operations with those types and proof utilities to easily prove security against the aforementioned common vulnerabilities. While with Coq-UPLC developers can work directly with the compiled UPLC, Coq-Plutus is designed to make the process of translating your smart contract (or critical components of your smart contract) into the framework as simple as possible. Once translated, you can easily leverage the power of the provided proof utilities for common vulnerabilities and if you are feeling adventurous you can venture on to introduce your own theorems with Coq's interactive theorem prover. Coq-Plutus is designed to make the process of translating your smart contract (or critical components of your smart contract) into the framework as simple as possible. Once translated, you can easily leverage the power of the provided proof utilities for common vulnerabilities and if you are feeling adventurous you can venture on to introduce your own theorems with Coq's interactive theorem prover.

Please define the positive impact your project will have on the wider Cardano community

The proposed formal verification framework for Cardano smart contracts has the potential to bring significant positive impact to the wider Cardano community. By providing developers, even those unaccustomed to formal methods, with the means to apply formal verification to their smart contracts, the framework stands to fortify the overall security and dependability of the Cardano ecosystem. This increased security will foster greater trust among users and investors, making Cardano a more attractive platform for decentralized applications and DeFi projects. Furthermore, the open-source nature of the framework and its built-in support for detecting common vulnerabilities will empower a broader range of developers, including those with limited formal verification expertise, to build secure DApps on Cardano. This democratization of formal methods tooling will lead to a more secure smart contract ecosystem, ultimately benefiting the entire Cardano community by reducing the risk of smart contract vulnerabilities.

Furthermore, Anastasia Labs plans to build additional tools to support formal veridication endevours on top of these libraries in question.

What is your capability to deliver your project with high levels of trust and accountability? How do you intend to validate if your approach is feasible?

Anastasia Labs has rapidly established itself as a leading auditing firm within the Cardano Ecosystem.

Our team consists of highly skilled developers who have made significant contributions to various community projects, including Lucid, Plutarch, and Liqwid-Plutarch-Extra. Our developers have had experience developing and publishing end-to-end DApps including production projects like WingRiders. Our auditing clients include Wanchain, Lenfi, Encoins, FluidTokens, Spectrum Finance, and Atrium. In addition to our project involvement, our team has been actively engaged in the developer experience domain. We have actively participated in educational panels focused on DApp Security Practices and Design Patterns. We specialize in Cardano smart contract auditing and security. Even outside of our auditing engagements, we have identified and resolved a number of smart contract vulnerabilities in open-source projects on Cardano including on Agora, Wanchain, and Spectrum finance (eventually leading to auditing engagements with the last two).

Furthermore, our team has experience with applied formal methods in the domain of smart contract verification.

See:

<https://drive.google.com/file/d/1lafzfhvD-R5va4YQjO-yxfwnHskgCC0a/view>

In-fact, we already have a proof of concept implementation of the Plutus CEK machine in Coq.

With broad range of expertise within the Cardano Ecosystem we are a highly capable and versatile development firm.

What are the key milestones you need to achieve in order to complete your project successfully?

Milestone 1: CEK machine

Output: Currently, we have a proof of concept implementation of the Plutus CEK machine in Coq. However, it is missing a number of features. With this, we hope to finalize the Coq implementation of the Plutus CEK machine.

Verification: All work for this proposal will be published publicly and open-sourced. The Plutus CEK machine implementation in Coq will be made available in a public GitHub repository.

Milestone 2: Introduction of non-cryptographic built-in functions

Output: There are a number of Plutus built-in functions that are currently missing from Coq-UPLC. For this milestone, we will finish adding support for all the remaining non-cryptographic Plutus built-in functions.

Verification: All work for this proposal will be published publicly and open-sourced on our GitHub.

Milestone 3: Proof tools through an example smart contract verification

Output: We will provide tools to aid in proving certain properties on serialized smart contracts. Additionally, we will provide an example use-case and tutorial to demonstrate how Coq-UPLC can be used in practice to apply formal methods to Cardano smart contracts.

Verification: All work for this proposal will be published publicly and open-sourced on our GitHub.

Milestone 4: Finalize implementation of ScriptContext types and associated BuiltinData representations in Coq-Plutus

Output: We will provide utilities to allow developers to prove certain properties on serialized smart contracts. Additionally, we will provide an example use-case and tutorial to demonstrate how Coq-UPLC can be used in practice to apply formal methods to Cardano smart contracts.

Verification: All work for this proposal will be published publicly and open-sourced on our GitHub.

Milestone 5: Common vulnerability theorem library for Coq-Plutus

Output: We will provide a library of theorems that developers can use to verify security against a number of common smart contract vulnerabilities.

Verification: All work for this proposal will be published publicly and open-sourced on our GitHub.

Final Milestone: Production use-case of Coq-Plutus and developer tutorial

Output: We will provide an example use-case and tutorial to demonstrate how developers can use Coq-Plutus in-practice to mathematically prove formalized security properties of a production smart contract. We will also publish a technical blog about the framework, its features, applications, and future roadmap.

Verification: All work for this proposal will be published publicly and open-sourced on our GitHub.

Who is in the project team and what are their roles?

Mark Petruska, formal methods, type theory, dependent types, theorem proving

Mark has years of professional experience in both Cardano smart contract development and applied formal methods engineering. This proposal is the perfect intersection of his skillset and interests.

Philip DiSarro, Compiler &amp; Programming Language Research

Philip has an MS in Compiler Development &amp; Programming Language Theory. He was the lead smart contract architect of many features on WingRiders DEX. Philip has also made significant contributions to the Cardano developer ecosystem. As a co-chair of the IOHK developer experience working group he worked to identify and resolve pain points that DApp developers experience in Cardano, and had an integral role in getting Lucid &amp; Plutus Simple Model included in the Plutus Pioneer Program. He has a vast wealth of experience in smart contract security and auditing on Cardano.

Philip is CEO and founder of Anastasia Labs and a senior Haskell developer on the XSY team, a consultant and lecturer for Emurgo.

Philip will be responsible for assisting with a number of the common vulnerability theorems and auxiliary work for Coq-Plutus.

Please provide a cost breakdown of the proposed work and resources

Formal Verification Lead - 1 individual - ADA 60K

Senior Coq developer - 2 individuals - ADA 40K each

Audit Lead - 1 individual - ADA 60K

No dependencies.

How does the cost of the project represent value for money for the Cardano ecosystem?

By investing in the development of a formal verification framework, we are proactively enhancing the security and reliability of Cardano's smart contracts. This not only safeguards the assets and interests of user, but also solidifies Cardano's position as the most secure and trustworthy platform for decentralized applications and DeFi projects. The long-term benefits of reduced security risks and increased confidence in the ecosystem far outweigh the initial investment, making it a cost-effective measure to ensure the sustainable growth and success of Cardano.