Proof-Carrying Code Survivability Validation Framework

Our project applies automated proof checking to two application domains: protecting host computers from untrusted application programs, and distributed authentication for access-control. Computers have many reasons to run untrusted application programs. Active-network routers may delegate decisions to embedded user code, e-mail recipients may want to run executable attachments, and high-assurance systems may want to run commercial off-the-shelf software for some applications. In all of these situations, the survivability goals are to protect private host data from modification or access by the untrusted code, to limit the code’s access to external resources, and to prevent execution faults from crashing the host. Two traditional and successful mechanisms that combine to achieve these goals are hardware virtual memory with an operating-system kernel. However, today’s environment often requires the host to interact with the application through an object-oriented interface, which is very clumsy to do when address-space boundaries must be crossed: instead of pointers and private variables, we have remote-procedure call with marshalling/unmarshalling of data. Our proof-carrying code (PCC) and certified binaries approach will achieve security goals even in a shared-memory, rich-API environment. For the remainder of this report we will discuss proof-carrying code. The issue