Sciweavers

ASIAN
2006
Springer

An Approach to Formal Verification of Arithmetic Functions in Assembly

13 years 7 months ago
An Approach to Formal Verification of Arithmetic Functions in Assembly
Abstract. It is customary to write performance-critical parts of arithmetic functions in assembly: this enables finely-tuned algorithms that use specialized processor instructions. However, such optimizations make formal verification of arithmetic functions technically challenging, mainly because of many bit-level manipulations of data. In this paper, we propose an approach for formal verification of arithmetic functions in assembly. It consists in the implementation in the Coq proof assistant of (1) a Hoare logic for assembly programs augmented with loops and (2) a certified translator to ready-to-run assembly with jumps. To properly handle formal verification of bit-level manipulations of data, we propose an original encoding of machine integers. For concreteness, we use the SmartMIPS assembly language, an extension of the MIPS instruction set for smartcards, and we explain the formal verification of an optimized implementation of the Montgomery multiplication, a de facto-standard fo...
Reynald Affeldt, Nicolas Marti
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ASIAN
Authors Reynald Affeldt, Nicolas Marti
Comments (0)