Goals and Results
SP1: Methods and Tools
SP2: Academic System
SP3: Correct Industrial
SP4: Biometric Identification
SP5: Project Management
Auf Deutsch, Bitte!
The work that is done in Subproject 1 aims at the integration of different deduction techniques in order to have a continuous verification.
We consider interactive as well as automatic deduction techniques.
The administration of the logical artefacts is managed by a repository that is developed in SP 1.
Furthermore, we develop a verification environment for cryptographie and security, which is used for the formalisation and verification of cryptographic primitives.
The tools and techniques that are developed within SP 1 are all evaluated directly with the help of the applications that are examined in SP2, SP3, SP4, and SP6.
An overview of the structure of SP 1 is given in the following figure.
For the verification of C0 programs, we develop a Big-Step and a corresponding Small-Step semantics.
Based on both semantics a Hoare Logic and a C0 calculus for dynamic logic have been developed.
The verification tools are all based on the mentioned semantics.
In SP 1 we divide automatic methods into automatic theorem proves and special procedures for
The integration of different automatic deduction techniques and the corresponding tools is illustrated in the following figure:
The integration of automatic theorem provers into interactive systems is shown in the following figure.
In addition to these generic techniques there are special procedure for the verification of temporal properties and for the analysis of programs, especially of programs working on pointer structures.
This part of the project handles cryptographic primitives, for example encryption, signatures, or hashing, in a formal way.
Furthermore, we develop and improve methods and techniques for the verification of cryptographic protocols.
The developed methods are evaluated at the early stages of the project with the help of the applications taken from SP 4.
Finally we will implement a verified system consisting of a host, a chipcard terminal, biosensors that are communicating with the help of a cryptographic protocol.
Further work is done with respect to the connection of the symbolic level of protocol verification and
the level of probabilistic protocol models.
The complete picture is given in the following figure.
- proving temporal properties,
- analysing C0 programs,
- analysing cryptographic protocols, and
- execution time analysis.
- Big-Step semantics and Small-Step semantics for C0, which form the semantic basis for the developed verification tools
- There is substantial progress in the correspondence proof between Big-Step semantics und Small-Step semantics
- Hoare Logics for partial and total correctness
- C0-calculus in dynamic logic
- Development method for state based systems working on pointer structures
- Tools for model-checking and termination analysis
- Symbolic shape analysis tool
- Refinement tool for the verification of temporal properties
- Integration of automatic procedures and methods in VSE and Isabelle
- Procedure for the (automatic) analysis of cryptographic protocols
- Implementation of a strategy for the inductive verification of protocols in VSE (SP 4 protocol is verified)
- Refinement of cryptographic protocols has just started
- Formalisation of the mathematical basics of cryptography in Isabelle
- Basic functionality of the repository for the management of developments
- Andreas Podelski, Andrey Rybalchenko: Transition Invariants. Proc. 19th IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland. July 13-17, 2004.
- 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.
- 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.
- Bernd Finkbeiner, Henny Sipma: Checking Finite Traces using Alternating Automata. Formal Methods in System Design, vol 24, pages 101-127. March 2004.
- Bernd Finkbeiner, Sriram Sankaranarayanan, Henny Sipma: Collecting Statistics over Runtime Executions. Formal Methods in System Design. To appear.
- 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.
- Jan Jürjens: Secure Systems Development with UML, Springer-Verlag, 2004.
- 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.
- Jan Jürjens and Pasha Shabalin: Tools for Critical Systems Development with UML, ETAPS 2005, Edinburgh, 2-10 April 2005, LNCS, Springer-Verlag
- 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
- 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
- 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
- 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
- Andreas Nonnengart, Georg Rock, Werner Stephan: Verification Support Environment (VSE), Fourth International Workshop on Planning and
Scheduling for Space - IWPSS '04, WPP-228
- Dieter Hutter: A Management of Change. Ausarbeitung für Dagstuhl Seminar 03451 ``Applied Deductive Verification'', www.dagstuhl.de, 2003