Foundational Certified Code in a Metalogical Framework

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. This material is based on work supported in part by NSF grants CCR-9984812 and CCR-0121633. Any opinions, findings, and conclusions or recommendations in this publication are those of the authors and do not reflect the views of this agency. 

• Type: Conference
• Year: 2003
• Where: CADE
• Authors: Karl Crary, Susmit Sarkar
• Keywords: Automated Reasoning, CADE 2003, Expressive Typed Assembly, Foundational Certified Code, Safety Proofs