Foundational certified code in the Twelf metalogical framework

Karl Crary*, Susmit Sarkar

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)

Abstract

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. Using the Twelf metalogical framework, we have constructed a safety policy for the IA-32 architecture with a trusted runtime library. The safety policy is based on a formalized operational semantics. We have also developed a complete, foundational proof that a fully expressive typed assembly language satisfies that safety policy.

Original languageEnglish
Article numberARTN 16
Number of pages26
JournalACM Transactions on Computational Logic
Volume9
Issue number3
DOIs
Publication statusPublished - 2008

Keywords

  • languages
  • logic programming
  • verification
  • foundational certified code
  • metalogic
  • TYPED ASSEMBLY LANGUAGE

Fingerprint

Dive into the research topics of 'Foundational certified code in the Twelf metalogical framework'. Together they form a unique fingerprint.

Cite this