×

zbMATH — the first resource for mathematics

An integrated approach to high integrity software verification. (English) Zbl 1107.68032
Summary: Using automated reasoning techniques, we tackle the niche activity of proving that a program is free from run-time exceptions. Such a property is particularly valuable in high integrity software, for example, safety- or security-critical applications. The context for our work is the SPARK Approach for the development of high integrity software. The SPARK Approach provides a significant degree of automation in proving exception freedom. Where this automation fails, however, the programmer is burdened with the task of interactively constructing a proof and possibly also having to supply auxiliary program annotations. We minimize this burden by increasing the automation, through an integration of proof planning and a program analysis oracle. We advocate a ‘cooperative’ integration, where proof-failure analysis directly constrains the search for auxiliary program annotations. The approach has been successfully tested on industrial data.
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ball, T., Rajamani, S.: The SLAM project: Debugging system software via static analysis. In: Conference Record of POPL’02: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1–3. Portland, Oregon (2002)
[2] Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston, Massachusetts (2003)
[3] Basin, D., Walsh, T.: A calculus for and termination of rippling. J. Autom. Reason. 16(1–2), 147–180 (1996) · Zbl 0847.68105 · doi:10.1007/BF00244462
[4] Baudin, P., Pacalet, A., Raguideau, J., Schoen, D., Williams, N.: CAVEAT: A tool for software validation. In: International Conference on Dependable Systems and Networks (DSN02). IEEE Computer Society (2002)
[5] Bergeretti, J.-F., Carré, B.A.: Information-flow and data-flow analysis of while-programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 7(1), 37–61 (1985) · Zbl 0559.68014 · doi:10.1145/2363.2366
[6] Fischer, B., Schumann, J.: Autobayes: A system for generating data analysis programs from statistical models. J. Funct. Program. 13(3), 483–508 (2003) · Zbl 1037.68044 · doi:10.1017/S0956796802004562
[7] Boyer, R.S., Moore, JS.: A Computational Logic Handbook. Perspectives in Computing, Vol. 23. Academic, Boston, Massachusetts (1988) · Zbl 0655.68117
[8] Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, R., Overbeek, R. (eds.) 9th International Conference on Automated Deduction, pp. 111–120 (1988). Longer version available from Edinburgh as DAI Research Paper No. 349
[9] Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge, England (2005) · Zbl 1095.68108
[10] Bundy, A., Smaill, A., Hesketh, J.: Turning Eureka steps into calculations in automatic program synthesis. In: Clarke, S.L. (ed.) Proc. UK IT 90, pp. 221–226 (1990a). Also available from Edinburgh as DAI Research Paper 448
[11] Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence 62, 185–253 (1993). Also available from Edinburgh as DAI Research Paper No. 567 · Zbl 0789.68121 · doi:10.1016/0004-3702(93)90079-Q
[12] Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. J. Autom. Reason. 7, 303–324 (1991). Earlier version available from Edinburgh as DAI Research Paper No 413 · Zbl 0733.68069 · doi:10.1007/BF00249016
[13] Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster–Clam system. In: Stickel, M.E. (ed.) 10th International Conference on Automated Deduction, Vol. 449 of Lecture Notes in Artificial Intelligence, pp. 647–648. Springer (1990). Also available from Edinburgh as DAI Research Paper 507
[14] Caplain, M.: Finding invariant assertions for proving programs. In: Proceedings of International Conference on Reliable Software. Los Angeles, California (1975)
[15] Chapman, R., Amey, P.: Industrial Strength Exception Freedom. In: Proc. ACM SigAda (2002)
[16] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL-4 (1977a) · Zbl 1149.68389
[17] Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: Mathematical foundations. In: ACM Symposium on Artificial Intelligence & Programming Languages, pp. 1–12 (1977b) · Zbl 0586.68019
[18] Cowan, C., Wagle, P., Pu, C., Beattie, S., Walpole, J.: Buffer overflows: Attacks and defenses for the vulnerability of the decade. In: DARPA Information Survivability Conference and Expo (DISCEX) (2000)
[19] Ellis, B., Ireland, A.: Automation for exception freedom proofs. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, pp. 343–346. IEEE Computer Society (2003). Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0010
[20] Ellis, B., Ireland, A.: An integration of program analysis and automated theorem proving. In: Boiten, E., Derrick, J., Smith, G. (eds.) Proceedings of the 4th International Conference on Integrated Formal Methods (IFM-04), Vol. 2999 of Lecture Notes in Computer Science, pp. 67–86 (2004). Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0014
[21] Elspas, D., Green, M., Levitt, K., Waldinger, R.: Research in Interactive Program-Proving Techniques. In: SRI, Menlo Park, California (1972) · Zbl 0266.68010
[22] ESA: Ariane 5 – Flight 501 Failure. Board of Inquiry Report, European Space Agency (1996)
[23] Filliâtre, J.-C., S. Owre, H. Rueß, and N. Shankar: ICS: Integrated Canonizer and Solver. In: Proc. CAV 2001 (2001) · Zbl 0996.68559
[24] Flanagan, C., Leino, K.R.M.: Houdini, an Annotation Assistant for ESC/Java. In: Proceedings FME 2001 (2001) · Zbl 0977.68671
[25] Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended Static Checking for Java. In: Proceedings PLDI (2002)
[26] Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19, pp. 19–32. American Mathematical Society, Providence, Rhode Island (1967) · Zbl 0189.50204
[27] German, S.: Automating proof of the absence of common runtime errors. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Conference on Principles of Programming Languages (1978)
[28] Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12, 576–583 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[29] Ireland, A.: The use of planning critics in mechanizing inductive proofs. In: Voronkov, A. (ed.) International Conference on Logic Programming and Automated Reasoning (LPAR’92), pp. 178–189. St. Petersburg (1992). Also available from Edinburgh as DAI Research Paper 592
[30] Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J. Autom. Reason. 16(1–2), 79–111 (1996). Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh · Zbl 0847.68103 · doi:10.1007/BF00244460
[31] Ireland, A., Bundy, A.: Automatic verification of functions with accumulating parameters. J. Funct. Program.: Special Issue on Theorem Proving & Functional Programming 9(2), 225–245 (1999). A longer version is available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM/97/11 · Zbl 0940.68023
[32] Ireland, A., Ellis, B., Cook, A., Chapman, R., Barnes, J.: An Integrated Approach to High Integrity Software Development (2006). Available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0027
[33] Ireland, A., Ellis, B., Ingulfsen, T.: Invariant patterns for program reasoning. In: Monroy, R., Arroyo-Figueroa, G., Sucar, L., Sossa, H. (eds.) Proceedings of the 3rd Mexican International Conference on Artificial Intelligence (MICAI-04), Vol. 2972 of Lecture Notes in Artificial Intelligence, pp. 190–201 (2004). Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0011
[34] Ireland, A., Stark, J.: On the automatic discovery of loop invariants. In: Proceedings of the Fourth NASA Langley Formal Methods Workshop – NASA Conference Publication 3356 (1997). Also available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM/97/1
[35] Ireland, A., Stark, J.: Proof planning for strategy development. Ann. Math. and Artif. Intell. 29(1–4), 65–97 (2001). An earlier version is available as Research Memo RM/00/3, Dept. of Computing and Electrical Engineering, Heriot-Watt University · Zbl 1001.68126 · doi:10.1023/A:1018969728171
[36] Ireland, A., Stark, J.: Combining proof plans with partial order planning for imperative program synthesis. J. Autom. Softw. Eng. 13(1), 65–105 (2005). An earlier version is available from the School of Mathematical and Computer Sciences, Heriot-Watt University, Technical Report HW-MACS-TR-0026 · doi:10.1007/s10515-006-5467-3
[37] ISO: Reference Manual for the Ada Programming Language. ISO/IEC 8652, International Standards Organization (1995)
[38] Janičić, P., Bundy, A.: A general setting for flexibly combining and augmenting decision procedures. J. Autom. Reason. 28(3), 257–305 (2002) · Zbl 1003.03012 · doi:10.1023/A:1015707001763
[39] Katz, S., Manna, Z.: Logical analysis of programs. Commun. ACM 19(4), 188–206 (1976) · Zbl 0353.68016 · doi:10.1145/360032.360048
[40] King, S., Hammond, J., Chapman, R., Pryor, A.: Is proof more cost effective than testing? IEEE Trans. SE 26(8), 675–686 (2000)
[41] Kraan, I., Basin, D., Bundy, A.: Middle-out reasoning for logic program synthesis. In: Warren, D.S. (ed.) Proceedings of the 10th International Conference on Logic Programming (1993). Also available as Max-Planck-Institut für Informatik Report MPI-I-93-214 and Edinburgh DAI Research Report 638 · Zbl 0847.68104
[42] MoD: Hazard analysis and safety classification of the computer and programmable electronic system elements of defence equipment. Interim Defence Standard 00-56, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK (1991a)
[43] MoD: The procurement of safety critical software in defence equipment (Part 1: Requirements, Part 2: Guidance). Interim Defence Standard 00-55, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK (1991b)
[44] Monroy, R., Bundy, A., Ireland, A.: Proof plans for the correction of false conjectures. In: Pfenning, F. (ed.) 5th International Conference on Logic Programming and Automated Reasoning, LPAR’94, pp. 54–68. Kiev, Ukraine (1994). Also available from Edinburgh as DAI Research Paper 681
[45] (NCSP), N. C. S.P.: Improving Security across the Software Development Lifecycle. http://www.cyberpartnership.org (2004)
[46] Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, New York (1999) · Zbl 0932.68013
[47] Polyspace, PolySpace-Technologies. http://www.polyspace.com/
[48] PURRS, PURRS: The Parma University’s Recurrence Relation Solver. http://www.cs.unipr.it/purrs/
[49] Seo, S., Yang, H., Yi, K.: Automatic construction of hoare proofs from abstract interpretation results. In: Ohori, A. (ed.) Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27–29, 2003, Proceedings, Vol. 2895 of Lecture Notes in Computer Science, pp. 230–245 (2003) · Zbl 1254.68088
[50] Stark, J., Ireland, A.: Invariant discovery via failed proof attempts. In: Flener, P. (ed.) Logic-Based Program Synthesis and Transformation, Vol. 1559 of Lecture Notes in Computer Science, pp. 271-288. Springer (1998). An earlier version is available from the Dept. of Computing and Electrical Engineering, Heriot-Watt University, Berlin, Research Memo RM/98/2
[51] Visser, E.: Stratego: A Language for Program Transformation based on Rewriting Strategies. System Description of Stratego 0.5. In: Rewriting Techniques and Applications (RTA) (2001) · Zbl 0981.68679
[52] Whiting, L., Hill, M.: Safety analysis of hawk in flight monitor. In: Workshop on Program Analysis For Software Tools and Engineering (1999)
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.