18th Annual IEEE Symposium on Logic in Computer Science (LICS'03) A Sound Framework for Untrusted Verification-Condition Generators Ottawa, Canada June 22-June 25 ISBN: 0-7695-1884-2
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. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||