Scientific direction Development of key enabling technologies
Transfer of knowledge to industry

PostDocs : selection by topics

Technological challenges >> Cyber security : hardware and sofware
2 proposition(s).

See all positions

Advanced Runtime Assertion Checking of C Programs

Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire pour la Sûreté du Logiciel

01-10-2020

PsD-DRT-20-0094

Julien.Signoles@cea.fr

Frama-C is a framework for code analysis of C code. E-ACSL is the Frama-C plug-in dedicated to runtime assertion checking. It converts a C program extended with formal annotations into a new C program which checks the validity of annotations at runtime: it behaves in the same way than the input program if all its annotations are valid, or (by default) the program execution stops whenever one annotation is violated. One key feature of E-ACSL is the expressiveness of its specification language which allows the user to describe powerful safety and security properties. Another key feature is the efficiency of the generated code which relies on a custom memory library and dedicated static analyses. Still, many challenging research questions are opened to go beyond the state of the art of runtime assertion checkers and improve E-ACSL significantly. They include (but are not limited to): - runtime assertion checking of axiomatic definitions by relying on synthesis techniques - runtime assertion checking of localized properties that refer to several program points - runtime assertion checking of frame conditions and data dependency properties - runtime assertion checking of properties over real numbers - static analysis for monitor optimisation In the context of the H2020 European project ENSURESEC (2020-2022) that aims at protecting e-commerce by monitoring, the hired postdoc researcher will collaborate with other engineers and researchers at LSL and possibly in other labs, in order to address several of these challenges. She or he will design, formalize and implement innovative solutions, and prove their soundness.

Download the offer (.zip)

Extensive Code Security Analyses for Frama-C

Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire pour la Sûreté du Logiciel

01-10-2020

PsD-DRT-20-0095

Julien.Signoles@cea.fr

Frama-C is a framework for code analysis of C code. In the context of the newly accepted H2020 European project ENSURESEC (2020-2022) that aims at protecting e-commerce, we plan to use Frama-C for detecting security threats in cyber interfaces such as middleware, cryptographic libraries, or communication protocol implementations. The postdoc researcher will adapt existing Frama-C plug-ins and/or design new ones for that purpose. Among others, one important topic is information flow security in order to detect information leakage. In that respect, possible solutions include: - abstract interpretation through the design of a new Frama-C's abstract domain; - runtime verification by taking advantage of unused bits of the Frama-C's shadow memory state; - extending and improving the dedicated hybrid information flow plug-in SecureFlow of Frama-C that allows the user to combine static and dynamic verifications to check non-interference. Another topic of interest is access control enforcement checking that could be performed within SecureFlow, and/or the MetACSL plug-in that allows the user to specify high-level global program properties such as security policies. Designing a dedicated plug-in could also be an option. The postdoc researcher should formalize and implement his/her solutions, prove their soundness and evaluate them on realistic use cases (e.g., provided by ENSURESEC's industrial partners).

Download the offer (.zip)

See all positions