Semantische Modellierung, Analyse und Verifikation von sprachbasierter Software-Sicherheit

• Applicants: Professor Tobias Nipkow, Ph.D.; Professor Dr.-Ing. Gregor Snelting
• Subject Area: Software Engineering and Programming Languages
• Term: from 2007 to 2013
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 47694595

• Final Report Year: 2016

Final Report Abstract

IT-Sicherheit wurde von Industrie und Politik längst als nationale Aufgabe erkannt. Deshalb entwickeln viele Wissenschaftler Verfahren zur Sicherheitsanalyse von Software. Neuerdings versucht man, direkt am Programmcode Software-Lecks zu erkennen, indem feindetalliert sämtliche möglichen Informationsflüsse durch ein Program nachvollzogen werden. Wenn eine App also heimlich Daten an die NSA schickt, wird das durch eine derartige Informationsflussanalyse (IFC) sofort erkannt. Aber wie schon Juvenal fragte: „Quis custodiet ipsos custodes?“, „Wer bewacht die Wächter?“. Es ist ein Beweis notwendig, dass die Informationsflussanalyse tatsachlich alle Lecks findet. Auch viele andere Aspekte der Verarbeitung von Programmiersprachen spielen eine Rolle bei Sicherheitsprüfungen, und müssen durch Beweise abgesichert werden. Manuelle Beweise wiederum haben sich als fehleranfällig herausgestellt, da sie typischerweise mathematisch eher schematisch, jedoch sehr umfangreich sind. Im DFG-Projekt Quis Custodiet gelang es, durch den Einsatz des rechnergestützten Beweisassistenten Isabelle erstmalig große Beweise über Sicherheitsanalysen und andere Programmeigenschaften maschinengeprüft zu führen. Dabei wurden auch die Einsatzmöglichkeiten von Isabelle selbst stark verbessert. Insbesondere wurde die Fähigkeit des Isabelle Systems signifikant gesteigert, mathematische Formeln automatisch zu beweisen oder zu widerlegen. Das Projekt koppelte Isabelle an eine Reihe externer, schneller Komponenten, die genau hierauf spezialisiert sind. So konnten nach Abschluss des Projekts 2013 40% mehr Formeln automatisch bewiesen werden als noch 2010. Weiterführende Arbeiten kommen auf eine Steigerung von fast 70% gegenüber 2010. Gleichzeitig wurde in Quis Custodiet das Sicherheitsanalyse-System JOANA mit Isabelle verifiziert. JOANA ist der z.Zt. einzige international verfügbare IFC-Analysator, der volles Java mit Threads bearbeiten kann, dabei auch die gefürchteten probabilistischen Lecks findet, dank ausgefeilter Programmanalyse kaum Fehlalarme erzeugt, bis ca. 100000 LOC skaliert, und eine ausgereifte Implementierung bietet. JOANA wird in vielen Projekten des DFG-SPP 1496 “Zuverlässig sichere Software” eingesetzt, industrielle Anwendungen sind in Vorbereitung. Dank Isabelle und Quis Custodiet kann sich der Anwender darauf verlassen, dass JOANA alle Lecks garantiert findet.

Publications

• On PDG-Based Noninterference and its Modular Proof. Proc. 4th Workshop on Programming Languages and Analysis for Security, pp. 31–44, ACM, 2009
  Daniel Wasserrab, Denis Lohner, Gregor Snelting
  
• From Formal Semantics to Verified Slicing – A Modular Framework with Applications in Language Based Security. Dissertation, Karlsruher Institut für Technologie, Fakultät für Informatik, Oktober 2010
  Daniel Wasserrab
  
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. Proc. Conference on Interactive Theorem Proving (ITP 2010), pp. 131–146, LNCS 6172, Springer, 2010
  Jasmin Christian Blanchette and Tobias Nipkow
  
• Verifying a Compiler for Java Threads. Proc. European Symposium on Programming (ESOP 2010), pp. 427–447, LNCS 6012, Springer, 2010
  Andreas Lochbihler
  
• Monotonicity Inference for Higher-Order Formulas. Journal of Automated Reasoning, Vol. 47(4), pp. 369–398, 2011
  Jasmin Christian Blanchette, Alexander Krauss
  
• Nitpicking C++ Concurrency. Proc. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011), pp. 113–124, ACM Press, 2011
  Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar
  
• A Machine-Checked, Type-Safe Model of Java Concurrency: Language, Virtual Machine, Memory Model, and Verified Compiler. Dissertation, Karlsruher Institut für Technologie, Fakultät für Informatik, Juli 2012
  Andreas Lochbihler
  
• Automatic Proofs and Refutations for Higher-Order Logic. Dissertation, Technische Universität München, Fakultät für Informatik, Juni 2012
  Jasmin Christian Blanchette
  
• Foundational, Compositional (Co)datatypes for Higher-Order Logic – Category Theory Applied to Theorem Proving. Proc. IEEE Symposium on Logic in Computer Science (LICS 2012), pp. 596–605, IEEE, 2012
  Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette
  
• Java and the Java Memory Model – a Unified, Machine-Checked Formalisation. Proc. European Symposium on Programming (ESOP’12), pp. 497–517, LNCS 7211, Springer, 2012
  Andreas Lochbihler
  
• Extending Sledgehammer with SMT Solvers. Journal of Automated Reasoning, Vol. 51(1), pp. 109–128, 2013
  Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson
  
• Making the Java Memory Model Safe. ACM Transactions on Programming Languages and Systems, Vol. 35(4), pp. 12:1–12:65, 2014
  Andreas Lochbihler
  (See online at https://doi.org/10.1145/2518191)