The unverse of modern software is characterized by increasing complexity and ever greater expansion over all areas of society. Penetration of software into numerous critical domains (such as energy, transportation, health, defence, etc.) explains the necessity to ensure its safety and security, and results in a strong need of analysis and verification. This requires powerful and expressive tools, capable to express and treat ever more complex properties of software.

The CEA LIST, based in Palaiseau (near Paris, France), is a key software systems and technology research center working on embedded systems (architecture and design of systems, methods and facilities for software and system dependability, and intelligent vision systems), interactive systems, signal detection and processing in partnership with the major industrial players in the nuclear, automotive, aeronautical, defense and medical fields. The Software Security Lab of the CEA LIST develops tools for verification and validation of software and software/hardware systems. One of these tools, Frama-C (http://frama-c.com), is a framework for analysis of C software. If offers a specification language, called ACSL, and a deductive verification plugin, WP, that allow the user to specify the desired program properties in the form of function contracts and to prove them.

However, some kinds properties that one would like to establish for a given C program cannot be easily specified as function contracts. Thus, one fequently needs to express a relational property invoking several functions, or comparing the results of the same function for different arguments. Groups of functions are often linked by algebraic specifications defining their relationships. Function contracts and classical deductive methods are not suitable for specification and verification of such properties. Some examples of relational preperties include monotonicity of a function (that is, x<=y => f(x)<=f(y)), correct encryption-decryption (e.g. Decrypt(Encrypt(Msg,PrivKey),PubKey)=Msg), parallel program specification (e.g. map(f, map(g, a)) = map (f o g, a) in the MapReduce approach), etc.

This Ph.D. aims at conceiving and developing verification techniques for this kind of properties, their implementation in the context of the Frama-C framework and their application to real-life case studies.

A first step of the work will include design of verification methods in presence of relational properties. During this step, based on the requirements of target applications, a list of types of properties to be considered will be identified, and appropriate solutions to treat them during verification will be proposed. One possible approach to treat different function calls invoked in the property would be creating an additional function that will call individual functions and establish a relation between them at the end. The ACSL specification language will be extended in order to support required properties. Next, these methods will be implemented in the Frama-C framework. Finally, the implemented methods will be applied to verification of case studies.

The candidate will have Master’s degree, or equivalent, in Computer Science, preferably in Software Verification and Validation, and good knowledge of formal methods.

This position is open until it is filled.

Department: Département Ingénierie Logiciels et Systèmes (LIST)
Laboratory: Laboratoire pour la Sûreté du Logiciel
Start Date: 01-10-2015
ECA Code: SL-DRT-15-0518
Contact: Nikolay.Kosmatov<στο>cea.fr