Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code

Abstract

Proof-Carrying Code (PCC) is a general framework for the mechanical verification of safety properties of machine-language programs. It allows a code producer to provide an executable program to a code consumer, along with a machine-checkable proof of safety such that the code consumer can check the proof before running the program. PCC has the advantage of small Trusted Computing Base (TCB), since the proof checking can be a simple mechanical procedure. A weakness of previous PCC systems is that the proof-checking infrastructure is based on some complicated logic or type system that is not necessarily sound. Foundational Proof-Carrying Code (FPCC) aims to further reduce the TCB size by an order of magnitude by building the safety proof based on the simple and trustworthy foundations of mathematical logic. There are three major componentsin an FPCC system: a compiler, a proof checker, and the safety proof of an input machine-language program. The compiler produces machine code accompanied bya proof of safety. The proof checker verifes, sometimes also reconstructs, the safety proof before the program gets executed. We have built a prototype system. Our prototype is the first end-to-end FPCC system, including a type-preserving compiler from Core ML to SPARC (based onSML/NJ), a low-level typed assembly language LTAL, a foundational proof-checkerFlit, and a nearly complete machine-checkable soundness proof. The system compilesCore ML programs to SPARC code, accompanied with programs in a low-level typed assembly language; these typed assembly programs serve as the proof witnesses of the safety of the corresponding SPARC machine code. In this thesis, I'll explain the design of interfaces between these components and show how to build an end-to-end FPCC system.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2005
Accession Number
AD1006373

Entities

People

  • Dinghao Wu

Organizations

  • Princeton University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Application Software
  • Artificial Intelligence
  • Assembly Languages
  • Authentication
  • Coding
  • Computer Program Documentation
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Decoding
  • Instruction Set Architecture
  • Machine Languages
  • Operating Systems
  • Programming Languages
  • Semantic Models
  • Word Processors

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.