DafnyEVM_GrantApplication_2023

Project Abstract

In 3-5 sentences what problem are you trying to solve? (The project abstract may be used for for the winners announcement.)

The Trustworthy Smart Contracts (TSC) Team at ConsenSys have developed a formal and executable semantics of the EVM in Dafny: the DafnyEVM. 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 formally verify properties of smart contracts written at the bytecode level. We have validated our formalisation against a larger number of the Ethereum Common Tests and demonstrated that the DafnyEVM provides a robust framework to reason about bytecode.

The purpose of this grant application is to support further development of the DafnyEVM and, in particular, to leverage the power of deductive verification for EVM bytecode.

Objectives

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 extend the DafnyEVM in two directions:

1. 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 subtle errors that may not be uncovered by other techniques like testing. Moreover, we can propose and validate fixes to these problems.

2. Formal verification of real-world smart contracts. Verifying contracts at the bytecode level means we are operating on the actual code that will execute. In this approach, we do not have to trust the compiler (e.g. from Solidity to EVM). 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 and broad applicability. However, at this time, the DafnyEVM has only been used to verify short code snippets or small 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?

Outcomes

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: can Dafny be utilised to provide meaningful value at the execution layer? In developing the DafnyEVM, we hope to answer this question for the Ethereum community.

Grant Scope

What are you going to research? What is the expected output?

EVM Object Format

The move towards the EVM Object Format (EOF) 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 unexpected errors.

Smart Contract Verification.

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 with 1000 gas.
  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);
}

The assert is a verification statement and the Dafny verifier checks it always holds at a given program control location. If this program verifies,
it is a formal and machine-checkable 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 not be able to prove correctness and 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.

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

Project Team

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 researchers working on this project:

1. David J. Pearce (ConsenSys). 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 lead researcher, and expects to work 10hrs per week on the project.
2. Franck Cassez (ConsenSys). 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 principle researcher, and expects to work 10hrs per week on the project.
3. Horacio M. A. Quiles (ConsenSys). 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 principle researcher, and expects to work 10hrs per week on the project.
4. Joanne Fuller (ConsenSys). 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.

Background

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.

The TSC team has a long-standing track record in the formal verification of Ethereum Consensus and and Execution layers:

• we have conducted a formal analysis of the the Eth 2.0 specification and published our results in TACAS'22 (Tools and Algorithms for the Construction and Analysis of Systems), a flagship conference in formal verification: Cassez, F., Fuller, J., Asgaonkar, A. (2022). Formal Verification of the Ethereum 2.0 Beacon Chain. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13243. Springer, Cham. https://doi.org/10.1007/978-3-030-99524-9_9. We have presented our results at the Ethereum Engineering Group meeting in this video. Finally, we have written a first blog post on our verification work, and a second post explaining a subtle possible error in the state transition function.

• we have formally verified the Deposit Smart Contracts with Dafny. The results have been published at the flagship conference Formal Methods'21: Cassez, F. (2021). Verification of the Incremental Merkle Tree Algorithm with Dafny. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science(), vol 13047. Springer, Cham. https://doi.org/10.1007/978-3-030-90870-6_24. We have presented our results at the Ethereum Engineering Group meeting in this video and in a blog post.

