×

Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. (English) Zbl 1197.68035

Summary: We introduce Pentagons (Pntg), a weakly relational numerical abstract domain useful for the validation of array accesses in byte-code and intermediate languages. This abstract domain captures properties of the form of \(x \in [a,b] \wedge x < y\). It is more precise than the well known Interval domain, but it is less precise than the Octagon domain.
The goal of Pntg is to be a lightweight numerical domain useful for adaptive static analysis, where Pntg is used to quickly prove the safety of most array accesses, restricting the use of more precise (but also more expensive) domains to only a small fraction of the code.
We implemented the Pntg abstract domain in Clousot, a generic abstract interpreter for .NET assemblies. Using it, we were able to validate 83% of array accesses in the core runtime library mscorlib.dll in a little bit more than 3 minutes.

MSC:

68N15 Theory of programming languages
68N25 Theory of operating systems

Software:

Cibai; ASTREE; CSSV
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Allamigeon, X.; Godard, W.; Hymans, C.: Static analysis of string manipulations in critical embedded C programs, (August 2006) · Zbl 1225.68064
[2] R. Alur, D.L. Dill, Automata for modeling real-time systems, in: ICALP’90, July 1990 · Zbl 0765.68150
[3] Bagnara, R.; Hill, P. M.; Mazzi, E.; Zaffanella, E.: Widening operators for weakly-relational numeric abstractions, (September 2005) · Zbl 1141.68445
[4] F. Banterle, R. Giacobazzi, A fast implementation of the octagon abstract domain on graphics hardware, in: SAS’07, August 2007
[5] M. Barnett, M. Fähndrich, F. Logozzo, Codecontracts for.net. http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx
[6] Blanchet, B.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X.: A static analyzer for large safety-critical software, (June 2003) · Zbl 1026.68514
[7] Bodík, R.; Gupta, R.; Sarkar, V.: ABCD: eliminating array bounds checks on demand, (2000)
[8] Clarisó, R.; Cortadella, J.: The octahedron abstract domain, Sci. comput. Program. 64, No. 1 (2007) · Zbl 1171.68540
[9] Clarke, E. M.; Grumberg, O.; Peled, D. A.: Model checking, (1999) · Zbl 0847.68063
[10] Courbot, A.; Pavlova, M.; Grimaud, G.; Vandewalle, J. -J.: A low-footprint Java-to-native compilation scheme using formal methods, Lncs (April 2006)
[11] Cousot, P.: The calculational design of a generic abstract interpreter, NATO ASI series F (1999) · Zbl 0945.68032
[12] Cousot, P.: Verification by abstract interpretation, (2003) · Zbl 1274.68180
[13] Cousot, P.; Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, (January 1977) · Zbl 1149.68389
[14] Cousot, P.; Halbwachs, N.: Automatic discovery of linear restraints among variables of a program, (January 1978)
[15] Dor, N.; Rodeh, M.; Sagiv, M.: CSSV: towards a realistic tool for statically detecting all buffer overflows in c, (2003)
[16] ECMA. Standard ECMA-335, Common Language Infrastructure (CLI). http://www.ecma-international.org/publications/standards/Ecma-335.htm, Ecma International, 2006
[17] S. Gaubert, E. Goubault, A. Taly, S. Zennou, Static analysis by policy iteration on relational domains, in: ESOP’07, April 2007 · Zbl 1187.68151
[18] Halbwachs, N.; Merchat, D.; Gonnord, L.: Some ways to reduce the space dimension in polyhedra computations, Formal methods in system design 29, No. 1, 79-95 (2006) · Zbl 1105.68107
[19] ECMA Int. Standard ECMA-355, Common Language Infrastructure, June 2006
[20] Karr, M.: On affine relationships among variables of a program, Acta informatica 6, No. 2, 133-151 (1976) · Zbl 0358.68025
[21] Kildall, G. A.: A unified approach to global program optimization, (October 1973) · Zbl 0309.68020
[22] D. Larochelle, D. Evans, Statically detecting likely buffer overflow vulnerabilities, in: 2001 USENIX Security Symposium, August 2001
[23] V. Laviron, F. Logozzo, Subpolyhedra: A (more) scalable approach to infer linear inequalities, in: VMCAI’09, January 2009 · Zbl 1206.68092
[24] Logozzo, F.: Cibai: an abstract interpretation-based static analyzer for modular analysis and verification of Java classes, (January 2007) · Zbl 1132.68329
[25] Logozzo, F.; Fähndrich, M. A.: On the relative completeness of bytecode analysis versus source code analysis, Lncs (March 2008)
[26] Miné, A.: A new numerical abstract domain based on difference-bounds matrices, (May 2001) · Zbl 0984.68034
[27] Miné, A.: The octagon abstract domain, (October 2001) · Zbl 1105.68069
[28] A. Miné, A few graph-based relational numerical abstract domains, in: SAS’02, September 2002
[29] A. Miné, Weakly relational numerical abstract domains, Ph.D. thesis, École Polythechnique, 2004
[30] Navas, J.; Mera, Ed.; López-García, P.; Hermenegildo, M. V.: User-definable resource bounds analysis for logic programs, (September 2007)
[31] C. Popeea, D.N. Xu, W.-N. Chin, A practical and precise inference and specializer for array bound checks elimination, in: PEPM’08, 2008
[32] P.Z. Revesz, The constraint database approach to software verification, in: VMCAI’07, January 2007 · Zbl 1132.68339
[33] S. Sankaranarayanan, F. Ivancic, A. Gupta, Program analysis using symbolic ranges, in: SAS’07, August 2007
[34] S. Sankaranarayanan, H.B. Sipma, Z. Manna, Scalable analysis of linear systems using mathematical programming, in: VMCAI’05, January 2005, pp. 25–41 · Zbl 1111.68514
[35] Simon, A.; King, A.; Howe, J. M.: Two variables per linear inequality as an abstract domain, (2002) · Zbl 1278.68072
[36] Venet, A.: Nonuniform alias analysis of recursive data structures and arrays, (September 2002) · Zbl 1015.68513
[37] Venet, A.; Brat, G. P.: Precise and efficient static array bound checking for large embedded c programs, (July 2004)
[38] Xi, H.; Pfenning, F.: Eliminating array bound checking through dependent types, (1998)
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.