ACL2 Ethereum Project
The first phase of the project, starting in October 2018, is to create a high-assurance command-line wallet suitable for cold storage of keys and transaction signing. This requires specifications and implementations of cryptographic algorithms such as Keccak-256, SHA-256, HMAC-SHA512, and secp256k1, and HD wallet standards such as BIP-32, BIP-39, BIP-43, and BIP-44. In addition, we will be synthesizing code for RLP encoding/decoding and Modified Merkle Patricia Tree processing.
Code created during the project, and supporting libraries that we are in the process of open-sourcing, will be published primarily under the Community Books directory of ACL2.
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.
Please contact us if you would like to explore collaboration ideas with us, or if you would like to sponsor related research.