A Verified Bignum Implementation in x86-64 Machine Code
Paper
Magnus O. Myreen and Gregorio Curello.
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code.
In Certified Programs and Proofs (CPP), 2013.Abstract
Verification of machine code can easily deteriorate into an endless clutter of low-level details. This paper presents a case study which shows that machine-code verification does not necessitate ghastly low-level proofs. The case study we describe is the construction of an x86-64 implementation of arbitrary-precision integer arithmetic. Compared with closely related work, our proofs are shorter and, more importantly, the reasoning is at a more convenient high level of abstraction, e.g. pointer reasoning is largely avoided. We achieve this improvement as a result of using previously developed tools, namely, a proof-producing decompiler and compiler. The work presented in this paper has been developed in the HOL4 theorem prover. The case study resulted in 800 lines of verified 64-bit x86 machine code.
Proof scripts
The proof scripts are part of the examples directory in the current development version of HOL4.
To browse the proof scripts, use the following links: multiwordScript.sml and x64_multiwordScript.sml.
To download and run the scripts:
- install Poly/ML.
- install the latest development version of the HOL4 theorem prover by doing a git clone from github (example) and then building HOL following the INSTALL instructions
- navigate to HOL/examples/machine-code/multiword/ and type Holmake, or open the script files in an interactive session using hol.