Sandrine: Created page with "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..."

2018-05-18T08:09:37Z

Created page with "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..."

New page

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.

Joint work with Gilles Barthe, Vincent Laporte, David Pichardie and Alix Trieu

WG211/M18Blazy - Revision history

Sandrine: Created page with "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..."