Proof pearl: A verified bignum implementation in x86-64 machine code

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en HOL4 titulado Proof pearl: A verified bignum implementation in x86-64 machine code.

Sus autores son

  • Magnus O. Myreen (de la Universidad de Cambridge)y
  • Gregorio Curello (de la Universidad Autónoma de Barcelona).

Su resumen es

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 necessarily require 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 and the case study resulted in 700 lines of verified 64-bit x86 machine code.

El código correspondiente se encuentra aquí.

El trabajo se presentará en la CPP 2013 (3rd International Conference on Certified Programs and Proofs).