Stack-Aware CompCert: Verified Compilation of C Programs into Machine Code
Speaker
汪宇霆, Yale University
Time
2019-02-23 14:00:00 ~ 2019-02-23 15:00:00
Location
Room 1319, Software Expert Building
Host
Qinxiang Cao, Assistant Professor, John Hopcroft Center for Computer Science
Abstract
A majority of the existing work on program verification is carried out in high-level programming languages (e g , C C++, Java, ML, Haskell) which provide abstraction mechanisms useful not only for programming but also for verification However, properties about the programs proved at the source level may no longer hold when they are compiled to executable code To bridge this gap, the compilers of these languages also need to be verified, i e, to show they preserve the behaviors of programs being compiled.
The C programming language has been widely used to implement system software for several decades The state-of-the-art verified compiler for C is CompCert which has been successfully applied to verification of realistic system software such as OS kernels However, CompCert lacks a key feature for end-to-end verification of system software: generation of native machine code Its verified compilation chain outputs a form of assembly code which is still quite far away from the actual assembly code In particular, it does not operate over a finite stack Instead, the stack is represented as an unbounded list of memory blocks even at the lowest level This essentially precludes generation of verified binary code in verification projects using CompCert.
We present Stack-Aware CompCert, the first extension of CompCert that compiles to machine code and that supports all the features of CompCert We overcome the deficiency of CompCert described above by enriching its memory model with an abstract stack that keeps track of the history of stack frames to bound the stack consumption Using this enriched memory model for all the languages of CompCert, we are able to reprove the correctness of the full compilation chain of CompCert, including all the advanced optimization passes, such as inlining and tail-call recognition, which no previous approaches have successfully shown to preserve stack consumption.
Another limitation of CompCert is that it only supports verified compilation of whole programs For verification of software systems, it is often necessary to prove correct the compilation of programs in an arbitrary context (e g , assembly programs calling a C function) We show that Stack-Aware CompCert supports this kind of contextual compilation In particular, by enriching our abstract stack with fine-grained stack permissions, we are able to enforce a uniform stack access policy for both the context and the program being compiled, leading to verified contextual compilation.
The C programming language has been widely used to implement system software for several decades The state-of-the-art verified compiler for C is CompCert which has been successfully applied to verification of realistic system software such as OS kernels However, CompCert lacks a key feature for end-to-end verification of system software: generation of native machine code Its verified compilation chain outputs a form of assembly code which is still quite far away from the actual assembly code In particular, it does not operate over a finite stack Instead, the stack is represented as an unbounded list of memory blocks even at the lowest level This essentially precludes generation of verified binary code in verification projects using CompCert.
We present Stack-Aware CompCert, the first extension of CompCert that compiles to machine code and that supports all the features of CompCert We overcome the deficiency of CompCert described above by enriching its memory model with an abstract stack that keeps track of the history of stack frames to bound the stack consumption Using this enriched memory model for all the languages of CompCert, we are able to reprove the correctness of the full compilation chain of CompCert, including all the advanced optimization passes, such as inlining and tail-call recognition, which no previous approaches have successfully shown to preserve stack consumption.
Another limitation of CompCert is that it only supports verified compilation of whole programs For verification of software systems, it is often necessary to prove correct the compilation of programs in an arbitrary context (e g , assembly programs calling a C function) We show that Stack-Aware CompCert supports this kind of contextual compilation In particular, by enriching our abstract stack with fine-grained stack permissions, we are able to enforce a uniform stack access policy for both the context and the program being compiled, leading to verified contextual compilation.
Bio
Yuting Wang is an associate research scientist at Yale University, working in Dr. Zhong Shao's group. Prior to joining Yale, he was a Ph.D. student at the University of Minnesota, Twin Cities, supervised by Dr. Gopalan Nadathur. His research interests include verified compilation, formal verification of system software, theories and implementation techniques of theorem provers for formal verification. He is a member of the core development team for Abella, an interactive theorem prover specialized in formalization and verification of meta-properties of programming languages and logics, and their compilation and transformations.
Website: http://www.cs.yale.edu/homes/wang-yuting/
Website: http://www.cs.yale.edu/homes/wang-yuting/