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

• Final Report Year: 2009

Final Report Abstract

Das Prinzip Proof Carrying Code bedeutet, ein Programm mit einem Beweis zu bündeln, dass das Programm gewisse Eigenschaften erfüllt. Dies können funktionale Eigenschaften sein, sind aber meist Sicherheitseigenschaften wie die Abwesenheit gewisser Laufzeitfehler oder die Einhaltung gewisser Zeit oder Platzgrenzen. Die Beweise müssen in einer standardisierten formalen Logik Schritt für Schritt ausgeführt sein, damit der Benutzer des Programms mit einfachen Mitteln die Korrektheit des Beweises überprüfen kann. Typisches Anwendugszenarium ist Software, die man vom Internet lädt, und die dann auf dem eigenen Rechner ausgeführt werden soll, ohne dort Schaden anzurichten. Das Projekt hat nun folgende Fortschritte erzielen k¨nnen: • Die Sicherheit des PCC Prinzips steht und fällt damit, ob eine bestimmten Formel tatsächlich ein bestimmtes Verhalten eines Programms impliziert, ob also die Formel das Verhalten des Programms richtig widerspiegelt. Daher haben wir einen logischen Rahmen entwickelt, der es ermöglicht, aus der Semantik der Programmiersprache und der Logik und der gewünschten Sicherheitseigenschaft einen Verifikationsbedingungsgenerator (VCG) zu erzeugen, der zu einem Programm eine Formel generiert, die genau dann wahr ist, wenn das Programm die Sicherheitseingenschaft erfüllt. Dies erlaubt eine logisch saubere Fundierung des PCC Prinzips und liefert automatisch einen verifizierten VCG, eine Kernkomponente jedes PCC Systems. • In unserer Anwendung spielen numerische Eigenschaften eine wichtige Rolle. Um die vom VCG erzeugten Formeln automatisch zu beu weisen, haben wir Entscheidungsprozeduren für verschiedene Klassen arithmetischer Formeln formalisiert und verifiziert. Eine wichtige technische Neuerung dabei ist die Benutzung des Prinzips der Reflktion für die betrachteten Verfahren. Dies erlaubt eine Beschleunigung der Entscheidungsprozeduren typischerweise um den Faktor 100.

Publications

• Verified bytecode subroutines. In: Theorem Proving in Higher Order Logics (TPHOLs’03), LNCS 2758, 55–70. 2003
  G. Klein and M. Wildmoser
  
• Verified bytecode subroutines. Journal of Automated Reasoning, 30(3–4):363–398, 2003
  G. Klein and M. Wildmoser
  
• Verified bytecode verifiers. Theoretical Computer Science, 298:583–626, 2003
  G. Klein and T. Nipkow
  
• Certifying machine code safety: Shallow versus deep embedding. In: Theorem Proving in Higher Order Logics (TPHOLs 2004), LNCS 3223, 305–320. 2004
  M. Wildmoser and T. Nipkow
  
• Prototyping proof carrying code. In: IFIP 18th World Computer Congress, 333–347. 2004
  M. Wildmoser, T. Nipkow, G. Klein, and S. Nanz
  
• Asserting bytecode safety. In: Programming Languages and Systems (ESOP), LNCS 3444, 326–341. 2005
  M. Wildmoser and T. Nipkow
  
• Bytecode Analysis for Proof Carrying Code. In: Proc. 1st Workshop Bytecode Semantics, Verification and Transformation, volume 141 of Electronic Notes in Computer Science, 19–34, 2005
  M. Wildmoser, A. Chaieb, and T. Nipkow
  
• Verifying and reflecting quantifier elimination for Presburger arithmetic. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005), LNCS 3835, 367–380. 2005
  A. Chaieb and T. Nipkow
  
• Proof-producing program analysis. In: Theoretical Aspects of Computing (ICTAC 2006), LNCS 4281, 287–301. 2006
  A. Chaieb
  
• Verifying mixed real-integer quantifier elimination. In: Automated Reasoning (IJCAR 2006), LNCS 4130, 528–540. 2006
  A. Chaieb
  
• Context aware Calculation and Deduction — Ring Equalities via Gröbner Bases in Isabelle. In: Towards Mechanized Mathematical Assistants (Calculemus/MKM), LNCS 4573, 27–39. 2007
  A. Chaieb and M. Wenzel
  
• Linear quantifier elimination. In: Automated Reasoning (IJCAR 2008), LNCS 5195, 18–33. 2008
  T. Nipkow
  
• Parametric linear arithmetic over ordered fields in Isabelle/HOL. In: Intelligent Computer Mathematics (AISC/Calculemus/MKM), LNCS 5144, 246–260. 2008
  A. Chaieb
  
• Proof synthesis and reflection for linear arithmetic. J. Automated Reasoning, 41:33–59, 2008
  A. Chaieb and T. Nipkow
  
• Reflecting quantifier elimination for linear arithmetic. In: Formal Logical Methods for System Security and Correctness, 245–266. IOS Press, 2008
  T. Nipkow