Verified Proof Carrying Code

点击翻译按钮获取中文摘要

Programme sind notorisch unzuverlässig, und Programmbeweise oft unmöglich. Eine Alternative ist, das Ergebnis einer Berechnung mit einem Zertifikat zu versehen, das die Korrektheit des Ergebnisses zumindest partiell überprüfbar macht. Ein Spezialfall ist der Proof Carrying Code (PCC) Ansatz, bei dem das Ergebnis (z.B. eines Übersetzungsvorgangs) ein Programm ist, und das Zertifikat gewisse Minimaleigenschaften des Programms garantiert (z.B. die Abwesenheit gewisser Laufzeitfehler). Ziel des Vorhabens ist es, den PCC Ansatz auf beliebige Sicherheitseigenschaften zu verallgemeinern, und ihn so weit wie möglich logisch vollständig zu fundieren. Die logische Fundierung wird mit Hilfe des Theorembeweisers Isabelle/HOL geleistet: Er erlaubt es, die der Zertifikatsüberprüfung zugrundeliegende Logil, bzgl. der Semantik der Programmiersprache als korrekt zu beweisen. Diesen genetischen Ansatz wenden wir dann auf zwei sicherheitskritische, aber bisher im PCC Rahmen kaum betrachteten Eigenschaften an: Garantie von Laufzeit- und Speicherplatzschranken, und Abwesenheit numerischer Fehler, insbesondere Überlauf.