research-article

A Formally-Verified C Static Analyzer

Authors:

Jacques-Henri Jourdan,

Vincent Laporte,

Sandrine Blazy,

David PichardieAuthors Info & Claims

POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Pages 247 - 259

https://doi.org/10.1145/2676726.2676966

Published: 14 January 2015 Publication History

Abstract

This paper reports on the design and soundness proof, using the Coq proof assistant, of Verasco, a static analyzer based on abstract interpretation for most of the ISO C 1999 language (excluding recursion and dynamic allocation). Verasco establishes the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. Verasco integrates with the CompCert formally-verified C compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled code.

Supplementary Material

MPG File (p247-sidebyside.mpg)

Download
1133.18 MB

References

[1]

A. Ahmed, A. W. Appel, C. D. Richards, K. N. Swadi, G. Tan, and D. C. Wang. Semantic foundations for typed assembly languages. ACM Trans. Program. Lang. Syst., 32(3), 2010.

Digital Library

[2]

A. W. Appel. Program Logics for Certified Compilers. Cambridge University Press, 2014.

[3]

A. W. Appel and S. Blazy. Separation logic for small-step Cminor. In TPHOLs, volume 4732 of LNCS, pages 5--21. Springer, 2007.

Digital Library

[4]

A. W. Appel and D. A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657--683, 2001.

Digital Library

[5]

Y. Bertot. Structural abstract interpretation: A formal study using Coq. In Language Engineering and Rigorous Software Development, LerNet Summer School, pages 153--194. Springer, 2008.

Digital Library

[6]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In PLDI, pages 196--207. ACM, 2003.

Digital Library

[7]

S. Blazy, Z. Dargaye, and X. Leroy. Formal verification of a C compiler front-end. In Formal Methods, volume 4085 of LNCS, pages 460--475. Springer, 2006.

Digital Library

[8]

S. Blazy, V. Laporte, A. Maroneze, and D. Pichardie. Formal verification of a C value analysis based on abstract interpretation. In SAS, volume 7935 of LNCS, pages 324--344. Springer, 2013.

[9]

S. Boldo and G. Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In ARITH, pages 243--252. IEEE, 2011.

Digital Library

[10]

T. Braibant, J.-H. Jourdan, and D. Monniaux. Implementing and reasoning about hash-consed data structures in Coq. J. Autom. Reasoning, 53(3):271--304, 2014.

Digital Library

[11]

D. Cachera, T. P. Jensen, D. Pichardie, and V. Rusu. Extracting a data flow analyser in constructive logic. Theor. Comput. Sci., 342(1):56--78, 2005.

Digital Library

[12]

A. Chlipala. Modular development of certified program verifiers with a proof assistant,. J. Funct. Program., 18(5--6):599--647, 2008.

Digital Library

[13]

S. Cho, J. Kang, J. Choi, C.-K. Hur, and K. Yi. SparrowBerry: A verified validator for an industrial-strength static analyzer.texttthttp://ropas.snu.ac.kr/sparrowberry/, 2013.

[14]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238--252. ACM, 1977.

Digital Library

[15]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In POPL, page 269--282. ACM, 1979.

Digital Library

[16]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, and X. Rival. Why does Astrée scale up? Formal Methods in System Design, 35(3):229--264, 2009.

Digital Library

[17]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. Combination of abstractions in the Astrée static analyzer. In ASIAN, volume 4435 of LNCS, pages 272--300. Springer, 2006.

Digital Library

[18]

A. Fouilhé, D. Monniaux, and M. Périn. Efficient generation of correctness certificates for the abstract domain of polyhedra. In SAS, volume 7935 of LNCS, pages 345--365. Springer, 2013.

[19]

A. Fouilhé and S. Boulmé. A certifying frontend for (sub)polyhedral abstract domains. In VSTTE, volume 8471 of LNCS, pages 200--215. Springer, 2014.

[20]

D. Greenaway, J. Andronick, and G. Klein. Bridging the gap: Automatic verified abstraction of C. In ITP, volume 7406 of LNCS, pages 99--115. Springer, 2012.

[21]

S. Gulwani, A. Tiwari, and G. C. Necula. Join algorithms for the theory of uninterpreted functions. In FSTTCS, volume 3328 of LNCS, pages 311--323. Springer, 2004.

Digital Library

[22]

N. Halbwachs and M. Péron. Discovering properties about arrays in simple programs. In PLDI, pages 339--348. ACM, 2008.

Digital Library

[23]

P. Herms, C. Marché, and B. Monate. A certified multi-prover verification condition generator. In VSTTE, volume 7152 of LNCS, pages 2--17. Springer, 2012.

Digital Library

[24]

M. Hofmann, A. Karbyshev, and H. Seidl. Verifying a local generic solver in Coq. In SAS, volume 6337 of LNCS, pages 340--355, 2010.

Digital Library

[25]

G. Klein and T. Nipkow. A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst., 28(4):619--695, 2006.

Digital Library

[26]

