Benutzer: Gast  Login
Originaltitel:
Verified Proof Carrying Code 
Übersetzter Titel:
Formalisierung und Verifikation eines Systems zum statischen Ausschluss von Sicherheitsfehlern in Bytecode Programmen 
Jahr:
2006 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof. Ph.D.) 
Gutachter:
Hofmann, Martin (Prof. Ph.D.) 
Format:
Text 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
Verification; security; safety; proof carrying code 
Übersetzte Stichworte:
Programmverifikation; Sicherheit; Theorembeweisen 
Kurzfassung:
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...    »
 
Übersetzte Kurzfassung:
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...    »
 
Veröffentlichung:
Universitätsbibliothek der Technischen Universität München 
Mündliche Prüfung:
19.05.2006 
Dateigröße:
1525353 bytes 
Seiten:
210 
Letzte Änderung:
10.07.2007