Team and background
Team members: Alessandro Coglio, Eric McCarthy, Eric Smith
We are employees at Kestrel Institute, a nonprofit organization dedicated to software research, but this proposal is a side project.
Main web site of Kestrel Institute:
https://www.kestrel.edu/
Most open-source software published here:
https://github.com/acl2/acl2/tree/master/books/kestrel
Links to related work:
https://www.kestrel.edu/home/projects/ethereum/index.html
https://www.kestrel.edu/home/people/coglio/index.html
https://www.kestrel.edu/home/people/eric.smith/index.html
https://www.kestrel.edu/home/people/mccarthy/index.html
We have extensive experience with formal methods, formal specifications of many algorithms including cryptographic primitives, formal models of VMs and ISAs such as the JVM and x86 binary, and formal verification of a variety of programs. In particular, we have formalized components of Bitcoin and Ethereum.
Project and justification
Proof-of-concept formal verification of the Rust implementation of the CKB-VM.
We propose to formally model subsets of the Rust language and the RISC-V ISA — subsets sufficient to formally verify a subset of the CKB-VM. As a proof-of-concept, this will introduce the technology to the Nervos community and, we hope, lead to a full formal verification of the CKB-VM as well as motivate additional layer-1 proofs using the technology. All work will be open-sourced to the ACL2 community libraries (see https://github.com/acl2/acl2/tree/master/books).
Correctness of layer-1, including the CKB-VM implementation, is essential to reduce existential risks. The more different formal methods that are applied to layer-1, the more assurance users will have that the CKB itself is secure. Our proofs increase that assurance.
High level technical specification and implementation
Our approach involves writing formal specifications in the industrial-strength ACL2 theorem prover (used by companies like Centaur, ARM, and Collins Aerospace). 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. For example, we and others have used ACL2 for formal verifications of Java bytecode programs and x86 programs.
We will create a model of a subset of the Rust language that is executable in the theorem prover, and a model of a subset of the RISC-V configuration used by CKB-VM (rv64imc + W^X) that is also executable in the theorem prover. Then we will prove that CKB-VM correctly implements rv64imc for some example RISC-V programs.
Timeline and project duration
We expect completion in 2 months after approval.
All artifacts will be open-sourced under a permissive license in the ACL2 community libraries, and will be written in a literate style that includes documentation.