Verification of safety properties for concurrent assembly code

ABSTRACT

Concurrency, as a useful feature of many modern programming languages and systems, is generally hard to reason about. Although existing work has explored the verification of concurrent programs using high-level languages and calculi, the verification of concurrent assembly code remains an open problem, largely due to the lack of abstraction at a low-level. Nevertheless, it is sometimes necessary to reason about assembly code or machine executables so as to achieve higher assurance.In this paper, we propose a logic-based "type" system for the static verification of concurrent assembly programs, applying the "invariance proof" technique for verifying general safety properties and the "assume-guarantee" paradigm for decomposition. In particular, we introduce a notion of "local guarantee" for the thread-modular verification in a non-preemptive setting.Our system is fully mechanized. Its soundness has been verified using the Coq proof assistant. A safety proof of a program is semi-automatically constructed with help of Coq, allowing the verification of even undecidable safety properties. We demonstrate the usage of our system using three examples, addressing mutual exclusion, deadlock freedom, and partial correctness respectively.

References

1. M. Abadi and L. Lamport. Composing specifications. ACM Trans. on Programming Languages and Systems, 15(1):73--132, 1993.
2. M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. on Programming Languages and Systems, 17(3):507--535, 1995.
3. A. Ahmed and D. Walker. The logical approach to stack typing. In Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, pages 74--85. ACM Press, 2003.
4. A. W. Appel. Foundational proof-carrying code. In Proc. 16th Annual IEEE Symposium on Logic in Computer Science, pages 247--258. IEEE Computer Society, June 2001.
5. A. Cau and P. Collette. Parallel composition of assumption-commitment specifications. Acta Informatica, 33(2):153--176, 1996.
6. B.-Y. E. Chang, G. C. Necular, and R. R. Schneck. Extensible code verification. Unpublished manuscript, 2003.
7. E. M. Clarke. Programming language constructs for which it is impossible to obtain good Hoare axiom systems. In Journal of the Association for Computing Machinery, pages 129--147, Jan. 1979.
8. E. M. Clarke. The characterization problem for Hoare logics. In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 89--106. Prentice Hall, 1985.
9. W.-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge, UK, 2001.
10. E. W. Dijsktra. Cooperating sequential processes. In F. Genuys, editor, Programming Languages, pages 43--112. Academic Press, 1968.
11. C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In Proc. 2002 European Symposium on Programming, pages 262--277. Springer-Verlag, 2002.
12. R. W. Floyd. Assigning meanings to programs. In A. M. Society, editor, Proceedings of the Symposium on Applied Math. Vol. 19, pages 19--31, Providence, R.I., 1967.
13. N. Francez and A. Pnueli. A proof method for cyclic programs. Acta Informatica, 9:133--157, 1978.
14. N. Glew and G. Morrisett. Type-safe linking and modular assembly language. In Proc. 26th ACM Symp. on Principles of Prog. Lang., pages 250--261. ACM Press, Jan. 1999.
15. N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof-carrying code. In Proc. Seventeenth Annual IEEE Symposium on Logic In Computer Science (LICS'02), pages 89--100. IEEE Computer Society, July 2002.
16. T. A. Henzinger, S. Qadeer, S. K. Rajamani, and S. Tasiran. An assume-guarantee rule for checking simulation. In Formal Methods in Computer-Aided Design, pages 421--432, 1998.
17. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580, Oct. 1969.
18. C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39--45, Jan. 1971.
19. C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666--677, 1978.
20. T. Hoare. The verifying compiler: A grand challenge for computing research. In Proc. 2003 International Conference on Compiler Construction (CC'03), LNCS Vol. 2622, pages 262--272, Warsaw, Poland, Apr. 2003. Springer-Verlag Heidelberg.
21. J. Hooman, W.-P. de Roever, P. Pandya, Q. Xu, P. Zhou, and H. Schepers. A compositional approach to concurrency and its applications. Incomplete manuscript. http://www.informatik.uni-kiel.de/inf/deRoever/books/, Apr. 2003.
22. W. A. Howard. The formulae-as-types notion of constructions. In To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, 1980.
23. C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems, 5(4):596--619, 1983.
24. L. Lamport. The temporal logic of actions. ACM Trans. on Programming Languages and Systems, 16(3):872--923, May 1994.
25. L. Lamport and F. B. Schneider. The "Hoare logic" of CSP, and all that. ACM Trans. on Programming Languages and Systems, 6(2):281--296, Apr. 1984.
26. R. Milner. A Calculus of Communicating Systems. Springer-Verlag New York, Inc., 1982.
27. J. Misra and K. M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(7):417--426, 1981.
28. G. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Prog. Lang., pages 106--119, New York, Jan. 1997. ACM Press.
29. G. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proc. 2nd USENIX Symp. on Operating System Design and Impl., pages 229--243, 1996.
30. G. C. Necula and R. R. Schneck. A sound framework for untrustred verification-condition generators. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 248--260. IEEE Computer Society, July 2003.
31. P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In Proc. 29th ACM Symp. on Principles of Prog. Lang., pages 268--280, Venice, Italy, Jan. 2004. ACM Press.
32. M. Ossefort. Correctness proofs of communicating processes: Three illustrative examples from the literature. ACM Trans. on Programming Languages and Systems, 5(4):620--640, Oct. 1983.
33. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319--340, 1976.
34. S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. on Programming Languages and Systems, 4(3):455--495, July 1982.
35. C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In M. Bezem and J. Groote, editors, Proc. TLCA, volume 664 of LNCS. Springer-Verlag, 1993.
36. A. Pnueli. In transition from global to modular temporal reasoning about programs. Logics and models of concurrent systems, pages 123--144, 1985.
37. J. H. Reppy. CML: A higher concurrent language. In Proc. 1991 Conference on Programming Language Design and Implementation, pages 293--305, Toronto, Ontario, Canada, 1991. ACM Press.
38. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings Seventeenth Annual IEEE Symposium on Logic in Computer Science, pages 55--74, Los Alamitos, California, July 2002. IEEE Computer Society.
39. Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for certified binaries. In Proc. 29th ACM Symp. on Principles of Prog. Lang., pages 217--232, Portland, OR, Jan. 2002. ACM Press.
40. E. W. Stark. A proof technique for rely/guarantee properties. In S. N. Maheshwari, editor, Proc. 5th Conference on Foundations of Software Technology and Theoretical Computer Science, volume 206 of LNCS, pages 369--391, New Delhi, 1985. Springer-Verlag.
41. C. Stirling. A generalization of Owicki-Gries's Hoare logic for a concurrent while language. Theoretical Computer Science, 58(1-3):347--359, 1988.
42. The Coq Development Team. The Coq proof assistant reference manual. The Coq release v7.1, Oct. 2001.
43. The FLINT Project. Coq (v7.3.1) implementation for CCAP language, soundness and examples. http://flint.cs.yale.edu/flint/publications/vsca.html (17k), Mar. 2004.
44. A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.
45. Q. Xu, A. Cau, and P. Collette. On unifying assumption-commitment style proof rules for concurrency. In International Conference on Concurrency Theory, pages 267--282, 1994.
46. D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for PCC:Dynamic storage allocation. In Proc. 2003 European Symposium on Programming, LNCS Vol. 2618, pages 363--379, Warsaw, Poland, Apr. 2003. Springer-Verlag.
47. D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 50(1-3):101--127, 2004.
48. Y. Yu. Automated proofs of object code for a widely used microprocessor. PhD thesis, University of Texas at Austin, Austin, TX, 1992.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • Formal language definitions

  • Software organization and properties

    • Software functional properties

      • Correctness

      • Formal methods

• Theory of computation

  • Formal languages and automata theory

  • Logic

    • Proof theory

  • Semantics and reasoning

    • Program reasoning

      • Assertions

      • Invariants

      • Program verification