The annual meeting of the GT MFS is organized by the Working Group (GT) "Formal Methods for Security" (MFS) of the GDR Sécurité Informatique. Its goal is to allow everyone in the formal methods community interested in applications to security to meet and discuss these subjects. The meeting welcomes presentations by researchers, including PhD students and practitioners.

In 2025, the meeting will occur from March 18 to 20 (with the possibility to come the day before and leave the day after). It will take place at Le Mont-Dore, France, and is organized by Pascal Lafourcade (Université Clermont Auvergne) and Grégoire Menguy (CEA LIST).

• Submission deadline: January 10, 2025
• Subscriptions open: January 10, 2025
• End of the early subscriptions: February 3, 2025
• Subscriptions deadline: March 1, 2025

• Véronique Cortier(CNRS, Loria, Nancy) :
  • Keywords: Voting protocols, verification
  • Title:  Electronic voting: design, attack, and formal verification
  • Abstract: Electronic voting aims at guaranteeing apparently conflicting properties: no one should know how I voted and yet, I should be able to check that my vote has been properly counted. Electronic voting belongs to the large family of security protocols, that aim at securing communications against powerful adversaries that may read, block, and modify messages. In this talk, we survey how voting protocols work through the example of the French Legislative elections in 2022. We will then see how to analyze them using formal methods and in particular ProVerif, in order to detect attacks at an early stage, or prove security, yielding a better understanding of the security guarantees and the threat model.
    
    
• Jan Reineke(Saarland University) :
  • Keywords: hardware security, verification, synthesis
  • Title: Verification and Synthesis of Hardware-Software Leakage Contracts
  • Abstract: Microarchitectural attacks compromise security by exploiting software-visible artifacts of optimizations like caches and speculative execution. To use modern hardware securely, programmers must be aware of the security implications of these optimizations. Unfortunately, instruction set architectures (ISAs), the traditional abstraction at the hardware-software interface, are an inadequate basis for secure programming: they entirely abstract microarchitectural details and thus fail to capture their security implications. To enable the construction of secure software systems on top of modern hardware, we have recently proposed leakage contracts as a new security abstraction at the ISA level. However, such contracts are only useful once processors are available that are known to satisfy them. In this talk, I will 1. introduce LeaVe, a tool for the verification of register-transfer-level (RTL) processor designs against ISA-level leakage contracts, and 2. a methodology for the synthesis of precise and sound leakage contracts. To scale to realistic processor designs, LeaVe exploits a new decoupling theorem that allows to separate security and functional correctness concerns. LeaVe employs inductive reasoning on relational abstractions to obtain unbounded contract satisfaction proofs and invariant synthesis to automate the process. Using LeaVe and our synthesis methodology, we precisely characterize the side-channel leakage of three open-source RISC-V processors at the ISA level.

The social event will be a hike, so take hiking shoes. 

There is also a swimming pool and a sauna, so take your swimsuit.

• Clara Bertolissi (Aix-Marseille University)
• Sandrine Blazy (University of Rennes)
• Sylvain Boulmé (Verimag)
• Yannick Chevalier (Toulouse University)
• Stephanie Delaune (CNRS)
• Aymeric Fromherz (INRIA)
• Charlie Jacome (INRIA)
• Tamara Rezk (INRIA)
• Alix Trieu (ANSSI)

Swimming pool: everyday from 9:30 am à 7:20 pm

sauna, hammam, jacuzzi: from 10 am to 12 pm and from 4 pm to 7:20 pm

Restaurant :

• Breakfast: 7:30 / 9:30 am
• Lunch: 12 pm
• Dinner: 7 pm