ACL2 Ethereum Project

Team

Goals

The goal of the ACL2 Ethereum project is to formally specify and synthesize/implement a full Ethereum client using the ACL2 theorem prover and the APT toolkit.

The first phase of the project, completed in August 2019, focused on formalizing the cryptographic primitives used in Ethereum. We developed a proof-of-concept formally-defined hierarchical deterministic wallet suitable for cold storage of keys and transaction signing. We would like to thank the Ethereum Foundation for supporting this work.

The wallet uses the following cryptographic algorithms. Each link points to documentation we wrote about our formalization. The documentation pages contain links to the official standards or specifications. See: Keccak-256, SHA-256 and SHA-512, HMAC, PBKDF2, secp256k1, and deterministic ECDSA, and HD wallet standards and other standards such as BIP-32, BIP-39, BIP-43, BIP-44, and EIP 155.

In addition, we developed a formal specification of RLP encoding and a verified implementation of RLP decoding, along with consistency proofs. See the technical report for more information. We also specified Modified Merkle Patricia Tree processing.

In the process of formalizing all the above components, we identified and reported a number of bugs and limitations in EthereumJ, Aleth, and KEVM. (We also reported an error in a NIST specification.) We also applied our Axe verification tool to prove correctness of kethereum’s Kotlin implementation of SHA-256, the bouncycastle Java implementation of SHA-256, and the GNU Java implementation of RIPEMD-160.

We have also made a number of improvements to the Ethereum Yellow Paper, many of which are documented here. Thanks to the Decentralization Foundation for additional support of this work.

Specifications created during the project, and supporting libraries that we have open-sourced, have been published in the ACL2 prover’s community libraries, which are also called the “Community Books”. Many of the source files have extensive comments, and we have also written documentation suitable for the ACL2 XDOC system. Some good starting points for exploring the documentation:

This project is motivated by the grand vision that all software development should incorporate formal methods and have proofs. More urgently, cryptocurrencies should have a diversity of formal methods brought to bear on them, since the consequences of vulnerabilities are so dire.

On the Suitability of ACL2 and APT

ACL2 is a theorem prover whose language can express both high-level declarative specifications and efficiently executable programs. Since the ACL2 language has a formally defined semantics, specifications and programs are amenable to formal proofs. In particular, specifications that are easy to reason about and to validate against external requirements can be provably refined to efficient executable code. Kestrel Institute’s APT toolkit of automated program transformations, built on top of ACL2, allows a developer to synthesize efficiently executable implementations from high-level declarative specifications, automatically generating formal proofs of the correctness of the implementations with respect to the specifications.

Benefits and Possible Extensions of this Work

  • Security-conscious parties can run the ACL2 implementation as a high-assurance Ethereum node.
  • The ACL2 implementation can be used for cross-testing other implementations.
  • The formal specification, along with the APT transformation toolkit and a formal model of the target language, can be used to generate a high-assurance client in another programming language.
  • The formal specification can serve as a reference that augments other specifications such as the Yellow Paper.
  • The formal specification can be used for cross-checking and verifying components of implementations in other programming languages, using our APT transformation tools and our Axe verification tools.
  • The formal specification can be used for proving global properties of the entire blockchain.
  • The formal specification and the APT toolkit can be used to rapid-prototype and prove properties about EIPs.
  • The formal specification provides a basis for developing high-assurance tools for exploring blockchain data and smart contract code.
  • The formal specification can be used to prove smart contract correctness and properties such as gas usage, using our high-performance Axe toolkit.
  • The formal specification provides a basis for building verifying compilers from smart contract languages to EVM and eWASM code.

Collaboration Opportunities

Besides the work mentioned above and on other Kestrel Institute project pages, we have been formalizing other elliptic curves such as Twisted Edwards curves and we are developing a SNARK R1CS (Rank-One Constraint System) verification system.

Please contact us if you would like to explore collaboration ideas with us, or if you would like to sponsor related research.

Donations

ENS: KestrelInstitute.eth
hex: 0x0B30afbf896A46415df70b0E4a12Dd7f2c73e5c1

Publications

Ethereum’s Recursive Length Prefix in ACL2
Alessandro Coglio
May 2020
16th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2020)
{Description of a formal specification of RLP encoding and a verified implementation of RLP decoding, all developed in ACL2. This web version of the paper is identical to the one published at EPTCS, with the addition of an appendix about ACL2 to make the paper more self-contained.}