Ongoing Projects
For-CoaLa (2024-2028)
PI: Hélène Coullon (IMT Atlantique)
co-PI: Frédéric Loulergue
For-CoaLa is a project funded by the French National Research Agency (ANR-24-CE25-3158).
Large distributed software systems (applications or infrastructures) are now ubiquitous, with component-based systems (e.g., service-oriented architectures or microservices) offering a convenient way to structure large systems, in particular distributed systems deployed in the Cloud, in the core, or at the edge of the network. DevOps operations, that include system configurations and reconfigurations, are required to handle various kinds of scenarios such as fault tolerance, scalability, software updates, or various optimizations, etc. Such changes may lead to faults. A study of 597 unplanned outages that affected popular cloud services between 2009 and 2015 found that 16% of them were caused by a system upgrade.
On the one hand, many configuration tools and languages exist in the DevOps community, some of them being specific to the provisioning of resources in Cloud providers, packaging problems, containerized deployments, configuration of applications or infrastructures, etc. The main advantage of these tools is their full integration and adoption in the DevOps community. Their disadvantage is they lack both formal and textual specifications. Moreover, their contours are blurred. On the other hand, many initiatives have been studied in academia to contribute to the deployment, configuration, and reconfiguration of distributed software, bringing improvements such as expressivity, speed, safety, etc. Many come with precise and sometimes formal definitions. However, they lack the breadth of the mainstream DevOps tools.
The goal of For-CoaLa is twofold: (1) understand and bridge the gap between a popular tool from the DevOps community (Ansible) and a tool from academia (Concerto); (2) improve the understanding of these languages based on mechanized formal semantics and develop verified semantic-preserving cross-language transformations.
https://for-coala.github.io
VéDySec (2024-2026)
PI: Nikolai Kosmatov (Thales Research & Technology)
co-PI: Frédéric Loulergue
co-PI: Julien Signoles (CEA List)
VéDySec is a project funded by the Defense Innovation Agency (AID) and managed by the French National Research Agency (ANR-24-ASM2-0001) in the ASTRID Maturation programme.
Security risks have become un major concern during the recent years. A security flaw can be exploited by attackers and allow them to steal confidential data (personal, medical, financial, industrial, defence, etc.), to access services without authorisation, or to modify or to compromise sensible data with a malicious goal (identity usurpation, espionage, hybrid war, terrorism, etc.) Static verification techniques, namely by abstract interpretation or deductive verification, can demonstrate the absence of vulnerabilities in a software product. However, these techniques remain difficult and expensive to apply on industrial software. Indeed, their application requires deep expertise and significant effort. In this context, developing dynamique verification techniques for security properties, easier to apply than static techniques, is necessary for application of these techniques to a large range of projects. The goal of the VeDySec project is to consolidate the techniques and tools for dynamic verification of security properties.
AcceptAlgo (2024-2025)
PI: Béatrice Boulu-Reshef (LEO, Laboratoire d’Economie d’Orléans)
co-PI: Frédéric Loulergue
AcceptAlgo is a two-year project funded by Région Centre Val de Loire.
Individuals have seen their exposure to algorithms increase considerably over the past decade. This exposure is exercised mainly in direct interaction with computers, telephones or other connected objects, during many moments of the social and economic life of individuals, but also in administrative or technical procedures of professionals. Individuals interact with algorithms when searching for information on the internet, when using connected medical devices, when delegating the management of their savings and retirement or when making online purchases. This research project aims to study how individuals evaluate and accept algorithms presented in mathematical form and in simple language form i.e. with words intelligible by individuals. It consists in measuring the acceptability for individuals of the algorithms presented through these simplified explanations.
CoMeMoV (2023-2026)
PI: Frédéric Loulergue
CoMeMoV is funded by ANR (ANR-22-CE25-0018) and is a joint project with CEA List and Thales Research & Technology.
While Frama-C was successfully used for deductive verification in various case studies, recent industrial applications conducted at Thales Research and Technology demonstrated the need for significant enhancements of the tool to make it possible to efficiently and soundly realise deductive verification of real-life industrial software products with >10k lines of code mixing complex data-structures, dynamic memory allocation and low-level constructs such as bitfields, unions and memory casts. The Frama-C/WP plugin provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial strength programs, this combination already makes WP mature enough to be deployed for proving industrial critical embedded software. However, several theoretical and practical issues still persist. The goal of CoMeMoV (Collaborative Memory Models for formal Verification) is to tackle these issues to scale on deductive verification of complex programs.
https://comemov.github.io
SeSTeRce (2023-2024)
PI: Jules Chouquet
SeSTeRce means “Sémantique des Systèmes Temporels et Réactifs” (Semantics of Timed and Reactive Systems). It is funded by Université d’Orléans in its BQR program.
The Internet of Things comes in the form of devices, most often connected to a multitude of other devices; these connections consist of a permanent and uninterrupted exchange of data. Some applications, in the medical field for example, require a very high degree of trust and security in the implemented software. The analysis and verification of these programs (known as reactive) is therefore a crucial issue, both scientific and social, at the heart of the themes of the PI. The project takes a fundamental and exploratory approach to these questions, from the point of view of theoretical and mathematical analyses.
SIOMediC (2023-2024)
PI: Patrice Clemente (SDS team)
coPI: Frédéric Loulergue
SIOMediC is a project of INSA Centre Val de Loire and Université d’Orléans, funded by Région Centre Val de Loire.
Digital health and in particular Connected Medical Devices (CMD) are experiencing rapid growth. Unfortunately, the numerous and recurring vulnerabilities of these devices present major confidentiality problems for medical data and significant dangers for the physical integrity of individuals. Our work aims to make DMCs safer (free from software bugs) and more secure (resistant to external attacks). We want to propose new protocols for interconnecting DMCs in their environment (hospital or domestic) and access control models, adapted to these different uses (often wireless). The goal is then to protect the DMCs from external attacks. We also want to be able to provide guarantees that neither the codes (programs) embedded on the DMCs, nor the protocols and protection mechanisms that we add to them, present any vulnerabilities. The main deliverables will be reusable software components.
https://siomedic.github.io/
Past projects
DeSSUF (2022-2023)
PI: Frédéric Loulergue
DeSSUF means “A Methodology for the Design of a Safe, Secure and User-Friendly Reactive Programming Language for the Internet of Things”. DeSSUF is funded by ANR via the PIA3 project Athena European University.
In the Internet of Things (IoT), billions of devices are connected. Very often, these devices are programmed with the C programming language, mostly because of the limited hardware resources of such objects. However, C is error-prone, and software bugs make devices both unreliable and vulnerable to cyber-attacks. Several cases of massive cyber-attacks using IoT devices are documented. Moreover, the IoT is more and more deployed in areas such as energy, transportation and health: it is of paramount importance such systems are reliable, safe and secure. The goal of the DeSSUF project is the design, implementation, and the evaluation of the safety, security and ease-of-use of a new programming language for the IoT.
This is a joint project between the University of Orleans, LIFO, France
and the University of Maribor, LPM, Slovenia both members of the
Athena European University.
https://dessuf.github.io/
Static Analysis of BSP Programs (2016-2019)
PI: Frédéric Loulergue
coPI: Frédéric Dabrowski and Wadoud Bousdira
In cooperation with Huawei we have conducted research on the static analysis and generation of imperative BSP (Bulk Synchronous Paradigm) programs. The result of this parternship can be found in Arvid Jakobsson’s PhD thesis https://tel.archives-ouvertes.fr/tel-02920363 and in Thibaut Tachon’s PhD thesis.
Girafon (2015-2017)
PI: Frédéric Loulergue
The GIRAFON project was funded by the Centre Val de Loire Region (APR-IA GIRAFON) and was a joint project with the CA, PAMDA, SDS Teams of LIFO, and LIFAT, Université de Tours.
The objective of the GIRAFON project was to design generic algorithms for mining large graphs based on a rich query language and distributed execution environments accompanied by dedicated programming libraries, while taking into account the protection of the privacy of individuals.
This objective was divided into four tasks which led to the development of software prototypes serving as proof of concept of the relevance of the proposed approaches, and which were evaluated in distributed computing environments: