loading...
A Sound Framework for Untrusted Verification-Condition Generators
Ottawa, Canada June 22-June 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2003.121006518th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
George C. Necula, University of California, Berkeley
Robert R. Schneck, University of California, Berkeley
We propose a framework called configurable proof-carrying code, which allows the untrusted producer of mobile code to provide the bulk of the code verifier used by a code receiver to check the safety of the received code. The resulting system is both more flexible and also more trustworthy than a standard proof-carrying code system, because only a small part of the verifier needs to be trusted, while the remaining part can be configured freely to suit the safety policy on one hand, and the structure of the mobile code on the other hand.
In this paper we describe formally the protocol that the untrusted verifier must follow in the interaction with the trusted infrastructure. We present a proof of the soundness of the system, and we give preliminary evidence that the architecture is expressive enough to delegate to the untrusted verifier even the handling of loop invariants, indirect jumps and calling conventions.
Citation:
George C. Necula, Robert R. Schneck, "A Sound Framework for Untrusted Verification-Condition Generators," lics, pp.248, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.