AnaStaSec

(publicly available)

presentation summary objectives and scientific challenges scientific program meetings and affiliated events participants publications

(restricted access)

deliverables meeting materials

AnaStaSec: scientific program

Static Analysis for Security Properties.


Scientific program

The proposition AnaStaSec describes an ambitious project on the formal verification of security properties for large-scale software-intensive embedded systems. Among the expected outcomes, a set of prototype tools, able to deal with realistic large systems, and the elaboration of industrial security evaluation processes will be designed. The project will focus on the analysis of some case studies provided by Airbus. More precisely, the secrecy and the authenticity of messages in cryptographic protocols envisioned to secure datalink communications will be addressed at model and implementation levels. Then, a large software-intensive system will be analysed. This system is composed of a trusted host platform (including a real-time operating system, communication protocols, routers, application monitoring), some trusted datalink applications implementing air traffic control functions, and some less trusted datalink applications -- the source of which is not available.

The project is made of the following tasks:

  1. The first task focuses on the analysis of communication protocols.
  2. The second task will provide case studies for the analysis of source and binary codes and the formalisation of the security properties of interest. Moreover, a specification of the interactions between the trusted host platform (in C), the trusted applications (in C), and the less trusted applications will be designed, so as to provide a conservative abstraction of the context of each subsystem.
  3. The third task deals with the analysis of C source code. Three case studies will be considered: a host platform, some trusted C applications and the implementation of the protocols of the first task. Static analyzers will be designed so as to detect and prove the properties formalised in second task. Special care will be taken about the diagnosis of alarm: new techniques will be designed to propose compact attack scenarios.
  4. The fourth task concerns the analysis of the less-trusted applications (in binary code) and the proof of their segregation. A modified compiler will be proposed to generate binary codes following a strict discipline. Dedicated static analyzers will be proposed to detect and prove the security properties. In particular, segregation will be guaranteed by verifying that the properties which have been proposed in the second task and assumed in the third task hold.
  5. The fifth task focuses on the evaluation and the dissemination in the industrial community, of security evaluation processes based on static analysis.