Deep Learning for improving formal verification with Frama-C / Eva

Institution

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development, and innovation. Drawing on the widely acknowledged expertise gained by its 16,000 staff spanned over 9 research centers with a budget of 4.1 billion Euros, CEA actively participates in more than 400 European collaborative projects with numerous academic (notably as a member of Paris-Saclay University) and industrial partners. Within the CEA Technological Research Division, the CEA List institute addresses the challenges coming from smart digital systems.

Among other activities, CEA List’s Software Safety and Security Laboratory (LSL) research teams design and implement automated analysis in order to make software systems more trustworthy, to exhaustively detect their vulnerabilities, to guarantee conformity to their specifications, and to accelerate their certification. In particular, the Frama-C platform is dedicated to perform a wide range of analyses over C programs (with an experimental C++ front-end).

Objectives

Inside Frama-C, the Eva plugin provides several static analysis techniques dedicated to the automatic inference of program properties and, in particular, runtime errors (arithmetic overflows, invalid memory accesses and other C undefined behaviors). These techniques are efficiently combined, but their activation can be expensive in terms of resource consumption (time and memory). It is therefore necessary to choose wisely which techniques to use in which case.

These choices are now made by the analyst, who uses the tool to perform safety proofs on a software. They require a detailed knowledge of Frama-C and its analysis techniques, both of which evolve with time. Moreover, to be as fine as possible, these choices can be made at the function or loop level in a sometimes large source code. This double difficulty, based on both the quantity of knowledge and the time needed, can be a blocking obstacle.

To remove this obstacle, we have implemented promising machine-learning techniques. This involves treating the difficulty no longer as a problem of understanding the analysis tool but as a problem of understanding the relation between code patterns and the different analysis techniques. This has two advantages. On the one hand, the learning can be repeated as the tool evolves, in order to remain adapted to the characteristics of the latest available techniques. On the other hand, the automatic choice of techniques can be done at a much finer level than what a human can accomplish in a reasonable time.

The objectives of the internship are to contribute to our machine-learning toolchain specialized on source code, to participate in its integration in Frama-C, and to improve its performance in the automatic selection of analysis strategies. Several internship directions are possible:

• Investigate and develop specialized learning techniques on graphs (in particular, Graph Neural Networks),
• Explore learning techniques in the presence of unbalanced data
• Study and develop a distributed version of the toolchain capable of fully leveraging the resources of our cluster FactoryIA.

All positions include theoritical research as well as prototyping and experimental evaluation.

Qualifications

• Minimal

  • Final-year master student in Computer Science or Computer Enginnering
  • Solid ability in Python programming
  • Solid ability with deep learning frameworks (TensorFlow or PyTorch)
  • ability to work in a team

• Preferred

  • A certain taste for mathematical matters
  • Some knowledge of functional programming, preferably OCaml
  • Some knowledge of imperative programming, preferably C

Characteristics

• Duration: 5-6 months

• Location: CEA Nano-INNOV, Paris-Saclay Campus, France

• Compensation:

  • €700 to €1300 monthly stipend (determined by CEA compensation grids)
  • maximum €229 housing and travel expense monthly allowance (in case a relocation is needed)
  • CEA buses in Paris region and 75% refund of transit pass
  • subsidized lunches

Application

If you are interested in this internship, please send to the contact persons an application providing the following information:

• Your resume;
• A cover letter indicating how your curriculum and experience match the qualifications expected and how you would plan to contribute to the project
• Your bachelor and master transcripts
• The contact details of two persons (at least one academic) who can be contacted to provide references.

Applications are welcomed until the position is filled. Please note that the administrative processing may take up to 3 months, so we encouraged interested students to take contact as soon as possible.

Contact persons

For further information or details about the internship before applying, please contact:

• Michele Alberti (michele.alberti@cea.fr)
• Valentin Perrelle (valentin.perrelle@cea.fr)