Formal Verification of a C Value Analysis Based on Abstract Interpretation
In: Static Analysis ISBN: 9783642388552 SAS SAS-20th Static Analysis Symposium SAS-20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344; (2013)
Online
unknown
Zugriff:
International audience; Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone. This paper presents a formal verification using the Coq proof assistant: a formalization of a value analysis (based on abstract interpretation), and a soundness proof of the value analysis. The formalization relies on generic interfaces. The mechanized proof is facilitated by a translation validation of a Bourdoncle fixpoint iterator. The work has been integrated into the CompCert verified C-compiler. Our verified analysis directly operates over an intermediate language of the compiler having the same expressiveness as C. The automatic extraction of our value analysis into OCaml yields a program with competitive results, obtained from experiments on a number of benchmarks and comparisons with the Frama-C tool.; Les analyseurs statiques fondés sur l'interprétation abstraite sont des logiciels complexes implémentant des algorithmes sophistiqués. Bien que es techniques d'analyse statique soient bien comprises, leur implémentation pour de vrais langages est toujours source d'erreurs. Cet article présente une vérification formelle à l'aide de l'assistant à la preuve Coq : une formalisation d'une analyse de valeurs (fondée sur m'interprétation abstraite), et une preuve de correction de l'analyse de valeurs. La formalisation repose sur des interfaces génériques. La preuve mécanisée est facilitée par une validation a posteriori d'un itérateur de point fixe à la Bourdoncle. Ce travail a été intégré au compilateur formellement vérifié CompCert C. Notre analyse vérifiée opère directement sur un langage intermédiaire du compilateur ayant le même pouvoir d'expression que C. L'extraction automatique de notre analyse de valeurs en OCaml fournit un programme dont les résultats sont compétitifs avec ceux fournis par l'outil Frama-C.
Titel: |
Formal Verification of a C Value Analysis Based on Abstract Interpretation
|
---|---|
Autor/in / Beteiligte Person: | Blazy, Sandrine ; André Oliveira Maroneze ; Laporte, Vincent ; Pichardie, David ; Software certification with semantic analysis (CELTIQUE) ; Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4) ; Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) ; Harvard John A. Paulson School of Engineering and Applied Sciences (SEAS) ; University, Harvard ; Manuel Fahndrich and Francesco Logozzo ; ANR-11-INSE-0003,VERASCO,Vérification formelle d'analyseurs statiques et de compilateurs(2011) ; CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1) ; Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA) ; Harvard University [Cambridge] |
Link: | |
Quelle: | Static Analysis ISBN: 9783642388552 SAS SAS-20th Static Analysis Symposium SAS-20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344; (2013) |
Veröffentlichung: | Springer Berlin Heidelberg, 2013 |
Medientyp: | unknown |
ISBN: | 978-3-642-38855-2 (print) |
DOI: | 10.1007/978-3-642-38856-9_18 |
Schlagwort: |
|
Sonstiges: |
|