Students should be aware of the foundations and limits of each approach in order to be able to understand or to define verification requirements for a given application and then to carry out appropriate verification operations.
Two topics (Testing, System Verification, Verification of Cryptographic protocols) will be teached every year.
Testing. Test is the most common verification method applied in industrial development projects. To meaningfully apply testing techniques, knowledge on its foundations and restrictions is essential. A first objective of this course is to explain the basic notions and the theoretical foundations of (software) testing. These basic notations are, for instance, defined on labelled transition systems and Mealy automata. A second aim of this course is to show that the existence of a formal framework makesit possible to automate to a large extent test case generation, test execution and test evaluation. We present approaches for which tools exist implementing model-based testing.
System verification. In the case of certain critical functionalities or systems, it is desirable to go beyond testing in order to be able to actually guarantee some critical properties: absence of bad behaviours (safety properies) or actual proof of well-functioning (progress properties). The aim of this part is to present some basic models and techniques for modelling systems and their properties, and to introduce some corresponding analysis methods for finite state models.
After a short introduction of the general problem and the intinsic difficulty of solving the verification problem, we introduce a basic model for the representation of systems at any level of abstraction. This model is based on transition systems and allows representing systems modularily, with the help of a parallel composition operator. Then, we first consider the verification of safety prperties (the simpler problem) and then the verification of progress properties, starting from some very simple ones. We will also introduce, respectively revise, some basic underlying theories, such as the theory of fixpoint computation.
Verification of cryptographic protocols. Nowadays secured applications are present everywhere : e-banking, mobile phone, electronic voting, secured web site ... All these applications use cryptographic protocols. These protocols assure the confidentiality and integrity of exchanged messages but offer also some other functionalities : authentication, fairness, privacy ... The aim of this part is to provide some theoretical foundations and to illustrate some techniques used to design and analyze security protocols.
After a short introduction to cryptography in general, and cryptographic protocols in particular, we present the symbolic (Dolev-Yao) model. Throughout examples, we give the theoretical foundations of cryptographic verification. During one lab session, we apply existing tools for illustrating the studied methods on some examples. Students will by them-self prove secure or find some flaws using automatic tools. Then, we take a look to the computational model and the faithfulnesss of the symbolic model with respect to this model.
Program summary :
A basic software engineering course, basic notions of logic and of automata theory (some knowledge on models for concurrency and model-checking techniques would be a plus).
Semestre 9 - L'examen existe uniquement en anglais
Semestre 9 - Le cours est donné uniquement en anglais
mise à jour le 15 janvier 2017