X. Leroy. Formal verification of a realistic compiler. Comm. ACM, 52(7):107--115, 2009.

Digital Library

[27]

X. Leroy. A formally verified compiler back-end. J. Automated Reasoning, 43(4):363--446, 2009.

Digital Library

[28]

A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31--100, 2006.

Digital Library

[29]

A. Miné. Symbolic methods to enhance the precision of numerical abstract domains. In VMCAI, volume 3855 of LNCS, pages 348--363. Springer, 2006.

Digital Library

[30]

D. Monniaux. Réalisation mécanisée d'interpréteurs abstraits. Master's thesis, U. Paris 7, 1998.

[31]

J. A. Navas, P. Schachte, H. Søndergaard, and P. J. Stuckey. Signedness-agnostic program analysis: Precise integer bounds for low-level code. In APLAS, volume 7705 of LNCS, pages 115--130. Springer, 2012.

[32]

F. Nielson, H. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 2005.

Digital Library

[33]

T. Nipkow. Abstract interpretation of annotated commands. In ITP, volume 7406 of LNCS, pages 116--132. Springer, 2012.

[34]

D. Pichardie. Interprétation abstraite en logique intuitionniste: extraction d'analyseurs Java certifiés. PhD thesis, U. Rennes 1, 2005.

[35]

D. Pichardie. Building certified static analysers by modular construction of well-founded lattices. Electr. Notes Theor. Comput. Sci., 212:225--239, 2008.

Digital Library

[36]

T. W. Reps, G. Balakrishnan, and J. Lim. Intermediate-representation recovery from low-level code. In PEPM, pages 100--111. ACM, 2006.

Digital Library

[37]

X. Rival and L. Mauborgne. The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst., 29(5), 2007.

Digital Library

Cited By

Monat ROuadjaout AMiné A(2025)Easing maintenance of academic static analyzersInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00770-126:6(673-686)Online publication date: 14-Jan-2025
Erhard JBentele MHeizmann MKlumpp DSaan SSchüssele FSchwarz MSeidl HTilscher SVojdani V(2025)Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with GhostsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-82700-6_4(74-100)Online publication date: 20-Jan-2025
Barrière A(2025)Formal Verification of Just-in-Time CompilationundefinedOnline publication date: 28-Jan-2025
Show More Cited By

Index Terms

A Formally-Verified C Static Analyzer

Recommendations

A verified prover based on ordered resolution
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional ...
Soundness and Completeness Proofs by Coinductive Methods

We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an ...
Formally verified differential dynamic logic
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

We formalize the soundness theorem for differential dynamic logic, a logic for verifying hybrid systems. To increase confidence in the formalization, we present two versions: one in Isabelle/HOL and one in Coq. We extend the metatheory to include ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 2015

716 pages

ISBN:9781450333009

DOI:10.1145/2676726

General Chair:
Sriram Rajamani
Microsoft Research, India
,
Program Chair:
David Walker
Princeton University, USA

ACM SIGPLAN Notices Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Agence Nationale de la Recherche

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 15 - 17, 2015

Mumbai, India

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

98
Total Citations
View Citations
648
Total Downloads

Downloads (Last 12 months)67
Downloads (Last 6 weeks)6

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Monat ROuadjaout AMiné A(2025)Easing maintenance of academic static analyzersInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00770-126:6(673-686)Online publication date: 14-Jan-2025
Erhard JBentele MHeizmann MKlumpp DSaan SSchüssele FSchwarz MSeidl HTilscher SVojdani V(2025)Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with GhostsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-82700-6_4(74-100)Online publication date: 20-Jan-2025
Barrière A(2025)Formal Verification of Just-in-Time CompilationundefinedOnline publication date: 28-Jan-2025
Michelland SZakowski YGonnord L(2024)Abstract Interpreters: A Monadic Approach to Modular VerificationProceedings of the ACM on Programming Languages10.1145/36746468:ICFP(602-629)Online publication date: 15-Aug-2024
Lesbre DLemerre M(2024)Compiling with Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/36563928:PLDI(368-393)Online publication date: 20-Jun-2024
Erhard JSchinabeck JSchwarz MSeidl HMonat RRubio-González C(2024)When to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the FlyProceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis10.1145/3652588.3663321(35-44)Online publication date: 20-Jun-2024
Smith IBertolaccini FTan WBrown M(2024)IRENE: A Toolchain for High-level Micropatching through Recompilable Sub-function RegionsMILCOM 2024 - 2024 IEEE Military Communications Conference (MILCOM)10.1109/MILCOM61039.2024.10773695(1064-1069)Online publication date: 28-Oct-2024
Monniaux D(2024)Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00760-326:4(463-477)Online publication date: 1-Aug-2024
Keidel SHelm DRoth TMezini M(2024)A Modular Soundness Theory for the Blackboard Analysis ArchitectureProgramming Languages and Systems10.1007/978-3-031-57267-8_14(361-390)Online publication date: 6-Apr-2024
Blazy S(2024)From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCertFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_1(1-21)Online publication date: 6-Apr-2024
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten