Abstract
Assertion checking is the restriction of program verification to validity of program assertions. It encompasses safety checking, which is program verification of safety properties, like memory safety or absence of overflows. In this paper, we consider assertion checking of program parts instead of whole programs, which we call modular assertion checking. Classically, modular assertion checking is possible only if the context in which a program part is executed is known. By default, the worst-case context must be assumed, which may impair the verification task. It usually takes user effort to detail enough the execution context for the verification task to succeed, by providing strong enough preconditions. We propose a method to automatically infer sufficient preconditions in the context of modular assertion checking of imperative pointer programs. It combines abstract interpretation, weakest precondition calculus and quantifier elimination. We instantiate this method to prove memory safety for C and Java programs, under some memory separation conditions.
This research is partly supported by CIFRE contract 2005/973 with France Télécom company, and ANR RNTL ‘CAT’.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol. 2304, pp. 159–178. Springer, Heidelberg (2002)
Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, Springer, Heidelberg (2007)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, pp. 84–96. ACM, New York (1978)
Suzuki, N., Ishihata, K.: Implementation of an array bound checker. In: Proc. POPL 1977, pp. 132–143. ACM, New York (1977)
Xu, Z., Miller, B.P., Reps, T.: Safety checking of machine code. ACM SIGPLAN Notices 35(5), 70–82 (2000)
Xu, Z.: Safety checking of machine code. PhD thesis, Univ. of Wisconsin, Madison (2000)
Bourdoncle, F.: Assertion-based debugging of imperative programs by abstract interpretation. In: Sommerville, I., Paul, M. (eds.) ESEC 1993. LNCS, vol. 717, pp. 501–516. Springer, Heidelberg (1993)
Rival, X.: Understanding the origin of alarms in astrée. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 303–319. Springer, Heidelberg (2005)
Gulwani, S., Tiwari, A.: Assertion checking unified. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, Springer, Heidelberg (2007)
International Organization for Standardization (ISO) (The ANSI C standard (C99))
Aiken, A., et al.: Checking and inferring local non-aliasing. In: Proc. PLDI 2003, pp. 129–140. ACM, New York (2003)
Koes, D., Budiu, M., Venkataramani, G.: Programmer specified pointer independence. In: MSP 2004, pp. 51–59. ACM, New York (2004)
Calcagno, C., et al.: Footprint analysis: A shape analysis that discovers preconditions. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, Springer, Heidelberg (2007)
Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119–134. Springer, Heidelberg (2005)
Leino, K.R.M., Logozzo, F.: Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain. Technical Report RISC-Linz Report Series No. 07-07, RISC, Hagenberg, Austria, Proc. WING 2007 (2007)
Tiwari, A., Gulwani, S.: Logical interpretation: Static program analysis using theorem proving. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 147–166. Springer, Heidelberg (2007)
Wagner, D., et al.: A first step towards automated detection of buffer overrun vulnerabilities. In: NDSS Symposium, San Diego, CA, pp. 3–17 (2000)
Dor, N., Rodeh, M., Sagiv, M.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: Proc. PLDI 2003, pp. 155–167. ACM Press, New York (2003)
Allamigeon, X., Godard, W., Hymans, C.: Static analysis of string manipulations in critical embedded C programs. In: SAS. LNCS, pp. 35–51. Springer, Heidelberg (2006)
Filliâtre, J.C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004)
Moy, Y., Marché, C.: Inferring local (non-)aliasing and strings for memory safety. In: Heap Analysis and Verification (HAV 2007), Braga, Portugal (2007)
APRON numerical abstract domain library http://apron.cri.ensmp.fr/
Barnett, M., et al.: Boogie: A modular reusable verifier for object-oriented programs. In: FMCO, Springer, Heidelberg (2005)
MINIX 3 Operating System, http://www.minix3.org/
Ku, K., et al.: A buffer overflow benchmark for software model checkers. In: Proc. ASE (2007)
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proc. POPL 2007, pp. 97–108. ACM Press, New York (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moy, Y. (2008). Sufficient Preconditions for Modular Assertion Checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2008. Lecture Notes in Computer Science, vol 4905. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78163-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-78163-9_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78162-2
Online ISBN: 978-3-540-78163-9
eBook Packages: Computer ScienceComputer Science (R0)