Verified Translation Validation of Static Analyses
Accepted at CSF'17
Abstract
Motivated by applications to security and high efficiency, we propose
an automated methodology for validating on low-level intermediate
representations the results of a source-level static analysis. Our
methodology relies on two main ingredients: a relative-safety checker,
an instance of a relational verifier which proves that a program is
“safer” than another, and a transformation of programs
into defensive form which verifies the analysis results at runtime. We
prove the soundness of the methodology, and provide a formally
verified instantiation based on the Verasco verified C static analyzer
and the CompCert verified C compiler. We experiment with the
effectiveness of our approach with client optimizations at RTL level,
and static analyses for cache-based timing side-channels and memory
usage at pre-assembly levels.
Preprint (PDF)
Coq Development
The accompanying Coq development is available here. It requires Coq 8.4pl6 in order to be compiled.
Documentation
The development can be browsed online. The following files may be of interest.
- Cshmdefgen.v defines the defensive encoding of points-to annotations at the C#minor level
- RTLdefgen.v defines the defensive encoding of points-to annotations at the RTL level
- RTLdefgenproof.v proves the correctness of the defensive encoding
- Sylvie.v defines the syntax of product programs used for relative safety checking
- Product.v defines how to build such a product program
- VCGen.v defines the VC-gen and proves its correctness
- ProductSimulation.v proves the correctness of the relative safety checker
- Theorems.v proves the correctness of the translation validation for points-to analyses
- MachIRTaintAnalysis.v defines the taint analysis presented in the paper
- CSEannot.v is the modified CSE pass making use of the points-to annotations