file.pdf (238.9 kB)
Download file

Foundational Certified Code in a Metalogical Framework

Download (238.9 kB)
journal contribution
posted on 01.01.1979, 00:00 authored by Karl Crary, Susmit Sarkar
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.

History

Publisher Statement

All Rights Reserved

Date

01/01/1979

Usage metrics

Exports