A Formalization of the Proof-Carrying Code Architecture in a Linear Logical Framework
M. Pleško, Frank Pfenning · 1999
this paper we formalize the PCC safety architecture in a logical framework, which constitutes an important first step towards an environment for experimentation and formal verification of properties of safety policies and their implementations in the PCC architecture. Our main tool is LLF [CP96], a logical framework based on linear logic [Gir87]. Linear logic provides natural means of describing programming languages and their semantics, especially those of an imperative nature. LLF permits us to give a high-level description of assembly code, safety policies, and safety proofs within the same language. In future work we plan to formally verify safety policies based on their encoding in LLF. We also hope to introduce linearity to the PCC architecture itself in order to reduce the size of safety proofs. We will first further describe the PCC infrastructure in Section 2 followed by a brief sketch of our meta-language, the linear logical framework in Section 3. In order to implement portions of the PCC system, we must choose a language for our simulated agent. We follow [Nec98] and use Safe Assembly Language (SAL), a generic RISC architecture. SAL is described in Section 4. Two execution models, one without and one with run-time safety checks, are described in Section 5. A formal connection between these two models is provided in Section 6, where we specify safety as a property of traces of unsafe execution. An implementation of the Verification Condition Generator