Proof-carrying Bytecode

Stephen Gilmore, Matthew Prowse

Research output: Contribution to journalArticlepeer-review

Abstract

In the Mobile Resource Guarantees project's Proof Carrying Code implementation, .class files are associated with Isabelle [Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002] proof scripts containing proofs of bounds on their resource consumption. By using the tools gf and isabelle on the consumer-side, it is possible to verify after download, that a piece of code conforms to a particular resource policy specified by the consumer, and prevent execution in the event that it does not. We present here a prototype implementation using certain features of the J2SE 5.0 Platform [Sun Microsystems, Inc. Java 2 Platform, Standard Edition 1.5.0, http://java.sun.com/j2se/1.5.0/, May 27, 2004]. The (unmodified) bytecode and its proof are packaged as a JAR file for convenient distribution. The codebase uses Java agents providing the Instrumentation interface, and implements a custom permission class and Security Manager. The external tools are invoked from within Java. Two system commands makeMRGjar and MRGjava provide a convenient way of using this implementation.

Original languageEnglish
Pages (from-to)3-18
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Volume141
Issue number1
DOIs
Publication statusPublished - 2005

Fingerprint Dive into the research topics of 'Proof-carrying Bytecode'. Together they form a unique fingerprint.

Cite this