Enhancing spark's contract checking facilities using symbolic execution

ABSTRACT

Spark, a subset of Ada for engineering safety and security-critical systems, is one of the best commercially available frameworks for formal-methods-supported development of critical software. Spark is designed for verification and includes a software contract language for specifying functional properties of procedures. Even though Spark and its static analysis components are beneficial and easy to use, its contract language is rarely used for stating properties beyond simple constraints on scalar values due to the burdens the associated tool support imposes on developers. Symbolic execution (SymExe) techniques have made significant strides in automating reasoning about deep semantic properties of source code. However, most work on SymExe has focused on bug-finding and test case generation as opposed to tasks that are more verification-oriented such as contract checking. In previous work we have presented: (a) SymExe techniques for checking software contracts in embedded critical systems, and (b) Bakar Kiasan, a tool that implements these techniques in an integrated development environment for Spark. In this paper, we give a detailed walk-through of Bakar Kiasan as it is applied to an industrial code base for an embedded security device. We illustrate how Bakar Kiasan provides significant increases in automation, usability, and functionality over existing Spark contract checking tools, and we present results from performance evaluations of its application to industrial examples.

References

1. T. Amtoft, J. Hatcliff, E. Rodrıguez, Robby, J. Hoag, and D. Greve. Specification and checking of software contracts for conditional information flow. In 15th International Symposium on Formal Methods (FM), pages 229--245. Springer, 2008.
2. J. Barnes. High Integrity Software -- the SPARK Approach to Safety and Security. Addison-Wesley, 2003.
3. C. Barrett and C. Tinelli. CVC3. In 19th International Conference on Computer Aided Verification (CAV), volume 4590 of Lecture Notes in Computer Science, pages 298--302. Springer, 2007.
4. J. Belt, J. Hatcliff, Robby, P. Chalin, D. Hardin, and X. Deng. Bakar kiasan: Flexible contract checking for critical systems using symbolic execution. In NASA Formal Methods, volume 6617 of Lecture Notes in Computer Science, pages 58--72. Springer, 2011.
5. J. Belt, Robby, and X. Deng. Sireum/Topi LDP: A lightweight semi-decision procedure for optimizing symbolic execution-based analyses. In Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 355--364, 2009.
6. C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 209--224. USENIX Association, 2008.
7. B.-Y. E. Chang and K. R. M. Leino. Inferring object invariants: Extended abstract. Electr. Notes Theor. Comput. Sci., 131:63--74, 2005.
8. AdaCore/SofCheck CodePeer tool set. http://www.adacore.com/home/products/codepeer/toolset/.
9. The Coq proof assistant. http://coq.inria.fr/.
10. L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pages 337--340. Springer, 2008.
11. X. Deng, J. Lee, and Robby. Efficient symbolic execution algorithms for programs manipulating dynamic heap objects. Technical Report SAnToS-TR2009-09--25, Kansas State University, September 2009.
12. X. Deng, R. Walker, and Robby. Program behavioral benchmarks for evaluating path-sensitive bounded verification techniques. Technical Report SAnToS-TR2010-08--20, Kansas State University, 2010.
13. B. Dutertre and L. de Moura. The Yices SMT solver. Tool paper at http://yices.csl.sri.com/tool-paper.pdf, August 2006.
14. J. C. Filliâtre and C. Marché. The why/krakatoa/caduceus platform for deductive program verification. In Proceedings of the 19th international conference on Computer aided verification, CAV'07, pages 173--177, Berlin, Heidelberg, 2007. Springer-Verlag.
15. Frama-C website. http://frama-c.com/.
16. P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI), pages 213--223. ACM Press, 2005.
17. W. Grieskamp, N. Tillmann, and W. Schulte. XRT--exploring runtime for .NET: Architecture and applications. Workshop on Software Model Checking, 2005.
18. S. L. Hantler and J. C. King. An introduction to proving the correctness of programs. ACM Computing Surveys (CSUR), 8(3):331--353, September 1976.
19. The AdaCore Hi-Lite project. http://www.open-do.org/projects/hi-lite/.
20. D. Jackson. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM), 11(2):256 -- 290, apr 2002.
21. P. Jackson and G. Passmore. Proving SPARK verification conditions with SMT solvers, 2009. Draft journal article. http://homepages.inf.ed.ac.uk/pbj/papers/vct-dec09-draft.pdf.
22. S. Khurshid, C. S. P\uas\uareanu, and W. Visser. Generalized symbolic execution for model checking and testing. Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 553--568, 2003.
23. J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976.
24. D. Kroening and O. Strichman. Decision Procedures -- An Algorithmic Point of View. Springer, 2008.
25. K. R. M. Leino and F. Logozzo. Loop invariants on demand. In K. Yi, editor, APLAS, volume 3780 of Lecture Notes in Computer Science, pages 119--134. Springer, 2005.
26. B. Rossebo, P. Oman, J. Alves-Foss, R. Blue, and P. Jaszkowiak. Using SPARK-Ada to model and verify a MILS message router. In Proceedings of the International Symposium on Secure Software Engineering, 2006.
27. J. Rushby. The design and verification of secure systems. In 8th ACM Symposium on Operating Systems Principles, volume 15(5), pages 12--21, 1981.
28. K. Sen and G. Agha. CUTE: A concolic unit testing engine for C. In ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pages 263--272, 2005.
29. N. Tillmann and J. de Halleux. Pex--white box test generation for .NET. In 2nd International Conference on Tests and Proofs (TAP), volume 4966 of Lecture Notes in Computer Science, pages 134--153. Springer, 2008.
30. Victor website. http://homepages.inf.ed.ac.uk/pbj/spark/victor.html.

Index Terms

• Computing methodologies

  • Symbolic and algebraic manipulation

• General and reference

  • Cross-computing tools and techniques

    • Reliability

    • Validation

• Hardware

  • Hardware validation

    • Functional verification

      • Assertion checking

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Empirical software validation

      • Formal software verification

      • Process validation

  • Software organization and properties

    • Software functional properties

      • Formal methods

• Theory of computation

  • Models of computation

    • Abstract machines

  • Semantics and reasoning

    • Program reasoning

      • Abstraction

      • Assertions