Verified proof carrying code [Elektronische Ressource] / Martin Wildmoser

M. Wildmoser

Description

ff f ff f f ff ff f ff f f ff f fVerified Proof Carrying CodeMartin WildmoserLehrstuhl fur¨ Software&Systems EngineeringInstitut fu¨r InformatikTechnische Universit¨at Munchen¨Lehrstuhl fur¨ Software & Systems EngineeringInstitut fur¨ InformatikTechnische Universit¨at Munch¨ enVerified Proof Carrying CodeMartin WildmoserVollst¨andiger Abdruck der von der Fakult¨at fur¨ Informatik der Technischen Universit¨atMu¨nchen zur Erlangung des akademischen Grades einesDoktors der Naturwissenschaften (Dr. rer. nat.)genehmigten Dissertation.Vorsitzender: Univ.-Prof. Dr. Uwe BaumgartenPruf¨ er der Dissertation: 1. Univ.-Prof. Tobias Nipkow, Ph.D.2. Univ.-Prof. Martin Hofmann, Ph.D.(Ludwig-Maximilians-Universit¨at Mun¨ chen)Die Dissertation wurde am 3.11.2005 bei der Technischen Universit¨at Mun¨ cheneingereicht und durch die Fakult¨at fur¨ Informatik am 10.5.2006 angenommen.KurzfassungProof Carrying Code (PCC) ist eine Technik zum Ausschluss von Sicherheitsfehlernin Maschinencode. Statt Laufzeittests durchzufuh¨ ren, wird statisch ein Beweis (Zerti-fikat) gepruf¨ t. Um zu garantieren, dass ein solches System nur sicheren Code akzep-tiert, formalisieren und verifizieren wir PCC in Isabelle/HOL, einem Beweissystem fur¨h¨oherstufige Logik. Wir beweisen, dass zertifizierter Code sicher ist, und unter welchenVoraussetzungen sich sicherer Code zertifizieren las¨ st.

Sujets

• Informatik

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2006
• Nombre de lectures: 18
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait