Marie-Christine Jakobs
ABSTRACT
Configurable program analysis (CPA) is a generic concept for the formalization of different software analysis techniques in a single framework. With the tool CPAchecker, this framework allows for an easy configuration and subsequent automatic execution of analysis procedures ranging from data-flow analysis to model checking. The focus of the tool CPAchecker is thus on analysis. In this paper, we study configurability from the point of view of software certification. Certification aims at providing (via a prior analysis) a certificate of correctness for a program which is (a) tamper-proof and (b) more efficient to check for validity than a full analysis. Here, we will show how, given an analysis instance of a CPA, to construct a corresponding sound certification instance, thereby arriving at configurable program certification. We report on experiments with certification based on different analysis techniques, and in particular explain which characteristics of an underlying analysis allow us to design an efficient (in the above (b) sense) certification procedure.
- M. Alba-Castro, M. Alpuente, and S. Escobar. Automatic certification of java source code in rewriting logic. In FMICS, LNCS, pages 200–217. Springer, 2007. Google Scholar
Digital Library
- E. Albert, P. Arenas-Sánchez, G. Puebla, and M. V. Hermenegildo. Reduced certificates for abstraction-carrying code. In ICLP, LNCS, pages 163–178. Springer, 2006. Google ScholarDigital Library
- E. Albert, G. Puebla, and M. V. Hermenegildo. Abstraction-carrying code. In LPAR, LNCS, pages 380–397. Springer, 2004.Google Scholar
- W. Amme, M.-A. Möller, and P. Adler. Data flow analysis as a general concept for the transport of verifiable program annotations. Electr. Notes Theor. Comput. Sci., 176(3):97–108, 2007. Google ScholarDigital Library
- T. Amtoft, J. Dodds, Z. Zhang, A. W. Appel, L. Beringer, J. Hatcliff, X. Ou, and A. Cousino. A certificate infrastructure for machine-checked proofs of conditional information flow. In POST, LNCS, pages 369–389. Springer, 2012. Google ScholarDigital Library
- A. W. Appel. Foundational proof-carrying code. In LICS, pages 247–256. IEEE Computer Society, 2001. Google ScholarDigital Library
- L. Bauer, M. A. Schneider, E. W. Felten, and A. W. Appel. Access control on the web using proof-carrying authorization. In Proceedings of the 3rd DARPA Information Survivability Conference and Exposition (DISCEX (2)), pages 117–119. IEEE Computer Society, 2003.Google Scholar
- F. Besson, T. P. Jensen, and D. Pichardie. Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci., 364(3):273–291, 2006. Google ScholarDigital Library
- D. Beyer. Second competition on software verification - (summary of SV-COMP 2013). In TACAS, LNCS, pages 594–609. Springer, 2013. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, and G. Théoduloz. Program analysis with dynamic precision adjustment. In ASE, pages 29–38. IEEE, 2008. Google ScholarDigital Library
- D. Beyer, M. Keremoglu, and P. Wendler. Predicate abstraction with adjustable-block encoding. In FMCAD, pages 189–197. IEEE, 2010. Google ScholarDigital Library
- D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In CAV, LNCS, pages 184–190. Springer, 2011. Google ScholarDigital Library
- D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, and P. Wendler. Precision reuse for efficient regression verification. In ESEC/SIGSOFT FSE, pages 389–399. ACM, 2013. Google ScholarDigital Library
- A. Chaieb. Proof-producing program analysis. In ICTAC, LNCS, pages 287–301. Springer, 2006. Google ScholarDigital Library
- K. Crary and S. Weirich. Resource bound certification. In POPL, pages 184–198. ACM, 2000. Google ScholarDigital Library
- K. Dräger, A. Kupriyanov, B. Finkbeiner, and H. Wehrheim. SLAB: a certifying model checker for infinite-state concurrent systems. In TACAS, LNCS, pages 271–274. Springer, 2010.Google Scholar
- S. Drzevitzky, U. Kastens, and M. Platzner. Proof-carrying hardware: Towards runtime verification of reconfigurable modules. In International Conference on Reconfigurable Computing and FPGAs (ReConFig), pages 189–194. IEEE Computer Society, 2009. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, G. C. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In CAV, LNCS, pages 526–538. Springer, 2002. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and M. A. A. Sanvido. Extreme model checking. In Verification: Theory and Practice, LNCS, pages 332–358. Springer, 2003.Google Scholar
- K. Klohs and U. Kastens. Memory requirements of java bytecode verification on limited devices. Electr. Notes Theor. Comput. Sci., 132(1):95–111, 2005. Google ScholarDigital Library
- G. C. Necula. Proof-carrying code. In POPL, pages 106–119. ACM Press, 1997. Google ScholarDigital Library
- G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: intermediate language and tools for analysis and transformation of C programs. In CC, LNCS, pages 213–228. Springer, 2002. Google ScholarDigital Library
- F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer Heidelberg, 2004. Google ScholarDigital Library
- X. Rival and L. Mauborgne. The trace partitioning abstract domain. ACM Transaction on Programming Languages and Systems, 29(5), 2007. Google ScholarDigital Library
- E. Rose. Lightweight bytecode verification. J. Autom. Reasoning, 31(3-4):303–334, 2003. Google ScholarDigital Library
- D. Wonisch, A. Schremmer, and H. Wehrheim. Programs from proofs - a PCC alternative. In CAV, LNCS, pages 912–927. Springer, 2013.Google Scholar
- S. Xia and J. Hook. Certifying temporal properties for compiled C programs. In VMCAI, LNCS, pages 161–174. Springer, 2004.Google Scholar
Index Terms
- Certification for configurable program analysis
Comments