CMU-CS-03-108
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-03-108

Foundational Cerfied Code in a
Metalogical Framework

Karl Crary, Susmit Sarkar

December 2003

CMU-CS-03-108.ps
CMU-CS-03-108.pdf


Keywords: Foundational certified code, meta-logic, logic programming


Foundational certified code systems seek to prove untrusted programs to be safe relative to safety policies given in terms of actual machine architectures, thereby improving the systems' flexibility and extensibility. Previous efforts have employed a structure wherein the proofs are expressed in the same logic used to express the safety policy. We propose an alternative structure wherein safety proofs are expressed in the Twelf metalogic, thereby eliminating from those proofs an extra layer of encoding needed in the previous accounts. Using this metalogical approach, we have constructed a complete, foundational account of safety for a fully expressive typed assembly language.

19 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu