-
Notifications
You must be signed in to change notification settings - Fork 8
DafnyEVM_GrantApplication_2023
In 3-5 sentences what problem are you trying to solve? (The project abstract may be used for for the winners announcement.)
The DafnyEVM is an executable formalisation of the EVM in Dafny being developed by the Trustworthy Smart Contracts team at ConsenSys, Inc. The DafnyEVM captures the EVM semantics in a relatively easy-to-digest fashion which, furthermore, is checked using the Dafny verifier. The DafnyEVM can be used to verify properties of smart contracts written at the bytecode level, and has been validated against a larger number of the Ethereum Common Tests. The purpose of this grant application is to support further development of the DafnyEVM and, in particular, to demonstrates its use a number of real-world settings.
What are you hoping to accomplish with this grant? How do you define and measure success for this project?
The aim of this project is to further develop the DafnyEVM in two directions:
-
For prototyping and checking future EIPs related to the execution layer (e.g. the upcoming EVM Object Format in EIP3540). The benefits of using the DafnyEVM here are that, by leveraging Dafny's verification system, we can catch problems that are otherwise hard to spot, or which cannot be found with existing tools.
-
For formally verification of real-world smart contracts. Verifying contracts at the bytecode level means we are operating on the actual code that will execute and, thus, compiler bugs (e.g. in Solidity) are not a concern. Since it provides a complete semantics of the EVM which has been validated against the common tests, the DafnyEVM offers a high-level of confidence. However, at this time, the DafnyEVM has only been used to verify small and artificial contracts (e.g. such as showing the absence of arithmetic overflow/underflow in this betting contract). Therefore, scaling the DafnyEVM up to real-world contracts remains an open problem.
Success will be measured in two ways: (1) by prototyping one or more upcoming EIPs using the DafnyEVM, were we able to contribute valuable insights to the discussion that, most likely, would otherwise have been missed? (2) were we able to verify a useful range of properties for a high-value contract deployed on mainnet?
How does this project benefit the greater Ethereum ecosystem?
Dafny is a state-of-the-art programming language which supports (mostly automatic) formal verification. Dafny is an open source project which is developed primarily at Amazon Web Services. Dafny represents a new class of tool that could offer significant benefits for the Ethereum ecosystem. For example, Dafny was previously used by members of our team to formalise the Eth 2.0 specification and has been used by others to verify the QBFT consensus protocol.
In many ways, the purpose of this project is to further explore how Dafny can be used to help developments at the execution layer. Whilst our team has already begun investigations in this direction, there remain many open questions. In particular, the question remains: can Dafny be utilised to provide meaninful value at the execution layer? In developing the DafnyEVM, we hope to answer this question for the Ethereum community.
What are you going to research? What is the expected output?
The move towards the EVM Object Format began in the London fork with EIP3541 and will continue in Cancun with EIP3540. This process represents a significant and challenging upgrade to the execution layer. As such, it offers an opportunity for the DafnyEVM to showcase itself as a valuable asset for ensuring such upgrades go smoothly.
The initial version of EOF (v1.0) constitutes four additional EIPs: EIP3670 for Code Validation; EIP4200 for Static relative jumps; EIP4750 for Functions; and EIP5450 for Stack Validation. Each of these EIPs includes a reference implementation which, in some cases, is reasonably involved (e.g. code validation in EIP4200). By prototyping these EIPs in the DafnyEVM, we can bring Dafny to bear on the problem of ensuring they are consistent and do not contain hidden problems.
The DafnyEVM can be used to verify security properties over arbitrary sequences of bytecodes. For example, using the DafnyEVM we can formally verify at compile time that the following assertion is always true:
method AddBytes(x: u8, y: u8) {
// Initialise an EVM.
var st := InitEmpty(gas:=1000);
// Execute three bytecodes
st := Push1(x);
st := Push1(y);
st := Add();
// Check top of stack is sum of x and y
assert st.Peek(0) == (x as u256) + (y as u256);
}This is a simple proof that adding two bytes in the EVM never causes an arithmetic overflow, no matter what values for x and y are chosen. Note, however, that if x and y had type u256 then Dafny would flag the potential arithmetic overflow for us at compile time. For a longer and more interesting example, see our short article introducing the DafnyEVM.
Formal verifying properties over relatively short bytecode sequences is straightforward with the DafnyEVM. However, a key challenge lies in scaling up to much larger and more realistic contracts. In particular, Dafny will timeout when verifying long uninterrupted bytecode sequences. To that end, we have been experimenting with a proof generation process that breaks the contract's bytecode up into many small chunks (roughly similar to the size of a basic block). This utilises a simple disassembler for the EVM bytecode, upon which a static analysis is conducted to extract key information (e.g. stack heights, return addresses, the current position of the free memory pointer, etc). Using this we were able to verify a simple betting contract written in Solidity was free from arithmetic overflow and underflow. You can see the complete proof object here.
Whilst we have demonstrated the DafnyEVM can be used to verify more realistic contracts, there remains much to be done before it could be routinely utilised for smart contract verification. In particular, our demonstration required manual adjustments to the proof object generated from the bytecode which were non-trivial and required considerable expertise. Furthermore we only consider one security property, namely arithmetic overflow. There are many other properties that need to be considered before such a tool could be used in a realistic setting.
How many people are working on this project? Please list their names and roles for the project as well as how many hours per month will each person work on this project?
There are four people working on this project:
- David J. Pearce (ConsenSys, Inc). David holds a PhD from Imperial College London, and was previously an Associate Professor at Victoria University of Wellington [Google Scholar][LinkedIn][Twitter][Homepage]. David will act as principal investigator, and expects to work 10hrs per week on the project.
- Franck Cassez (ConsenSys, Inc). Franck holds a PhD from École Centrale de Nantes, and was previously an Associate Professor at Macquarie University [Google Scholar][LinkedIn][Twitter][Homepage]. Franck will act as a key researcher, and expects to work 10hrs per week on the project.
- Horacio M. A. Quiles (ConsenSys, Inc). Horacio holds an MSc from Universidad Politécnica de Valencia, and was previously a Senior Software Engineer at Runtime Verification, Inc [LinkedIn]. Horacio will act as a key researcher, and expects to work 10hrs per week on the project.
- Joanne Fuller (ConsenSys, Inc). Joanne holds a PhD from Queensland University of Technology (QUT), and was previously a lecturer at QUT [Google Scholar][LinkedIn]. Joanne will act as a supplementary researcher and expects to work 5hrs per week on the project.
Give us a bit of info and include relevant links, if available! Please provide other projects or research papers (ideally public and/or open source), engagements or other types of proof that your team has the necessary experience to undertake the project you are applying for. Any links for us to review? E.g. research papers, blog posts, etc.
How do you plan to achieve your research objectives?
Please include a brief explanation on the milestones/roadmap, along with expected deliverables. Also outline how the funds will be used for the research project and or members of the team.
Throughout the project, we expect team members to be following the discussions around the EOF and, for example, attending implementer calls, etc.
- Shanghai Upgrade. The starting point for the project will be to update the DafnyEVM for the Shanghai fork (once this has occurred). At this stage, we expect the following EIPs are relevant: EIP3651 (Warm COINBASE); EIP3855 (PUSH0 instruction); EIP3860 Limit and meter initcode. These are relatively straightforward changes, and we don't anticipate significant difficulties.
- EIP3450 (EOFv1). The starting point for implementing EOF within the DafnyEVM is to support the high-level container format, type sections, validation rules, etc. This includes validating against the relevant Ethereum common tests.
- EIP4200 (Static Relative Jumps). This represents a relatively self-contained update to the handling of control flow within the EVM, and should provide a useful test for the DafnyEVM.
- EIP4750 (Functions). This is a more involved update which alters the internal representation of the EVM state by adding a new return stack alongside the operand stack. We anticipate challenges supporting this EIP whilst retaining backwards compatibility with legacy contracts.
- Finalisation. At this stage, we aim to wrap up the remaining EIPs (EIP3670 for Code Validation (EOF) and EIP5450 for Stack Validation).
Requested grant amount and how this will be used. Please provide an requested amount and outline of how the grant will be used. A detailed budget proposal would be helpful and some item you could include are: Principle Researchers Costs; Other Staff Costs; Hardware Costs; Software Costs; Data Collection Costs; Indirect Costs
The amount requested is US$132K, and the breakdown is as follows:
-
(Principle Researcher Costs) Our budget is for a total of six person months at US$22K per month (
6 x 22K = 132K). This contributes torwards the costs of team members at their respective institutions.
Given the nature of the project, we do not anticipate any other significant costs (e.g. for hardware or software).