ENSTA Bretagne : sécurité informatique

Processes For Safe And Secure Software And Systems (P4S team)

The team’s interest is in methods and tools for specifying and describing systems and software, with a view to assessing and analyzing their performances. This will, in turn, increase user confidence and guarantee the operating safety and security of digital systems.

Enhance the operating safety and security of digital systems: methodological strands

  • System modeling to describe the needs of the system under study
  • Modeling of construction processes and their improvement, which is critical for the safety, and security of and, more generally, confidence in, the system studied.
  • Federation of models since varying viewpoints need to be merged.
  • Free modeling to enable specific viewpoints to be developed, as no framework can encompass all viewpoints.
  • Formal verification at all levels: intra-model and inter-model.
  • As well as automated and semi-automated methods alike.

Expertise

  • Model-driven engineering,
  • Software engineering,
  • Software verification
  • Product lines
  • (Self) adaptive systems
  • Cognitive systems
  • Requirements engineering
  • Formal specification
  • Diagnosis
  • Executable semantics, 
  • Formal verification
  • Debugging 

Collaborations

  • Companies: Airbus, Thales, PragmaDEV, Kereval, Davidson, Lucio-Zekat
  • Institutions: DGA, CEA
  • Academia: IRISA
  • Research Groups: GPL, SOC2
Examples of research programs
Oneway project: Modeling capacities and digital analysis of a Product Development Plan

Against a fiercely competitive global economic backdrop, the aeronautical industry is one of France’s strengths. With a fabric of small, medium and large companies, the French aeronautics sector is the only one, along with the United States, that is fully capable of developing, producing and marketing civil and military aircraft. The French Government has developed a plan for supporting the aeronautics sector, designed to protect French expertise and know-how, while delivering the far-reaching changes needed to achieve the energy transition. The strategy is focused on the green transition and lowering carbon emissions in air transport.

The French aeronautical industry’s expertise on its products, programs and interactions within its value chain is widely recognized. For all that, it must contend with a growing number of challenges if it is to become more proficient in its design and development cycles and more efficient in its engineering activities and ensure that the performances of its products and support systems continually improve. It also needs to take technological innovations more swiftly on board and take advantage of the opportunities offered by new information technologies. Given these challenges, there is an inevitable need for radical changes to engineering methods within the French aeronautical industry, and this is where the ONEWAY project comes in. 

The project began in May 2021, for an 18-month period, with a budget of €48m. It brought together 14 partners: Airbus, Dassault Aviation, Liebherr Aerospace, Safran Electrical & Power, Safran Aerotechnics, Thales, Altran Technologies, Cap Gemini, Sopra Steria, CIMPA, PragmaDEV, IMT Mines Ales, Université de Rennes 1 and ENSTA Bretagne.

ENSTA Bretagne helped to define a digital capacity for supporting decisions regarding launch, then control and management of a Product Development Plan (PDP). The PDP seeks to predict and control the best date for a product and its industrial system to be brought to the market, as well as the expected production ramp-up stage. This has become crucial for the competitiveness of the French aeronautical industry.

Thanks to the experience of ENSTA Bretagne’s Processes for Safe and Secure Software and Systems (P4S) team on federating complex software systems, the development of formal semantics and analytical algorithms, an equipped PDP modeling framework has been established. The tool developed allows for a detailed capture of the business specifics, industrial-scale simulation of the development process and validation of the models built through formal verification methods. 

For ENSTA Bretagne, the two main implications in the ONEWAY project concern the formal verification and validation of the PDP. Project outcomes:

  1. Extension of the OBP2 model-checker with statistical exploration algorithms for massive testing on industry-derived models;
  2. Improvement of the layer of expression of formal properties associated with the system requirements or Top Program Objectives;
  3. Invention of a modular strategy for the formal verification of time-bound systems, based on the PDP’s formal semantics without the need for costly model processing procedures. 

Specification and formalization of secure software and hardware architecture
  • Cyber-security modelling and analysis framework" research project: Developing a cohesive framework for the specification, formalization and analysis of secure software and hardware architecture
  • in progress since December 2020
    funded by the AID (Defense Innovation Agency)
  • led by Raul Mazo Pena, a research professor at ENSTA Bretagne / Lab-STICC (SHARP department, P4S team)

To find out more: read the article on this program

It is still early days for the "Security by Design" approach and significant R&D efforts will be required for its use to become systematic and widespread. That’s the aim of this groundbreaking project, which is in some ways opening up a whole new engineering discipline by outlining a new vision. To take up this challenge, the project sets out to create a cohesive, overarching theory, with systematic design tools, techniques and methods.

Ker-Seveco: connected vehicle security
  • Project funded by the Brittany Region and FEDER
  • started at the end of 2019 until 2022
  • 3 partners: KEREVAL, Mobility Tech Green and ENSTA Bretagne
  • led by: Joël Champeau, a research professor at ENSTA Bretagne, UMR (joint research unit) Lab-STICC (SHARP department, P4S team

The project sets out to develop products and services embedded in connected vehicles, as well as associated off-board services.

These on-board services will have gone through a secure development process.

ENSTA Bretagne’s contribution involves developing a design methodology and tooling of cybersecurity tests specially geared towards "connected vehicles".

This method will need to range from the system level, factoring in the security requirements, to the communication modules of the embedded calculator.

The expected results of the project are the development of such new mobility services as fleet management, development of a CyberLab to run the security tests of the services and a methodological support grounded in a formal verification of the security requirements.

 

Modeling and monitoring of security contracts in a "Secure by design" approach

...

contact

Ciprian Téodorov
Associate Professor
IT Departement
Lab-STICC laboratory / SHARP Department / P4S Team
+33 (0)2 98 34 89 53