Advertisement

Formal Verification of a C Value Analysis Based on Abstract Interpretation

  • Sandrine Blazy
  • Vincent Laporte
  • André Maroneze
  • David Pichardie
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7935)

Abstract

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.

Keywords

Memory Model Abstract Interpretation Proof Assistant Abstract Domain Program Point 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Bertot, Y., Grégoire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 66–81. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Certified result checking for polyhedral analysis of bytecode programs. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010, LNCS, vol. 6084, pp. 253–267. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Boldo, S., Jourdan, J., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: Proc. of ARITH 21. IEEE Computer Society Press (to appear, 2013)Google Scholar
  6. 6.
    Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol. 735, pp. 128–141. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  7. 7.
    Cachera, D., Jensen, T.P., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theoretical Computer Science 342(1), 56–78 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Cachera, D., Pichardie, D.: A certified denotational abstract interpreter. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 9–24. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  9. 9.
    Coupet-Grimal, S., Delobel, W.: A uniform and certified approach for two static analyses. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 115–137. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The Astrée analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. of POPL 1978, pp. 84–97. ACM Press (1978)Google Scholar
  13. 13.
    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  14. 14.
    Pichardie, D.: Interprétation abstraite en logique intuitionniste : extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes 1 (2005) (in French)Google Scholar
  15. 15.
    Gonthier, G.: The Four Colour Theorem: Engineering of a Formal Proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  16. 16.
    Gonthier, G.: Engineering mathematics: the odd order theorem proof. In: Proc. of POPL 2013, pp. 1–2. ACM (2013)Google Scholar
  17. 17.
    Hofmann, M., Karbyshev, A., Seidl, H.: Verifying a local generic solver in Coq. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 340–355. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  18. 18.
    Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: SeL4: formal verification of an operating-system kernel. Comm. of the ACM 53(6), 107–115 (2010)CrossRefGoogle Scholar
  19. 19.
    Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM TOPLAS 28(4), 619–695 (2006)CrossRefGoogle Scholar
  20. 20.
    Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363–446 (2009)MathSciNetzbMATHCrossRefGoogle Scholar
  21. 21.
    Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model, version 2. Research report RR-7987, INRIA (June 2012)Google Scholar
  22. 22.
    Robert, V., Leroy, X.: A formally-verified alias analysis. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 11–26. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  23. 23.
    Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Proc. of LCTES 2006, pp. 54–63. ACM (June 2006)Google Scholar
  24. 24.
    Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Signedness-agnostic program analysis: Precise integer bounds for low-level code. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 115–130. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  25. 25.
    Nipkow, T.: Abstract interpretation of annotated commands. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 116–132. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  26. 26.
    Rideau, S., Leroy, X.: Validating register allocation and spilling. In: Gupta, R. (ed.) CC 2010. LNCS, vol. 6011, pp. 224–243. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  27. 27.
    Simon, A., King, A.: Taming the wrapping of integer arithmetic. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 121–136. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  28. 28.
    Vafeiadis, V., Zappa Nardelli, F.: Verifying fence elimination optimisations. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 146–162. Springer, Heidelberg (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Sandrine Blazy
    • 1
  • Vincent Laporte
    • 1
  • André Maroneze
    • 1
  • David Pichardie
    • 2
  1. 1.IRISAUniversité Rennes 1France
  2. 2.INRIAHarvard UniversityUSA

Personalised recommendations