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:
- Double Satisfaction
- Unbounded Datum
- Unbounded Value
- Staking Control Theft
- 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.