VEP: a virtual machine for extended proof-carrying code

ABSTRACT

One of the key issues with the practical applicability of Proof-Carrying Code (PCC) and its related methods is the difficulty in communicating the proofs which are inherently large. One way to alleviate this problem is to transmit, instead, a proof generator for the program in question in a generic extended PCC framework (EPCC). The EPCC needs to provide the execution of the proof generator at the consumer side in a secure manner. The ability to securely run arbitrary untrusted proof generator is a challenging problem.

We explore the design of a small and safe virtual machine (VEP) which provides the EPCC with a robust security guarantee. The VEP is a minor TCB extension of less than 300 lines of code which works as a safe execution environment and brings about a practical solution to thecommon security and resource management issues.

REFERENCES

• 1: Andrew W. Appel , Edward W. Felten, Proof-carrying authentication, Proceedings of the 6th ACM conference on Computer and communications security, p.52-62, November 01-04, 1999, Kent Ridge Digital Labs, Singapore [doi>10.1145/319709.319718]
• 2: A. W. Appel and D. C. Wang. JVM TCB: Measurements of the trusted computing base of Java virtual machines. Technical Report Technical Report CS-TR-647--02, Princeton University, 2002.
• 3: J. Cheney. First-order term compression: Techniques and applications, 1998.
• 4: Brian Davis , Andrew Beatty , Kevin Casey , David Gregg , John Waldron, The case for virtual register machines, Proceedings of the 2003 workshop on Interpreters, virtual machines and emulators, p.41-49, June 12-12, 2003, San Diego, California [doi>10.1145/858570.858575]
• 5: John L. Hennessy , David A. Patterson, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 02
• 6: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 7: E. Meijer and J. Gough. Technical Overview of the Common Language Runtime, 2000.
• 8: George C. Necula, A Scalable Architecture for Proof-Carrying Code, Proceedings of the 5th International Symposium on Functional and Logic Programming, p.21-39, March 07-09, 2001
• 9: George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
• 10: George C. Necula , S. P. Rahul, Oracle-based checking of untrusted software, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-154, January 2001, London, United Kingdom
• 11: Heidar Pirzadeh , Danny Dubé, Encoding the Program Correctness Proofs as Programs in PCC Technology, Proceedings of the 2008 Sixth Annual Conference on Privacy, Security and Trust, p.121-132, October 01-03, 2008 [doi>10.1109/PST.2008.20]
• 12: S. P. Rahul , George C. Necula, Proof Optimization Using Lemma Extraction, University of California at Berkeley, Berkeley, CA, 2001
• 13: Dinghao Wu , Andrew W. Appel , Aaron Stump, Foundational proof checkers with small witnesses, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.264-274, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888276]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
      C.1.3 Other Architecture Styles

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Macro and assembly languages; Specialized application languages
      D.3.4 Processors
          Subjects: Interpreters

General Terms:
Languages, Security, Verification

Keywords:
proof-carrying code, virtual machine