Home

   Consortium

   Project Structure

   Goals and Results

      SP1: Methods and Tools

      SP2: Academic System

      SP3: Correct Industrial
          Hardware/Software-System

      SP4: Biometric Identification
          System

      SP5: Project Management

      SP6: Automotive

      Verisoft Repository

   Publications

   Press

   Contact





   Internal



   Auf Deutsch, Bitte!

Subproject 1: Tools and Methods

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.

TP1-Struktur-eng.gif

Semantics and Interactive Verification

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.

semantik-eng-1.jpg

Integration of Automatic Methods and Techniques

In SP 1 we divide automatic methods into automatic theorem proves and special procedures for
  • proving temporal properties,
  • analysing C0 programs,
  • analysing cryptographic protocols, and
  • execution time analysis.

The integration of different automatic deduction techniques and the corresponding tools is illustrated in the following figure:

Werkzeug-Integration-eng.gif

The integration of automatic theorem provers into interactive systems is shown in the following figure.

Automatische-Beweiser-1-eng.gif

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.

Temporal-Pointer-eng.gif

Cryptography and Security

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.

Krypto-Protokolle-eng.gif

Results

  • 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

Publications

  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
  11. 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
  12. 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
  13. 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
  14. Andreas Nonnengart, Georg Rock, Werner Stephan: Verification Support Environment (VSE), Fourth International Workshop on Planning and Scheduling for Space - IWPSS '04, WPP-228
  15. Dieter Hutter: A Management of Change. Ausarbeitung für Dagstuhl Seminar 03451 ``Applied Deductive Verification'', www.dagstuhl.de, 2003

 
Revision 14 Dec 2006