Using Dependent Types to Certify the Safety of Assembly Code

14 years 25 days ago
Using Dependent Types to Certify the Safety of Assembly Code
There are many source-level analyses or instrumentation tools that enforce various safety properties. In this paper we present an infrastructure that can be used to check independently that the assembly output of such tools has the desired safety properties. By working at assembly level we avoid the complications with unavailability of source code, with source-level parsing, and we certify the code that is actually deployed. The novel feature of the framework is an extensible dependently-typed framework that supports type inference and mutation of dependent values in memory. The type system can be extended with new types as needed for the source-level tool that is certified. Using these dependent types, we are able to express the invariants enforced by CCured, a sourcelevel instrumentation tool that guarantees type safety in legacy C programs. We can therefore check that the x86 assembly code resulting from compilation with CCured is in fact type-safe.
Matthew Harren, George C. Necula
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SAS
Authors Matthew Harren, George C. Necula
Comments (0)