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.
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.) |
Keywords:
specification languages; functional behavior; contracts; inference; abstract interpretation; weakest precondition; quantifier eliminationReferences:
| [1] | Aiken, A.; Foster, J. S.; Kodumal, J.; Terauchi, T., Checking and inferring local non-aliasing, (PLDI ’03: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (2003), ACM: ACM New York, NY, USA), 129-140 |
| [3] | Barnett, M.; Leino, K. R.M.; Schulte, W., The Spec# Programming System: An Overview, (Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS’04. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS’04, Lecture Notes in Computer Science, vol. 3362 (2004), Springer), 49-69 |
| [5] | Bourdoncle, F., Assertion-based debugging of imperative programs by abstract interpretation, (ESEC ’93: Proceedings of the 4th European Software Engineering Conference on Software Engineering (1993), Springer-Verlag: Springer-Verlag London, UK), 501-516 |
| [6] | Bradley, A. R.; Manna, Z., The Calculus of Computation: Decision Procedures with Applications to Verification (2007), Springer-Verlag New York, Inc.: 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, (Proceedings of the 14th International Static Analysis Symposium. Proceedings of the 14th International Static Analysis Symposium, Lecture Notes in Computer Science, vol. 4634 (2007), Springer-Verlag), 402-418 |
| [11] | Colon, M.; Sankaranarayanan, S.; Sipma, H., Linear invariant generation using non-linear constraint solving, (Proc. of the Int. Conf. on Computer Aided Verification, CAV. Proc. of the Int. Conf. on Computer Aided Verification, CAV, Lecture Notes in Computer Science, vol. 2725 (2003)), 420-432 · Zbl 1278.68164 |
| [14] | Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (POPL’79: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (1979), ACM: ACM New York, NY, USA), 269-282 · Zbl 0788.68094 |
| [15] | Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (POPL’78: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (1978), ACM: ACM New York, NY, USA), 84-96 |
| [16] | Dahlweid, M.; Moskal, M.; Santen, T.; Tobies, S.; Schulte, W., VCC: Contract-based modular verification of concurrent C, (31st International Conference on Software Engineering. 31st International Conference on Software Engineering, ICSE 2009, May 16-24, Vancouver, Canada (2009), Companion Volume. IEEE), 429-430 |
| [17] | Dijkstra, E. W., (A Discipline of Programming. A Discipline of Programming, Series in Automatic Computation (1976), Prentice Hall Int) · Zbl 0368.68005 |
| [18] | Dill, D. L., Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits (1989), MIT Press: 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, (Damm, W.; Hermanns, H., 19th International Conference on Computer Aided Verification. 19th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 4590 (2007), Springer: Springer Berlin, Germany), 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, (FME’01: Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity (2001), Springer-Verlag: Springer-Verlag London, UK), 500-517 · Zbl 0977.68671 |
| [22] | Gulwani, S.; Tiwari, A., Combining abstract interpreters, (Annual ACM Conference on Programming Language Design and Implementation (2006), ACM) |
| [23] | Gulwani, S.; Tiwari, A., Assertion checking unified, (The 8th International Conference on Verification, Model Checking and Abstract Interpretation (2007), Springer), 363-377 · Zbl 1132.68470 |
| [24] | Hackett, B.; Das, M.; Wang, D.; Yang, Z., Modular checking for buffer overflows in the large, (ICSE’06: Proceedings of the 28th International Conference on Software Engineering (2006), ACM: ACM New York, NY, USA), 232-241 |
| [29] | Jim, T.; Morrisett, J. G.; Grossman, D.; Hicks, M. W.; Cheney, J.; Wang, Y., Cyclone: A safe dialect of C, (Proc. 2002 USENIX Annual Technical Conference (2002), Berkeley: Berkeley CA, USA), 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: Prentice-Hall Englewood Cliffs, New Jersey |
| [32] | Koes, D.; Budiu, M.; Venkataramani, G., Programmer specified pointer independence, (MSP’04: Proceedings of the 2004 Workshop on Memory System Performance (2004), ACM: ACM New York, NY, USA), 51-59 |
| [33] | Ku, K.; Hart, T. E.; Chechik, M.; Lie, D., A buffer overflow benchmark for software model checkers, (ASE’07: Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering (2007), ACM: ACM New York, NY, USA), 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, (APLAS’05: Proceedings of The 3rd ASIAN Symposium on Programming Languages and Systems. APLAS’05: Proceedings of The 3rd ASIAN Symposium on Programming Languages and Systems, LNCS (2005), Springer-Verlag), 119-134 · Zbl 1159.68374 |
| [37] | Leino, K. R.M.; Saxe, J. B.; Stata, R., Checking Java programs via guarded commands, (Proceedings of the Workshop on Object-Oriented Technology (1999), Springer-Verlag: Springer-Verlag London, UK), 110-111 |
| [38] | Liang, D.; Harrold, M. J., Efficient computation of parameterized pointer information for interprocedural analyses, (SAS’01: Proceedings of the 8th International Symposium on Static Analysis (2001), Springer-Verlag: Springer-Verlag London, UK), 279-298 · Zbl 1005.68898 |
| [39] | Marché, C., Jessie: an intermediate language for Java and C verification, (Programming Languages meets Program Verification (PLPV) (2007), ACM: ACM Freiburg, Germany), 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 |
| [44] | Popeea, C.; Xu, D. N.; Chin, W.-N., A practical and precise inference and specializer for array bound checks elimination, (PEPM’08: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (2008), ACM: ACM New York, NY, USA), 177-187 |
| [45] | Reynolds, J. C., Syntactic control of interference, (POPL’78: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (1978), ACM: ACM New York, NY, USA), 39-46 |
| [46] | Rival, X., Understanding the origin of alarms in astrée, (12th Static Analysis Symposium. 12th Static Analysis Symposium, SAS’05. 12th Static Analysis Symposium. 12th Static Analysis Symposium, SAS’05, LNCS, vol. 3672 (2005), Springer-Verlag: Springer-Verlag London, UK), 303-319 · Zbl 1141.68376 |
| [49] | Steensgaard, B., Points-to analysis in almost linear time, (POPL’96: Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1996), ACM: ACM New York, NY, USA), 32-41 |
| [50] | Suzuki, N.; Ishihata, K., Implementation of an array bound checker, (POPL’77: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (1977), ACM: ACM New York, NY, USA), 132-143 |
| [52] | Talpin, J.-P.; Jouvelot, P., The type and effect discipline, (Seventh Annual IEEE Symposium on Logic in Computer Science. Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California (1992), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, California), 162-173 |
| [54] | Weispfenning, V., Complexity and uniformity of elimination in presburger arithmetic, (ISSAC’97: Proceedings of the 1997 International Symposium on Symbolic and Algebraic computation (1997), ACM: ACM New York, NY, USA), 48-53 · Zbl 0915.03032 |
| [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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
