Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving

Stefan Maus, Michal Moskal, and Wolfram Schulte

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.

Details

Publication typeInproceedings
Published inAMAST
Pages284-298
Volume5140
SeriesLecture Notes in Computer Science
ISBN978-3-540-79979-5
PublisherSpringer
> Publications > Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving