Foundational proof-carrying code

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

1 Scopus citations

Abstract

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.
Pages25-34
Number of pages10
ISBN (Electronic)076952057X, 9780769520575
DOIs
StatePublished - Jan 1 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

Other

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

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software

Keywords

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

Cite this