Advertisement

Temporal Logic for Proof-Carrying Code

  • Andrew Bernard
  • Peter Lee
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

Proof-carrying code (PCC) is a framework for ensuring that untrusted programs are safe to install and execute. When using PCC, untrusted programs are required to contain a proof that allows the program text to be checked efficiently for safe behavior. In this paper, we lay the foundation for a potential engineering improvement to PCC. Specifically, we present a practical approach to using temporal logic to specify security policies in such a way that a PCC system can enforce them.

Keywords

Proof-carrying code temporal logic 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 243–253, Boston, MA, January 2000.Google Scholar
  2. 2.
    Andrew Bernard and Peter Lee. Temporal logic for proof-carrying code. Technical Report CMU-CS-02-130, Carnegie Mellon University, School of Computer Science, 2002. In preparation.Google Scholar
  3. 3.
    Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A certifying compiler for Java. In Proceedings of the ACM SIG-PLAN’ 00 conference on programming language design and implementation, pages 95–107, Vancouver, BC Canada, June 2000.Google Scholar
  4. 4.
    Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 262–275, San Antonio, TX, January 1999.Google Scholar
  5. 5.
    Karl Crary and Stephnie Weirich. Resource bound certification. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 184–198, Boston, MA, January 2000.Google Scholar
  6. 6.
    Úlfar Erlingsson and Fred B. Schneider. IRM enforcement of Java stack inspection. In RSP: 21th IEEE Computer Society Symposium on Research in Security and Privacy, 2000.Google Scholar
  7. 7.
    Dexter Kozen. Efficient code certification. Technical Report TR98-1661, Cornell University, Computer Science Department, January 1998.Google Scholar
  8. 8.
    Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Verlag, 1991.Google Scholar
  9. 9.
    Neophytos G. Michael and Andrew W. Appel. Machine instruction syntax and semantics in higher order logic. In Proceedings of the 17th International Conference on Automated Deduction (CADE-17), June 2000.Google Scholar
  10. 10.
    Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85–97, San Diego, CA, January 1998.Google Scholar
  11. 11.
    George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106–119, Paris, France, January 1997.Google Scholar
  12. 12.
    George C. Necula and Peter Lee. Safe, untrusted agents using proof-carrying code. In Mobile Agents and Security, volume 1419 of Lecture Notes in Computer Science. Springer Verlag, 1998.CrossRefGoogle Scholar
  13. 13.
    George C. Necula and S. P. Rahul. Oracle-based checking of untrusted software. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 142–154, London, UK, January 2001.Google Scholar
  14. 14.
    George Ciprian Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, September 1998. Available as Technical Report CMU-CS-98-154.Google Scholar
  15. 15.
    Frank Pfenning and Carsten Schürmann. System description: Twelf — A meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202–206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.Google Scholar
  16. 16.
    Fred B. Schneider. Enforceable security policies. Technical Report TR99-1759, Cornell University, Computer Science Department, July 1999.Google Scholar
  17. 17.
    Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. Efficient software-based fault isolation. In Proceedings of the Fourteenth ACM Symposium on Operating Systems Principles, pages 203–216, Asheville, NC, December 1993.Google Scholar
  18. 18.
    David Walker. A type system for expressive security policies. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 254–267, Boston, MA, January 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Andrew Bernard
    • 1
  • Peter Lee
    • 1
  1. 1.School of Computer ScienceCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations