IUT2 Grenoble, salle 315, 3me étage
Adresse : 2 place Doyen Gosse, 38000 Grenoble
Plan et itinéraire : https://maps.app.goo.gl/khzeayyfAMcKirsJ6
Pour toute inscription ou modification d'inscription tardive,
merci de contacter par mail les animateurs de MTV2. La liste des inscrits est sur
https://framadate.org/Hbcxcu2ARNLWJHjS
Talks can be given in French or in English. Since some part of the audience might not be fluent in French, it is recommended to have the presentation slides in English.
10h00-10h40 Accueil, café / Arrivals, welcome coffee
10h40-10h45 Ouverture de la journée / Opening. Nikolai Kosmatov, Natalia Kushik, Pascale Le Gall, Antoine Rollet
10h45-12h15 Session 1.
Finding Backdoors with Protocol-Aware Fuzzing. Alexandre Doyen (CEA List)
An Efficient and Versatile Approach to Shortest Path Problems in Interprocedural Programs. Theo De Castro Pinto (LaBRI)
Runtime Verification of Inductive Predicates with E-ACSL. Jan Rochel (CEA List)
12h15-13h30 Déjeuner / Lunch
13h30-15h10 Session 2.
Exposé invité / Invited talk. Modelling, Runtime Analysis and Optimization of Business Processes. Gwen Salaün (Université Grenoble Alpes)
(Exposé court/Short talk) Formal Verification of Consent Properties in a Data Protection by Design and by Default Approach. Myriam Clouet (LIFO)
(Exposé court/Short talk). Neuro-symbolic approach to generate a test repository. Eléa Jacquin (FEMTO-ST)
15h10-15h50 Pause café / Coffee break
15h50-17h20 Session 3.
On the use of anti-unification for composing interactions via gate connection. Joel Nguetoum (CEA List)
Specification Theories, Reloaded Relationally. Uli Fahrenberg (LMF)
Formal Study of Algorand's Byzantine Agreement Algorithm. Hubert Garavel (INRIA, LIG)
17h20. Fin de la journée / End of the workshop.
The duration of a regular talk is 30 min (20-25 min talk + questions & answers).
The duration of a short talk is 20 min (10-15 min talk + questions & answers).
The duration of an invited talk is 60 min (50 min talk + questions & answers).
Exposé invité: Gwen Salaün (Université Grenoble Alpes).
"Modelling, Runtime Analysis and Optimization of Business Processes".
A business process is defined as a set of tasks executed in a certain order to achieve a specific goal. BPMN has become the standard modelling language for describing and developing business processes. One of the main challenges in the business process management area is to provide techniques and tools for analyzing and optimizing processes, which is necessary for avoiding unexpected process executions or for making these executions more efficient in terms of execution times or resource usage. In this talk, we will present several results in this context, namely (i) the automated generation of BPMN processes from textual descriptions using LLM, (ii) the formal verification of functional and quantitative properties on BPMN processes, and (iii) the optimization of processes via resource allocation or process refactoring.
An Efficient and Versatile Approach to Shortest Path Problems in Interprocedural Programs (Theo De Castro Pinto - LaBRI)
This talk addresses the shortest path problem for weighted interprocedural automata (WIPA), a simple model adapted to the analysis of low-level programs. We propose an efficient and versatile approach, relying on Knuth's generalization of Dijkstra's algorithm to context-free grammars. Several variants of the problem are considered in the paper, depending on the starting and ending stacks. Moreover, we solve both the single-source and single-target versions. Each problem is translated into a succinct context-free grammar, permitting the efficient computation of a solution in O(n log(n) + m) time, where n and m are the number of states and transitions in the underlying WIPA. We provide experimental results on real-size programs showing the scalability of the approach.
Formal Verification of Consent Properties in a Data Protection by Design and by Default Approach (Myriam Clouet - LIFO) (exposé court)
Nowadays, computer systems process large quantities of personal data. Many laws and regulations have been established around the world to regulate personal data processing for preventing privacy issues. In Europe, GDPR requires Data Protection by Design and by Default (DPbD). To fulfill this requirement, it is necessary to verify that the system respects privacy properties, including consent- related properties, at different steps of its development. We propose a refinement-based solution using runtime verification to be used in such a stepwise verification process. For that we use CASTT and IAT, an offline runtime verification tool for interaction models. CASTT is a formal privacy verification tool targeting two widely different abstraction levels of systems, namely high-level graphical models and C programs. Here, we extend it to also verify systems at an intermediate level of abstraction by considering formal interaction models. To do so, we rely on the trace mechanism of CASTT and on a new translation mechanism to IAT. We empirically evaluate the correctness and the efficiency of this mechanism. We also define methodical refinement steps to allow our solution to be included in a privacy-minded refinement process, from graphical models to formal interaction models to C code.
Specification Theories, Reloaded Relationally (Uli Fahrenberg - LMF)
Models and specifications are central objects in theoretical computer science, and many formalisms exist for constructing models, devising specifications, and checking models against specifications. Yet there appears to be no agreement on an underlying theory of specifications. Standing on the shoulders of Pnueli (1985), Hennessy-Milner (1985), and Larsen (1990), we develop a relational theory of specifications. One of the advantages is that specifications for preorders (e.g., simulation or subsumption) work out of the box, and that notions up-to equivalence may be treated on-the-nose. It also seems that quantitative generalizations are easier to obtain than in previous settings. Joint ongoing work with Paul Brunet (LACL).
Tulip: Finding Backdoors with Protocol-Aware Fuzzing (Alexandre Doyen - CEA List)
Code-level backdoors are hidden functionalities embedded in source code that enable unauthorized access or privilege escalation when triggered by specific, secret inputs. A typical example is the injection of hard-coded credentials into a file server’s codebase, allowing attackers to compromise all deployed instances globally. Such backdoors have been observed in real-world supply-chain attacks targeting open-source software and embedded network daemons. Greybox fuzzing—an automated testing technique that combines randomized input generation with lightweight instrumentation—has proven effective for discovering memory-safety vulnerabilities. However, its application to backdoor detection remained largely unexplored until the recent emergence of the Rosa tool, which demonstrated that general-purpose fuzzers like AFL++ can be repurposed for this task. While Rosa significantly advanced automation compared to earlier approaches, the current state of the art still suffers from a critical limitation: the generation of false alarms that require manual vetting. To address this, we present Tulip, a protocol-aware greybox fuzzing framework specifically designed to detect backdoors in implementations of application-layer network protocols, such as web and file server programs. By specializing in such programs—where most known backdoors reside—Tulip can leverage dedicated protocol models to identify backdoor-triggering behaviors without producing false alarms. These models can also guide the fuzzer towards input sequences more likely to expose backdoor logic. We evaluate Tulip across 14 backdoors affecting 4 widely used protocols (HTTP, FTP, POP, and IMAP), including 7 authentic samples from real-world attacks, five of which are CVEs. Our results show that Tulip consistently avoids false alarms and, in most cases, detects backdoors faster than Rosa.
On the use of anti-unification for composing interactions via gate connection (Joel Nguetoum - CEA List)
Interaction languages provide a formal framework for specifying and formally verifying distributed systems. Interaction models are represented as terms and depicted using UML sequence diagrams, which describe coordinated message exchanges in distributed systems governed by sequencing, parallel, repetitive, and alternative algebraic operators. Our work aims to develop an algorithmic method for interaction composition, which is the process of constructing a global interaction of a distributed system from the local interactions of its subsystems. In local models, an emission of a message to the environment paired with the reception of the same message in another local model is termed complementary actions, linked by a shared object called a gate. To compose interactions, we rely on a specialization of anti-unification, introducing constant-preserving anti-unification, a variant that enforces the preservation of shared gate constants while generalizing local interactions that do not involve gates into a coherent generalizer representing the resulting global model. The composition is then formalized as anti-unification modulo the algebraic laws of interaction operators (associativity, commutativity, and unit) so that the resulting model preserves the structure of local interactions while reorganizing them into a consistent global view by connecting complementary communications.
Runtime Verification of Inductive Predicates with E-ACSL (Jan Rochel - CEA List)
Formal languages for software verification may include a syntax for defining predicates in an inductive manner. This facilitates inductive reasoning, a readily employed technique in the context of automated deductive verification. There are currently no known methods for the runtime verification of inductively defined predicates (inductive predicates for short). The usual fixpoint semantics of inductive predicates does not suggest any obvious method for how they may be executed in order to verify whether they are true or false for some given arguments. With a view to runtime verification of inductive predicates, this work presents a three-valued semantics of E-ACSL inductive predicates and a semantics-preserving translation of a subset of such predicates into an easy-to-execute form. An implementation of this translation has been added to the E-ACSL plug-in of Frama-C.
Neuro-symbolic approach to generate a test repository (Eléa Jacquin - FEMTO-ST) (exposé court)
The presentation outlines the approach proposed in my thesis, which aims to use an AI assistant to automatically generate tests from models. First, the assistant generates the model and requirements from the specifications written in natural language. The model is then validated against the requirements. Symbolic techniques take over to calculate test data. The goal is to provide a tool that leverages the advantages of LLMs while allowing the validation engineer to control and correct each step.
Formal Study of Algorand's Byzantine Agreement Algorithm (Hubert Garavel - INRIA, LIG)
Algorand is a promising blockchain technology targeting at decentralization, scalability, security, and energy savings. At the heart of Algorand is a BBA* (generalized Binary Byzantine Agreement) protocol, a formal model of which was developed in LNT by Marco Bernardo and Andrea Esposito (University of Urbino, Italy). Starting from this formal model, we explore several variants of the protocol, by applying both Algorand-specific and LNT-generic transformations, in order to obtain a model as concise as possible. We then verify this model using a combination of techniques supported by the CADP tools, namely visual checking, equivalence checking, and model checking.
La réunion aura lieu à l'IUT2 (2 Place Doyen Gosse, 38000 Grenoble), dans la salle 315, au 3me étage. Le bâtiment a une entrée principale côté place Doyen Gosse et une seconde entrée côté rue d'Arsonval (côté garage à vélos). Nous conseillons de privilégier l'entrée principale (côté place Doyen Gosse). Si vous entrez côté rue d'Arsonval, il faut traverser la cour pour rejoindre le hall. Un ascenseur est accessible depuis la cour du bâtiment, il faut s'adresser à l'accueil pour pouvoir y accéder. Téléphone accueil : 04 76 28 45 09. Le déjeuner se fera sur place (malheureusement, nous ne pouvons pas garantir l'adéquation du repas en cas de contraintes alimentaires). L'entrée principale est visible sur la photo sur https://iut2.univ-grenoble-alpes.fr/l-iut2/batiments-et-acces/
Les animateurs du groupe MTV2 : Nikolai Kosmatov, Natalia Kushik, Pascale Le Gall, Antoine Rollet
Les organisateurs locaux : Yves Ledru, Sophie Dupuy-Chessa, Nicolas Hili, Yann Laurillau, Lydie du Bousquet, Gabriela Gonzalez-Saez