JFLA 2026

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.

The Arm Architecture Formal Team looks after the formalisation of a number of areas of the Arm Architecture.

Historically, the team has looked after the Concurrency Model, which determines which value a Load instruction is Architecturally Allowed to see. To do that, we develop, maintain and enhance a number of tools [1] which allow us to propose, execute, test and amend formalisations of the prose in the Arm Architecture Reference Manual (Arm ARM) [2]. We discuss our proposals with stakeholders and ratify them, after which a (partially automated) transliteration of the formalisation lands back into the Arm ARM. The current scope of the formal Arm Concurrency Model [3] includes some aspects of virtual memory and instruction fetch, and we work assiduously to expand the scope to the entirety of the Architecture [4,5,6,7].

More recently, the team has looked into defining and formalising the Arm Architecture Specification Language (ASL) [8], which is used to describe the behaviour of the instructions of the Arm Instruction Set Architecture (ISA) [9]. Originally this language was a pseudocode without well defined syntax and semantics, and the team has provided a formal definition of both, as well as the Arm Reference type-checker and interpreter [10].

I will give an overview of our work on both topics, as well as some considerations about the accessibility of specifications, whether formal or not.

[1] https://developer.arm.com/herd7

[2] https://developer.arm.com/documentation/ddi0487/latest/

[3] https://github.com/herd/herdtools7/blob/master/herd/libdir/aarch64.cat

[4] https://community.arm.com/arm-community-blogs/b/architectures-and-processors-blog/posts/how-to-use-the-memory-model-tool?_ga=2.204474131.26066257.1591604084-1566025861.1574767315

[5] https://community.arm.com/arm-community-blogs/b/architectures-and-processors-blog/posts/generate-litmus-tests-automatically-diy7-tool

[6] https://community.arm.com/arm-community-blogs/b/architectures-and-processors-blog/posts/running-litmus-tests-on-hardware-litmus7

[7] https://community.arm.com/arm-community-blogs/b/architectures-and-processors-blog/posts/expanding-memory-model-tools-system-level-architecture

[8] https://developer.arm.com/Architectures/Architecture%20Specification%20Language

[9] https://developer.arm.com/documentation/ddi0602/2024-09/Base-Instructions

[10] https://github.com/herd/herdtools7/tree/master/asllib

Iris est un système logique dédié à la vérification de programmes séquentiels et concurrents. Il est issu de la tradition des logiques dites de séparation, qui soulignent l’importance fondamentale du raisonnement local, c’est-à-dire la possibilité de comprendre et de vérifier chaque composant d’un système logiciel indépendamment des autres. On entend par là en particulier la possibilité d’analyser une fonction indépendamment de son appelant et un fil d’exécution indépendamment des autres fils qui s’exécutent de façon concurrente.

Deux des notions fondamentales qui rendent Iris particulièrement riche et flexible, car elles permettent à la fois raisonnement local à propos de chaque acteur et coordination entre l’ensemble des acteurs, sont l’état fantôme séparable et les invariants. Nous proposerons un aperçu de ces notions et de leurs applications. Nous illustrerons également l’utilisation d’Iris en tant que logique embarquée dans l’assistant de preuve Rocq.