[Prev][Next][Index][Thread]
Paper announcement: A Metalogical Approach to Foundational Certified Code
-
To: types@cis.upenn.edu
-
Subject: Paper announcement: A Metalogical Approach to Foundational Certified Code
-
From: Karl Crary <crary@cs.cmu.edu>
-
Date: Thu, 6 Feb 2003 12:45:49 -0500
-
Importance: Normal
-
MMDF-Warning: Parse error in original version of preceding line at postoffice.srv.cs.cmu.edu
We would like to announce the availability of the following paper at:
http:/www.cs.cmu.edu/~crary/papers
Comments or suggestions are always welcome.
-- Karl Crary and Susmit Sarkar
--------------------
A Metalogical Approach to Foundational Certified Code
Karl Crary and 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. 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 and foundational account of safety for a fully expressive
typed assembly language.