Treffer: Verified Proof Carrying Code ; Formalisierung und Verifikation eines Systems zum statischen Ausschluss von Sicherheitsfehlern in Bytecode Programmen

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 conditions safe code can be certified. Our main contribution is a generic verification condition generator (VCG), which inspects code and emits proof obligations. By adjusting parameters, we instantiate this VCG to a Java-like bytecode language with objects, methods and exceptions. Bytecode with annotations in a first order assertion logic can be certified not to cause arithmetic overflow. To annotate code we integrate bytecode analysers for intervals and types. Finally, Isabelle's facilities for code generation, proof production and proof checking enable us to turn our formalisation into a runnable prototype. ; 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 ein generischer Verifikationsbedingungsgenerator (VCG), den wir für eine Teilsprache von Java-Bytecode instanziieren. Dieser VCG inspiziert Bytecode, der mit Formeln einer eigens geschaffenen Zusicherungssprache annotiert ist, und liefert Beweisverpflichtungen, die arithmetischen Überlauf und falsche Annotationen ausschließen. Annotationen können wir manuell oder mittels angebundener Analysatoren für Typen und Intervalle ...