• we have developed a methodology to formally specify and reason about smart contracts using Dafny. The results are published at the Formal Methods for Industrial Critical Systems (FMICS'22): Cassez, F., Fuller, J., Quiles, H.M.A. (2022). Deductive Verification of Smart Contracts with Dafny. In: Groote, J.F., Huisman, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2022. Lecture Notes in Computer Science, vol 13487. Springer, Cham. https://doi.org/10.1007/978-3-031-15008-1_5. The paper got the Best Paper Award at FMICS'22.

• Recently we have developed a fully functional EVM in Dafny, the DafnyEVM. Once again, we have published our results at the flagship conference Formal Methods'23: Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In M. Chechik et al. (Eds.): FM 2023, LNCS 14000; Forthcoming. The preprint version of the paper is available here.

• A Blog Post on the formalisation of the semantics of the EVM in Dafny.

Methodology

How do you plan to achieve your research objectives?

Formal Verification

The main technique used in software engineering to uncover bugs is testing. However, testing has a severe limitation, as quoted by Dijkstra almost fifty years ago:

“Program testing can be used to show the presence of bugs, but never to show their absence!” Edsger W. Dijkstra (1930–2002), Turing Award 1972

To provide guarantees that a program does the right thing, we must first precisely define what the program is expected to do. This has the form of a specification, and the program is the implementation.

It is usually impossible to exhaustively test all the cases, and to prove conformance, and there is a need for alternative techniques. This is exactly what program verification is about. It is based on the seminal work of Tony Hoare, establishing the validity of Hoare triples. Hoare triples are of the form { P } f {Q} where f is a function performing a computation (e.g AddBytes below), and P is a logical statement corresponding to pre-condition on the input variables of f, i.e under which condition f is supposed to be used, and Q is the post-condition (e.g. (1) and (2) above) on the combination of the input and result variables of f, specifying what is guaranteed to hold at the end of any of f’s computation.

Proving the validity of Hoare triples is not a trivial task. It involves logical reasoning, finding loop invariants (logical statements) and induction proofs (for loops or recursive calls). However, thanks to tremendous progress in automated reasoning engines (SMT-solvers) in the last two decades, it has become feasible to design verification-aware programming languages, like Dafny that leverage the power of SMT-solvers to automatically verify the validity of Hoare triples.

Proposed Method to Verify EIP and Smart Contracts

The DafnyEVM can be used to prove properties about EVM bytecode. It can also be easily configured to support different versions of the semantics of bytecode (e.g. Berlin, London) and gas cost models. This makes it a target of choice to prototype EIPs and analyse their effects.

Regarding the second aspects of our project, to verify EVM bytecode, we can instrument the code with properties. The methodology to prove functional properties of EVM bytecode is to build proof objects: there are Dafny programs that contain the EVM bytecode and some instrumentation (e.g. assert statements, invariants, ghost variables etc). The proof objects enable us to reason about the code and prove some properties of interest.

Timeline

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.

Milestones

There are two tracks of work for this project (EIPs and Smart Contract Verification) which will run in parallel. They have separate milestones:

EIP Track

1. 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.
2. 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.
3. 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.
4. 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.
5. EIP3670 (Code Validation) and EIP5450 (Stack Validation). At this stage, we aim to wrap up the remaining EIPs.

Throughout the project, we expect team members to be following the discussions around the EOF and, for example, attending implementer calls, etc.

Smart Contract Verification Track

1. Verify No Arithmetic Underflow/Overflow in Wrapped Ether. The goal here is to repeat the verification conducted on the simple betting contract for a real world contract. For this milestone, we target the Wrapped Ether contract deployed at 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2 on Mainnet. In essence, this tests our ability to disassemble the contract and generate the DafnyEVM proof objects.
2. Verify Other Simple Properties for Wrapped Ether. The goal here is to expand the set of properties that our tool checks for beyond just overflow and underflow. For example, verifying there is no division by zero with the DIV and IDIV instructions. Other example properties might include verifying that CALLDATALOAD always requests data within bounds, or similarly that a RETURNDATACOPY does not revert due to an out-of-bounds access.
3. Verifying Complex Properties for Wrapped Ether. The goal here is to further expand the set of properties that our tool checks for. In particular, to demonstrate that the tool can verify key requirements are met (e.g. preservation of total supply, etc).
4. Verifying Other Deployed Contracts. At this stage, the goal is to try and use the tool on a wider range of deployed contracts in an effort to: (1) check the tool is capable of scaling to even larger contracts; (2) to look for hidden problems that other tools could not find.

Deliverables

For each milestone we will deliver the results in a git repository. Depending on the complexity and sensitivity of the results, we may keep the repository in restricted access before the results are published.

Budget

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): US$132K Our budget is for a total of six person months at US$22K per month (6 x 22K = 132K). This contributes towards 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).