A type system for resource protocol verification and its correctness proof

ABSTRACT

We present a new method, based on a form of dependent typing, to verify the correct usage of resources in a program. Our approach allows complex resources to be specified, whose properties are captured by annotated types and conditions on invariance and final states. The protocol itself is specified through a set of pre-defined methods, whose pre-condition and post-condition together, enforce the correct temporal usage of each resource type. We design a simple language together with a type system that shows how resource protocol verification can be achieved. We formalise an operational semantics for the language and provide a correctness proof which confirms that well-typed programs conform to the specified protocol of each resource type.

REFERENCES

• 1: Martín Abadi and Bruno Blanchet. Computer-Assisted Verification of a Protocol for Certified Email. In Radhia Cousot, editor, Proceedings of the International Static Analysis Symposium (SAS), volume 2694 of Lecture Notes on Computer Science, pages 316--335, San Diego, California, June 2003. Springer Verlag.
• 2: 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
• 3: Hugh Anderson and Siau-Cheng Khoo. Affine-based size-change termination. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS), June 2003.
• 4: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 5: Edwin C. Chan , John T. Boyland , William L. Scherlis, Promises: limited specifications for analysis and manipulation, Proceedings of the 20th international conference on Software engineering, p.167-176, April 19-25, 1998, Kyoto, Japan
• 6: Wei-Ngan Chin , Siau-Cheng Khoo, Calculating sized types, Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.62-72, January 22-23, 2000, Boston, Massachusetts, United States
• 7: W.N. Chin, S.C. Khoo, and S.C. Qin. A Sized Type System for Objects with Alias Controls. Technical report, SoC, Natl Univ. of Singapore, January 2004. avail. at http://www.comp.nus.edu.sg/~qinsc/papers/sizedtype.ps.gz.
• 8: Wei-Ngan Chin , Siau-Cheng Khoo , Dana N. Xu, Deriving Pre-conditions for Array Bound Check Elimination, Proceedings of the Second Symposium on Programs as Data Objects, p.2-24, May 21-23, 2001
• 9: Thomas Colcombet , Pascal Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325703]
• 10: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 11: 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
• 12: Amy P. Felty , Douglas J. Howe , Frank A. Stomp, Protocol Verification in Nuprl, Proceedings of the 10th International Conference on Computer Aided Verification, p.428-439, June 28-July 02, 1998
• 13: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 14: Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Software verification with Blast. In Proceedings of the Tenth International Workshop on Model Checking of Software (SPIN), pages 235--239. Lecture Notes in Computer Science 2648, Springer-Verlag, 2003.
• 15: Martin Hofmann, The strength of non-size increasing computation, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.260-269, January 16-18, 2002, Portland, Oregon
• 16: John Hughes , Lars Pareto, Recursion and dynamic data-structures in bounded space: towards embedded ML programming, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.70-81, September 27-29, 1999, Paris, France
• 17: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 18: Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.331-342, January 16-18, 2002, Portland, Oregon
• 19: Naoki Kobayashi. Time regions and effects for resource usage analysis. Technical report, Tokyo Inst. of technology, 2003.
• 20: Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.213-225, August 25-29, 2003, Uppsala, Sweden
• 21: Kim Marriott, Peter Stuckey, and Martin Sulzmann. Resource usage verification. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS), Beijing, China, November 2003.
• 22: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 23: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 24: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 25: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, 1998
• 26: Hongwei Xi, Imperative Programming with Dependent Types, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.375, June 26-29, 2000
• 27: Hongwei Xi, Dependent Types for Program Termination Verification, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.231, June 16-19, 2001
• 28: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Theory, Verification

Keywords:
correctness proof, dependent type system, path-sensitive analysis, protocol verification, resource specification