Teilprojekt 1: Werkzeuge und Methoden

Die Arbeiten in Teilprojekt 1 zielen auf die Integration verschiedener Beweistechniken, um letztendlich eine durchgängige Verifikation zu ermöglichen. Es werden sowohl interaktive wie auch automatische Verfahren betrachtet. Zur konsistenten Verwaltung der erstellten logischen Artefakte wird in TP1 ein Repository entwickelt. Zusätzlich entwickeln wir eine Verifikationsumgebung für Kryptographie und Sicherheit, in der Kryptographische Primitive formalisiert und verifiziert werden. Die (weiter-)entwickelten Werkzeuge und Techniken werden anhand der Anwendungsprojekte in TP2, TP3, TP4 und TP6 evaluiert.

Eine Übersicht der Struktur von TP1 gibt das folgende Schaubild wieder:

TP1-Struktur.gif

Semantik und interaktive Verifikation

In TP1 werden zur Analye von C0 Programmen ein Big-Step Semantik und eine korrenspondierende Small-Step Semantik entwickelt. Aufbauend auf diesen Semantiken werden eine Hoare-Logik und ein C0-Kalkül für dynamische Logik entwickelt. Die genannten Semantiken liegen den bei der Verifikation verwendeten Werkzeugen zu Grunde.

semantik-2.gif

Einbindung von automatischen Verfahren

Automatische Verfahren gliedern sich in dem in TP1 verfolgten Ansatz in automatische Theorembeweiser (ATP) und in spezielle Verfahren

  • zum Nachweis temporaler Eigenschaften.
  • zur Analyse von C0 Programmen,
  • zur Protokollanalyse und
  • zur Execution Time Analysis.
Die Integration verschiedener (automatischer) Beweistechniken und der damit verbundenen Werkzeuge ist im folgenden Schaubild dargestellt:

Werkzeug-Integration.gif

Die Einbindung automatischer Beweiser in die interaktiven Beweissysteme ist im folgenden Schaubild verdeutlicht.

Automatische-Beweiser-1.gif

Neben diesen generischen Techniken gibt es spezielle Verfahren z.B. zur Verifikation temporaler Eigenschaften und zur Programmanalyse, insbesondere von Programmen auf Pointerstrukturen.

Temporal-Pointer.gif

Kryptographie und Sicherheit

Die Arbeiten in diesem Bereich analysieren zum einen die bei sicherheitskritischen Anwendungen verwendeten kryptographischen Primitive wie beispielsweise Verschlüsselung, Signatur und Hashbildung. Zum anderen werden Verfahren zur Verifikation und Analyse kryptographischer Protokolle untersucht und optimiert. Die entwickelten Techniken werden hierbei entwicklungsbegleitend zu TP4 bereits in sehr frühen Phasen eingesetzt. Abschließend wird im Rahmen von TP4 ein Szenario bestehend aus Host, Chipkartenterminal, Chipkarte, Biosensor und kryptographischem Protokoll in C0 implementiert.

Weiterführende Arbeiten behandeln die Verbindung der symbolischen Ebene der Protokollverifikation mit der Ebene eines probabilistischen (Protokoll-) Modells.

Das gesamte Vorgehen ist im folgenden Schaubild veranschaulicht.

Krypto-Protokolle.gif

