ARM Verification

Presented as part of the 2007 HCSS conference.

Abstract

This talk will present preliminary results on a project to create correct by construction ARM machine code implementations of elliptic curve cryptography. Starting from the mathematical theory of elliptic curves formalized in higher order logic, the verification flow employs a compiler targeting a formalized model of the ARM processor. In addition to producing ARM machine code, the verifying compiler also generates a proof that the code implements the mathematical specification of the cryptographic algorithm.