Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving

Abstract. Vx86 is the first static analyzer for sequential Intel x86 assembler code using automated deductive verification. It proves the correctness of assembler code against function contracts, which are expressed in terms of pre-, post-, and frame conditions using first-order predicates. Vx86 takes the annotated assembler code, translates it into C code simulating the processor, and then uses an existing C verifier to either prove the correctness of the assembler program or find errors in it. First experiments on applying Vx86 on the Windows Hypervisor code base are encouraging. Vx86 verified the Windows Hypervisor's memory safety, arithmetic safety, call safety and interrupt safety.

• Type: Conference
• Year: 2008
• Where: AMAST
• Authors: Stefan Maus, Michal Moskal, Wolfram Schulte
• Keywords: AMAST 2008, Assembler Code, Intel X86 Assembler, Software Engineering, Windows Hypervisor