|
||||||||||||||||
|
Ph.D. ThesesCode-Carrying Theory
By Aytekin Vargun
Code-carrying Theory (CCT) is an alternative to the proof-carrying code (PCC) approach to secure delivery of code. With PCC, code is accompanied by assertions and a proof of its correctness or of other required properties. The code consumer does not accept delivery unless it first succeeds in generating theorems, called verification conditions, from the code and assertions and checking that the supplied proof proves these theorems. With CCT, instead of transmitting both code and proof explicitly, only assertions and proofs are transmitted to the consumer. If proof checking succeeds, code is then obtained by applying a simple tool called CODEGEN to the resulting theory. This thesis first explains the design and implementation of CCT steps and shows how it can be used to achieve secure delivery of code with required correctness or safety properties. All the tools used in the verification steps are implemented in ATHENA, which is both a traditional programming language and a deduction language. In addition, we present examples of generic and nongeneric proofs which play an important role in our design. We show how critical it is to organize theories and proofs to reduce the amount of information transmitted between the producer and consumer.
|
||||||||||||||||
Research