Resultate

  • Big-Step Semantik und Small-Step Semantik für C0 sind fertig und bilden die Basis für die verwendeten/erweiterten/entwickelten Verifikationswerkzeuge
  • Korrespondenzbeweis zwischen Big-Step Semantik und Small-Step Semantik ist zur Zeit in Arbeit
  • Hoare Logik für partielle und totale Korrekthiet ist fertiggestellt
  • C0-Kalkül in dynamischer Logik ist fertiggestellt
  • Entwicklungsmethode für zustandsbasierte Systeme mit Pointern ist erstellt
  • Werkzeuge für Model-Checking und Terminierung sind erstellt
  • Symbolische Shape Analyse ist in Arbeit
  • Refinement Werkzeug zum Nachweis temporaler Eigenschaften
  • Einbindung automatischer Verfahren in VSE und ISABELLE ist in einer ersten Ausbaustufe erstellt und werden innerhalb der Anwendungen verwendet
  • Verfahren zur (automatischen) Analyse von kryptographischen Protokollen sind erstellt
  • Strategie zur induktiven Protokollverifikation in VSE ist implementiert (TP4 Protokoll ist verifiziert)
  • Verfeinerung der kryptographischen Protokolle ist in Arbeit
  • Formalisierung der mathematischen Grundlagen der Kryptographie ist in ISABELLE erstellt
  • Grundlgegende Funktionalität des Repository zur Verwaltung der Entwicklungen ist erstellt

Publikationen

  1. Andreas Podelski, Andrey Rybalchenko: Transition Invariants. Proc. 19th IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland. July 13-17, 2004.
  2. Amir Pnueli, Andreas Podelski, Andrey Rybalchenko: Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. Proc. of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Edinburgh, U.K. April 4-8, 2005.
  3. Andreas Podelski, Andrey Rybalchenko: Transition Predicate Abstraction and Fair Termination. Proc. of the 32nd ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2005), Long Beach, California, USA. January 12-14, 2005.
  4. Bernd Finkbeiner, Henny Sipma: Checking Finite Traces using Alternating Automata. Formal Methods in System Design, vol 24, pages 101-127. March 2004.
  5. Bernd Finkbeiner, Sriram Sankaranarayanan, Henny Sipma: Collecting Statistics over Runtime Executions. Formal Methods in System Design. To appear.
  6. Andreas Podelski, Ina Schäfer, Silke Wagner: Summaries for While Programs with Recursion. Proc. of the European Symposium on Programming (ESOP 2005), Edinburgh, U.K., April 4-8, 2005.
  7. Jan Jürjens: Secure Systems Development with UML, Springer-Verlag, 2004.
  8. Jan Jürjens and Pasha Shabalin: Automated Verification of UMLsec Models for Security Requirements, UML 2004, Lisabon, Portugal Oct. 11-15, 2004, LNCS, Springer-Verlag.
  9. Jan Jürjens and Pasha Shabalin: Tools for Critical Systems Development with UML, ETAPS 2005, Edinburgh, 2-10 April 2005, LNCS, Springer-Verlag
  10. Jan Jürjens: Sound Methods and Effective Tools for Model-based Security Engineering with UML, 27th International Conference on Software Engineering, St. Louis, Missouri, USA; May 15-21, 2005, IEEE Computer Society
  11. Dieter Hutter, Axel Schairer: Possibilistic Information Flow Control in the Presence of Encrypted Communication. In Proceedings of the 6th European Symposium on Research in Computer Security (ESORICS 2004), Springer, LNCS 3193, pp. 209-224, 2004
  12. Dieter Hutter: Towards a generic management of change. In Proceedings of the Workshop on Computer-Supported Mathematical Theory Development, International Joint Conference on Automated Reasoning, IJCAR-2004, Cork, Ireland, 2004
  13. Till Mossakowksi, Piotr Hoffman, Serge Autexier, Dieter Hutter: CASL Logic. Part 4 of the CASL Reference Manual, P.D. Mosses (Ed.) Springer, LNCS 2960, pp. 275-324, 2004
  14. Till Mossakowski, Serge Autexier, Dieter Hutter: Extending development graphs with hiding. Journal of Logic and Algebraic Programming, Special Issue on Algebraic Specification and Development Techniques. 2004
  15. Andreas Nonnengart, Georg Rock, Werner Stephan: Verification Support Environment (VSE), Fourth International Workshop on Planning and Scheduling for Space - IWPSS '04, WPP-228
  16. Dieter Hutter: A Management of Change. Ausarbeitung für Dagstuhl Seminar 03451 ``Applied Deductive Verification'', www.dagstuhl.de, 2003

 
Revision 14 Dec 2006