PI:<\/b> H\u00e9l\u00e8ne Coullon (IMT Atlantique) For-CoaLa is a project funded by the French National Research Agency (ANR-24-CE25-3158<\/a>).<\/p>\n\n\n\n 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. \n<\/p>\n\n\n\n \nOn 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.\n<\/p>\n\n\n\n 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. PI:<\/strong> Nikolai Kosmatov (Thales Research & Technology) V\u00e9DySec is a project funded by the Defense Innovation Agency<\/a> (AID) and managed by the French National Research Agency (ANR-24-ASM2-0001<\/a>) in the ASTRID Maturation programme. <\/p>\n\n\n\n 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 <\/span>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 <\/span>range of projects. The goal of the VeDySec project is to consolidate the techniques and tools for dynamic verification of security properties.<\/p>\n\n\n\n PI<\/strong>: Fr\u00e9d\u00e9ric Loulergue<\/p>\n\n\n\n CoMeMoV is funded by ANR (ANR-22-CE25-0018<\/a>) and is a joint project with CEA List and Thales Research & Technology.<\/p>\n\n\n\n While Frama-C<\/a> 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<\/a>\/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. PI<\/strong>: B\u00e9atrice Boulu-Reshef (LEO, Laboratoire d’Economie d’Orl\u00e9ans) AcceptAlgo is a two-year project funded by R\u00e9gion Centre Val de Loire.<\/p>\n\n\n\n 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.<\/p>\n\n\n\n PI<\/strong>: Jules Chouquet<\/p>\n\n\n\n SeSTeRce means “S\u00e9mantique des Syst\u00e8mes Temporels et R\u00e9actifs” (Semantics of Timed and Reactive Systems). It is funded by Universit\u00e9 d’Orl\u00e9ans in its BQR program.<\/p>\n\n\n\n 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. <\/p>\n\n\n\n PI<\/strong>: Patrice Clemente (SDS team) SIOMediC is a project of INSA Centre Val de Loire and Universit\u00e9 d\u2019Orl\u00e9ans, funded by R\u00e9gion Centre Val de Loire.<\/p>\n\n\n\n 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. PI<\/strong>: Fr\u00e9d\u00e9ric Loulergue<\/p>\n\n\n\n DeSSUF means \u201cA Methodology for the Design of a Safe, Secure and User-Friendly Reactive Programming Language for the Internet of Things\u201d. DeSSUF is funded by ANR via the PIA3 project Athena European University. <\/p>\n\n\n\n In the Internet of Things (IoT), billions of devices are connected. \nVery often, these devices are programmed with the C programming \nlanguage, \nmostly because of the limited hardware resources of such objects. \nHowever, C is error-prone, and software bugs make devices both \nunreliable and \nvulnerable to cyber-attacks. Several cases of massive cyber-attacks \nusing IoT devices are documented. \nMoreover, the IoT is more and more deployed in areas such as energy, \ntransportation and health: it is of paramount importance such systems \nare reliable, safe and secure. The goal of the DeSSUF project is the \ndesign, implementation, and the evaluation of the safety, security \nand ease-of-use of a new programming language for the IoT.<\/p>\n\n\n\n This is a joint project between the University of Orleans<\/a>, LIFO<\/a>, France and the University of Maribor<\/a>, LPM<\/a>, Slovenia both members of the Athena European University<\/a>.<\/p>\n\n\n\n PI:<\/strong> Fr\u00e9d\u00e9ric Loulergue In cooperation with Huawei we have conducted research on the static analysis and generation of imperative BSP (Bulk Synchronous Paradigm) programs.\u00a0 The result of this partnership can be found in Arvid Jakobsson’s PhD thesis https:\/\/tel.archives-ouvertes.fr\/tel-02920363<\/a>\u00a0and in Thibaut Tachon’s PhD thesis.<\/p>\n\n\n\n PI<\/strong>: Fr\u00e9d\u00e9ric Loulergue<\/p>\n\n\n\n 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\u00e9 de Tours.<\/p>\n\n\n\n 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.<\/p>\n\n\n\n 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:<\/p>\n\n\n\n https:\/\/projet-girafon.github.io<\/a><\/p>\n","protected":false},"excerpt":{"rendered":" Ongoing Projects For-CoaLa (2024-2028) PI: H\u00e9l\u00e8ne Coullon (IMT Atlantique)co-PI:\u00a0Fr\u00e9d\u00e9ric 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 … Continue reading “Projects”<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":3,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-228","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/228","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/comments?post=228"}],"version-history":[{"count":21,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/228\/revisions"}],"predecessor-version":[{"id":1313,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/228\/revisions\/1313"}],"wp:attachment":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/media?parent=228"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
co-PI:<\/strong>\u00a0Fr\u00e9d\u00e9ric Loulergue<\/p>\n\n\n\n
https:\/\/for-coala.github.io<\/a><\/p>\n\n\n\nV\u00e9DySec (2025-2027)<\/h3>\n\n\n\n
co-PI:<\/strong> Fr\u00e9d\u00e9ric Loulergue
co-PI:<\/strong> Julien Signoles (CEA List)<\/p>\n\n\n\nCoMeMoV (2023-2026) <\/h3>\n\n\n\n
https:\/\/comemov.github.io<\/a><\/p>\n\n\n\nPast projects<\/h2>\n\n\n\n
AcceptAlgo (2024-2025)<\/h3>\n\n\n\n
co-PI<\/strong>: Fr\u00e9d\u00e9ric Loulergue<\/p>\n\n\n\nSeSTeRce (2023-2024) <\/h3>\n\n\n\n
SIOMediC<\/strong>\u00a0(2023-2024)<\/h3>\n\n\n\n
coPI<\/strong>: Fr\u00e9d\u00e9ric Loulergue<\/p>\n\n\n\n
https:\/\/siomedic.github.io\/<\/a><\/p>\n\n\n\nDeSSUF<\/strong>\u00a0(2022-2023)<\/h3>\n\n\n\n
Static Analysis of BSP Programs<\/strong> (2016-2019)<\/h3>\n\n\n\n
coPI:<\/strong>\u00a0Fr\u00e9d\u00e9ric Dabrowski and Wadoud Bousdira<\/p>\n\n\n\nGirafon (2015-2017)<\/h3>\n\n\n\n