Efficient software model checking of soundness of type systems

ABSTRACT

This paper presents novel techniques for checking the soundness of a type system automatically using a software model checker. Our idea is to systematically generate every type correct intermediate program state (within some finite bounds), execute the program one step forward if possible using its small step operational semantics, and then check that the resulting intermediate program state is also type correct--but do so efficiently by detecting similarities in this search space and pruning away large portions of the search space. Thus, given only a specification of type correctness and the small step operational semantics for a language, our system automatically checks type soundness by checking that the progress and preservation theorems hold for the language (albeit for program states of at most some finite size). Our preliminary experimental results on several languages--including a language of integer and boolean expressions, a simple imperative programming language, an object-oriented language which is a subset of Java, and a language with ownership types--indicate that our approach is feasible and that our search space pruning techniques do indeed significantly reduce what is otherwise an extremely large search space. Our paper thus makes contributions both in the area of checking soundness of type systems, and in the area of reducing the state space of a software model checker.

REFERENCES

• 1: Jonathan Aldrich , Valentin Kostadinov , Craig Chambers, Alias annotations for program understanding, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 2: B. E. Aydemir et al. Mechanized metatheory for the masses: The POPLMARK challenge, May 2005. http://www.cis.upenn.edu/ plclub/wiki-static/poplmark.pdf.
• 3: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 4: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 5: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 6: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira, Ownership types for object encapsulation, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-223, January 15-17, 2003, New Orleans, Louisiana, USA
• 7: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira , Chuang-Hue Moh , Steven Richman, Lazy modular upgrades in persistent object stores, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 8: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 9: Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 10: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 11: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 12: James Cheney , Alberto Momigliano, Mechanized metatheory model-checking, Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland [doi>10.1145/1273920.1273931]
• 13: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 14: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 15: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 16: Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of data structure properties, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 17: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 18: Claudio DeMartini , Radu Iosif , Riccardo Sisto, A deadlock detection tool for concurrent Java programs, Software—Practice & Experience, v.29 n.7, p.577-603, June 1999 [doi>10.1002/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V]
• 19: J. Dolby, M. Vaziri, and F. Tip. Checking properties of heap-manipulating procedures using a constraint solver. In European Software Engineering Conference and Foundations of Software Engineering (ESEC/FSE), September 2007.
• 20: S. Drossopoulou and S. Eisenbach. Java is type safe-probably. In European Conference for Object-Oriented Programming (ECOOP), June 1997.
• 21: M. Dwyer, J. Hatcliff, M. Hoosier, and Robby. Building your own software model checker using the Bogor extensible model checking framework. In Computer Aided Verification (CAV), January 2005.
• 22: N. Een and A. Biere. Effective preprocessing in SAT through variable and clause elimination. In Theory and Applications of Satisfiability Testing (SAT), June 2005.
• 23: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 24: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 25: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 26: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 27: W. Grieskamp, N. Tillmann, and W. Shulte. XRT-Exploring runtime for .NET: Architecture and applications. In Workshop on Software Model Checking (SoftMC), July 2005.
• 28: Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 29: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 30: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 31: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 32: Radu Iosif, Symmetry Reduction Criteria for Software Model Checking, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.22-41, April 11-13, 2002
• 33: C. Norris Ip , David L. Dill, Better Verification Through Symmetry, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.97-111, April 26-28, 1993
• 34: Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
• 35: Daniel Jackson , Craig A. Damon, Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector, IEEE Transactions on Software Engineering, v.22 n.7, p.484-495, July 1996 [doi>10.1109/32.538605]
• 36: Sarfraz Khurshid , Darko Marinov, TestEra: Specification-Based Testing of Java Programs Using SAT, Automated Software Engineering, v.11 n.4, p.403-434, October 2004 [doi>10.1023/B:AUSE.0000038938.10589.b9]
• 37: Sarfraz Khurshid , Darko Marinov , Daniel Jackson, An analyzable annotation language, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 38: S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2003.
• 39: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 40: G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University, May 1998.
• 41: D. Marinov, A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard. An evaluation of exhaustive testing for data structures. Technical Report TR-921, MIT Laboratory for Computer Science, September 2003.
• 42: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 43: M. Musuvathi and D. Dill. An incremental heap canonicalization algorithm. In SPIN workshop on Model Checking of Software (SPIN), August 2005.
• 44: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 45: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 46: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 47: Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
• 48: N. Nystrom, M. R. Clarkson, and A. C. Myers. Polyglot: An extensible compiler framework for Java. In Compiler Construction (CC), April 2003.
• 49: J. Offutt and R. Untch. Mutation 2000: Uniting the orthogonal. In Mutation 2000: Mutation Testing in the Twentieth and the Twenty First Centuries, October 2000.
• 50: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 51: Peter Sewell , Francesco Zappa Nardelli , Scott Owens , Gilles Peskine , Thomas Ridge , Susmit Sarkar , Rok Strniša, Ott: effective tool support for the working semanticist, Proceedings of the 12th ACM SIGPLAN international conference on Functional programming, October 01-03, 2007, Freiburg, Germany
• 52: M. Vaziri and D. Jackson. Checking properties of heap-manipulating procedures using a constraint solver. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2003.
• 53: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 54: David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325728]
• 55: Glynn Winskel, The formal semantics of programming languages: an introduction, MIT Press, Cambridge, MA, 1993
• 56: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Reliability, Verification

Keywords:
software model checking, type soundness