Automated symbolic verification of programs and cryptographic protocols in distributed systems

Automated verification of finite- or infinite state distributed systems working in network environments (e.g., in the Internet), performed via an analysis of their state spaces, is a very important and dynamic area of research, which brings promissing practical results. In the course of the previous project Automated verification of time dependent systems our group developed a model checker VerICS (available at http://pegaz.ipipan.waw.pl/~verics/), which was presented at one of the main international conferences on verification - "Tools and Algorithms for Construction and Analysis of Systems" (TACAS'03), and at the main Polish conference on real-time systems "Systemy Czasu Rzeczywistego" (SCR'03). Moreover, its results were published in more than 30 papers, which resulted in a high note given to the project by the State Committee for Scientific Research. The above-mentioned grant was directed towards theoretical problems (i.e., obtaining new verification methods, supported in a mathematical way). Conversely, the current project is orientated to practical aims, and its main goals are to prepare a programming environment enabling an easy access to VerICS, and to apply the model checker to verification of distributed software systems and cryptographic protocols.

Summing up, our current aims cover not only obtaining new theoretical results in the area of symbolic verification (i.e., in verification by a translation to SAT ¹) for systems specified in high-level languages and cryptographic protocols, but also extending VerICS in a way which will enable automated verification of these systems. To this aim we are going to deal with the following problems: firstly, for verification purposes, the main model used in our system - i.e., networks of standard timed automata - will be extended by adding operations on integer variables performed while action steps, and the main model checker module BMC (bounded model checking) will be modified to handle that extension. Next, we are going to add a new verification module UMC (i.e., unbounded model checking), which shall enable proving correctness of timed systems in a symbolic way, by a translation to SAT. In order to build the programming environment we need to develop methods of translating programs written in high-level programming languages either to networks of extended timed automata, or to the VerICS' intermediate language IL. The current version of the system supports translations from a subset of Estelle (a language used mainly for specifying telecommunnication protocols). In the future, we are going to work on translations (combined with reductions) for important fragments of the specification/programming languages Promela, Timed-UML and Java. The task is particularly difficult for UML, since this language has no precise semantics, and therefore for translation purposes such a semantics has to be defined. Choosing the three above languages is justified by the fact that Java is widely used in object-oriented programming, and UML - to specifying distributed systems. Promela will enable extending VerICS by methods and solutions proposed for the existing model checker SPIN.

Our plans include also developing new methods of verification of cryptographic protocols used for authentication in telecinformatic networks, and implementing them in our system. Applying VerICS to testing cryptographic software is one of the most important goals of the project. The above goal is to be reached by defining a method for specifying the protocols (including also these with timing dependencies) in one of the supported input languages, or by proposing a new input language designed especially to this aim. For specifying protocols' properties the logics TCTL or CTL augmented with deontic and knowledge operators will be used.

back