Verified Translation Validation of Static Analyses

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.
Type de document :
Communication dans un congrès
Computer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States. 30th IEEE Computer Security Foundations Symposium
Liste complète des métadonnées

Littérature citée [48 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01588422
Contributeur : Alix Trieu <>
Soumis le : vendredi 15 septembre 2017 - 16:13:22
Dernière modification le : jeudi 15 novembre 2018 - 11:58:59
Document(s) archivé(s) le : samedi 16 décembre 2017 - 14:03:29

Fichier

csf17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01588422, version 1

Citation

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. 30th IEEE Computer Security Foundations Symposium. 〈hal-01588422〉

Partager

Métriques

Consultations de la notice

866

Téléchargements de fichiers

183