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

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

0x0B30afbf896A46415df70b0E4a12Dd7f2c73e5c1

Publications

Ethereum's Recursive Length Prefix in ACL2
Alessandro Coglio
August 2019
Technical Report, Kestrel Institute
{Description of a formal specification of RLP encoding and a verified implementation of RLP decoding, all developed in ACL2.}