User: Guest  Login
Original title:
Verified Proof Carrying Code 
Translated title:
Formalisierung und Verifikation eines Systems zum statischen Ausschluss von Sicherheitsfehlern in Bytecode Programmen 
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 
Oral examination:
19.05.2006 
File size:
1525353 bytes 
Pages:
210 
Last change:
10.07.2007