Skip to Main content Skip to Navigation
Conference papers

Verified Translation Validation of Static Analyses

Gilles Barthe 1 Sandrine Blazy 2 Vincent Laporte 1 David Pichardie 2 Alix Trieu 2 
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Complete list of metadata

Cited literature [48 references]  Display  Hide  Download
Contributor : Alix Trieu Connect in order to contact the contributor
Submitted on : Friday, September 15, 2017 - 4:13:22 PM
Last modification on : Monday, April 4, 2022 - 9:28:22 AM
Long-term archiving on: : Saturday, December 16, 2017 - 2:03:29 PM


Files produced by the author(s)


  • HAL Id : hal-01588422, version 1


Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu. Verified Translation Validation of Static Analyses. Computer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States. ⟨hal-01588422⟩



Record views


Files downloads