Verified Translation Validation of Static Analyses

Gilles Barthe Sandrine Blazy Vincent Laporte David Pichardie Alix Trieu

Accepted at CSF'17


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.


The development can be browsed online. The following files may be of interest.