Verified Proof Carrying Code

• Applicant: Professor Tobias Nipkow, Ph.D.
• Subject Area: Theoretical Computer Science
• Term: from 2003 to 2009
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5396601

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.

• DFG Programme: Research Grants