@inproceedings{1179fe75c46b466d804edbbf7893825a,

title = "Foundational proof-carrying code",

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.",

keywords = "Application software, Assembly, Java, Kernel, Logic, Mechanical factors, Permission, Program processors, Software safety, Virtual machining",

author = "Appel, {Andrew W.}",

year = "2003",

month = jan,

day = "1",

doi = "10.1109/FITS.2003.1264926",

language = "English (US)",

series = "Foundations of Intrusion Tolerant Systems, OASIS 2003",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "25--34",

editor = "Lala, {Jaynarayan H.}",

booktitle = "Foundations of Intrusion Tolerant Systems, OASIS 2003",

address = "United States",

note = "Foundations of Intrusion Tolerant Systems, OASIS 2003 ; Conference date: 01-12-2003",

}