Foundational proof-carrying code

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations


Proof-carrying code is a framework for the mechanical verification of safety properties of machine language programs, but the problem arises of quis custodiat ipsos custodes - who will verify the verifier itself? Foundational proof-carrying code is verification from the smallest possible set of axioms, using the simplest possible verifier and the smallest possible runtime system. I will describe many of the mathematical and engineering problems to be solved in the construction of a foundational proof-carrying code system.

Original languageEnglish (US)
Title of host publicationFoundations of Intrusion Tolerant Systems, OASIS 2003
EditorsJaynarayan H. Lala
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages10
ISBN (Electronic)076952057X, 9780769520575
StatePublished - 2003
EventFoundations of Intrusion Tolerant Systems, OASIS 2003 - Los Alamitos, United States
Duration: Dec 1 2003 → …

Publication series

NameFoundations of Intrusion Tolerant Systems, OASIS 2003


OtherFoundations of Intrusion Tolerant Systems, OASIS 2003
Country/TerritoryUnited States
CityLos Alamitos
Period12/1/03 → …

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software


  • Application software
  • Assembly
  • Java
  • Kernel
  • Logic
  • Mechanical factors
  • Permission
  • Program processors
  • Software safety
  • Virtual machining

Cite this