Foundational Certified Code in a Metalogical Framework

12 years 6 days ago
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.
Karl Crary, Susmit Sarkar
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where CADE
Authors Karl Crary, Susmit Sarkar
Comments (0)