Teilprojekt 1: Werkzeuge und Methoden

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

Semantik und interaktive Verifikation

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 Einbindung automatischer Beweiser in die interaktiven Beweissysteme ist im folgenden Schaubild verdeutlicht.

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

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.

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