×

zbMATH — the first resource for mathematics

Modular inference of subprogram contracts for safety checking. (English) Zbl 1213.68385
Summary: Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently.
The practical applicability of our approach is demonstrated on experiments performed on a library and two benchmarks of vulnerabilities of C code.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aiken, A.; Foster, J. S.; Kodumal, J.; Terauchi, T., Checking and inferring local non-aliasing, (), 129-140
[2] Assaad, M.G., Leavens, G.T., 2001. Alias-free parameters in C for better reasoning and optimization. Technical Report 01-11, Department of Computer Science, Iowa State University.
[3] Barnett, M.; Leino, K.R.M.; Schulte, W., The spec# programming system: an overview, (), 49-69
[4] Baudin, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V., 2008. ACSL: ANSI/ISO C Specification Language. http://frama-c.cea.fr/acsl.html.
[5] Bourdoncle, F., Assertion-based debugging of imperative programs by abstract interpretation, (), 501-516
[6] Bradley, A.R.; Manna, Z., The calculus of computation: decision procedures with applications to verification, (2007), Springer-Verlag New York, Inc. Secaucus, NJ, USA · Zbl 1126.03001
[7] Burdy, L.; Cheon, Y.; Cok, D.; Ernst, M.; Kiniry, J.; Leavens, G.T.; Leino, K.R.M.; Poll, E., An overview of JML tools and applications, International journal on software tools for technology transfer, (2004)
[8] C99, ISO/IEC 9899:1999: programming languages-C, (2000), International Organization for Standardization
[9] Calcagno, C.; Distefano, D.; O’Hearn, P.W.; Yang, H., Footprint analysis: a shape analysis that discovers preconditions, (), 402-418
[10] Chaki, S., Hissam, S., 2006. Certifying the absence of buffer overflows. Technical Note CMU/SEI-2006-TN-030, Carnegie-Mellon University/Software Engineering Institute.
[11] Colon, M.; Sankaranarayanan, S.; Sipma, H., Linear invariant generation using non-linear constraint solving, (), 420-432 · Zbl 1278.68164
[12] Conchon, S., Contejean, E., 2008. The Alt-Ergo automatic theorem prover http://alt-ergo.lri.fr/.
[13] Couchot, J.-F., Hubert, T., 2007. A Graph-based Strategy for the Selection of Hypotheses. In: FTP 2007 — International Workshop on First-Order Theorem Proving. Liverpool, UK.
[14] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (), 269-282 · Zbl 0788.68094
[15] Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (), 84-96
[16] Dahlweid, M.; Moskal, M.; Santen, T.; Tobies, S.; Schulte, W., VCC: contract-based modular verification of concurrent C, (), 429-430
[17] Dijkstra, E.W., ()
[18] Dill, D.L., Trace theory for automatic hierarchical verification of speed-independent circuits, (1989), MIT Press Cambridge, MA, USA
[19] Filliâtre, J.-C., Verification of non-functional programs using interpretations in type theory, Journal of functional programming, 13, 4, 709-745, (2003) · Zbl 1111.68389
[20] Filliâtre, J.-C.; Marché, C., The why/krakatoa/caduceus platform for deductive program verification, (), 173-177, URL http://www.lri.fr/ filliatr/ftp/publis/cav07.pdf
[21] Flanagan, C.; Leino, K.R.M., Houdini, an annotation assistant for ESC/Java, (), 500-517 · Zbl 0977.68671
[22] Gulwani, S.; Tiwari, A., Combining abstract interpreters, ()
[23] Gulwani, S.; Tiwari, A., Assertion checking unified, (), 363-377 · Zbl 1132.68470
[24] Hackett, B.; Das, M.; Wang, D.; Yang, Z., Modular checking for buffer overflows in the large, (), 232-241
[25] Hart, T.E., Ku, K., Lie, D., Chechik, M., Gurfinkel, A., 2008. Ptyasm: Software model checking with proof templates. In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE’08.
[26] Hatcliff, J., Leavens, G.T., Leino, K.R.M., Miller, P., Parkinson, M., 2009. Behavioral interface specification languages. Technical Report CS-TR-09-01, University of Central Florida, School of EECS, a survey paper, Draft. · Zbl 1293.68078
[27] Hubert, T., Marché, C., Mar. 2007. Separation analysis for deductive verification. In: Heap Analysis and Verification, HAV’07. Braga, Portugal, pp. 81-93, http://www.lri.fr/ marche/hubert07hav.pdf.
[28] Janota, M., 2007. Assertion-based loop invariant generation. In: Proceedings of the 1st International Workshop on Invariant Generation, WING’07. Hagenberg, Austria, workshop at CALCULEMUS, 2007.
[29] Jim, T.; Morrisett, J.G.; Grossman, D.; Hicks, M.W.; Cheney, J.; Wang, Y., Cyclone: A safe dialect of C, (), 275-288
[30] Karr, M., Affine relationships among variables of a program, Acta informatica, 133-151, (1976) · Zbl 0358.68025
[31] Kernighan, B.W.; Ritchie, D.M., The C programming language, (1978), Prentice-Hall Englewood Cliffs, New Jersey
[32] Koes, D.; Budiu, M.; Venkataramani, G., Programmer specified pointer independence, (), 51-59
[33] Ku, K.; Hart, T.E.; Chechik, M.; Lie, D., A buffer overflow benchmark for software model checkers, (), 389-392
[34] Lattner, C.; Lenharth, A.; Adve, V., Making context-sensitive points-to analysis with heap cloning practical for the real world, SIGPLAN notices, 42, 6, 278-289, (2007)
[35] Leino, K.R.M.; Logozzo, F., Loop invariants on demand, (), 119-134 · Zbl 1159.68374
[36] Leino, K.R.M., Logozzo, F., 2007. Using widenings to infer loop invariants inside an SMT solver, or: a theorem prover as abstract domain. Tech. Rep. RISC-Linz Report Series No. 07-07, RISC, Hagenberg, Austria, proc. WING’07.
[37] Leino, K.R.M.; Saxe, J.B.; Stata, R., Checking Java programs via guarded commands, (), 110-111
[38] Liang, D.; Harrold, M.J., Efficient computation of parameterized pointer information for interprocedural analyses, (), 279-298 · Zbl 1005.68898
[39] Marché, C., Jessie: an intermediate language for Java and C verification, (), 1-2, URL http://doi.acm.org/10.1145/1292597.1292602
[40] Miné, A., The octagon abstract domain, Higher order symbolic computation, 19, 1, 31-100, (2006) · Zbl 1105.68069
[41] Monniaux, D., 2008. A quantifier elimination algorithm for linear real arithmetic. CoRR abs/0803.1575, informal publication. · Zbl 1182.68213
[42] Moy, Y., 2009. Automatic modular static safety checking for C programs. Ph.D. Thesis, Université Paris-Sud.
[43] Norrish, M., 1998. C formalised in HOL. Ph.D. Thesis, University of Cambridge.
[44] Popeea, C.; Xu, D.N.; Chin, W.-N., A practical and precise inference and specializer for array bound checks elimination, (), 177-187
[45] Reynolds, J.C., Syntactic control of interference, (), 39-46
[46] Rival, X., Understanding the origin of alarms in , (), 303-319 · Zbl 1141.68376
[47] Rousset, N., 2008. Automatisation de la spécification et de la vérification d’applications Java Card. Thèse de doctorat, Université Paris-Sud.
[48] Starostin, A., 2006. Formal verification of a C-library for strings. Master’s Thesis, Saarland University.
[49] Steensgaard, B., Points-to analysis in almost linear time, (), 32-41
[50] Suzuki, N.; Ishihata, K., Implementation of an array bound checker, (), 132-143
[51] Talpin, J.-P., Jouvelot, P., 1991. Polymorphic type region and effect inference. Tech. Rep. EMP-CRI E/150. · Zbl 0817.68099
[52] Talpin, J.-P.; Jouvelot, P., The type and effect discipline, (), 162-173
[53] Tofte, M., Talpin, J.-P., 1997. Region-based memory management. Information and Computation. · Zbl 0876.68027
[54] Weispfenning, V., Complexity and uniformity of elimination in Presburger arithmetic, (), 48-53 · Zbl 0915.03032
[55] Xu, Z., 2000. Safety checking of machine code. Ph.D. Thesis, Univ. of Wisconsin, Madison.
[56] Xu, Z.; Miller, B.P.; Reps, T., Safety checking of machine code, ACM SIGPLAN notices, 35, 5, 70-82, (2000)
[57] Zitser, M.; Lippmann, R.; Leek, T., Testing static analysis tools using exploitable buffer overflows from open source code, SIGSOFT software engineering notes, 29, 6, 97-106, (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.