User: Guest  Login
Original title:
Verified Proof Carrying Code
Translated title:
Formalisierung und Verifikation eines Systems zum statischen Ausschluss von Sicherheitsfehlern in Bytecode Programmen
Author:
Wildmoser, Martin
Year:
2006
Document type:
Dissertation
Institution:
Fakultät für Informatik
Advisor:
Nipkow, Tobias (Prof. Ph.D.)
Referee:
Hofmann, Martin (Prof. Ph.D.)
Format:
Text
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik
Keywords:
Verification; security; safety; proof carrying code
Translated keywords:
Programmverifikation; Sicherheit; Theorembeweisen
Abstract:
Proof Carrying Code (PCC) is a technique to exclude safety errors in low level code. Instead of runtime tests, it statically checks a proof of safety (a certificate) attached to the code. To guarantee that PCC only accepts safe code, we formalise and verify it in Isabelle/HOL, an interactive theorem prover for higher order logic. In an abstract framework we identify key components and their interfaces, specify requirements and prove theorems stating that accepted code is safe and under what cond...    »
Translated abstract:
Proof Carrying Code (PCC) ist eine Technik zum Ausschluss von Sicherheitsfehlern in Maschinencode. Statt Laufzeittests durchzuführen, wird statisch ein Beweis (Zertifikat) geprüft. Um zu garantieren, dass ein solches System nur sicheren Code akzeptiert, formalisieren und verifizieren wir PCC in Isabelle/HOL, einem Beweissystem für höherstufige Logik. Wir beweisen, dass zertifizierter Code sicher ist, und unter welchen Voraussetzungen sich sicherer Code zertifizieren lässt. Der Hauptbeitrag ist e...    »
Publication :
Universitätsbibliothek der Technischen Universität München
WWW:
https://mediatum.ub.tum.de/?id=601800
Date of submission:
03.11.2005
Oral examination:
19.05.2006
File size:
1525353 bytes
Pages:
210
Urn (citeable URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss20060619-1654162861
Last change:
10.07.2007
 BibTeX