ABZ 2023 (Nancy, France)

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 will see how to design secure electronic voting protocols and how to analyze them using formal methods, in order to detect attacks at an early stage, or prove security. This yielded several enhancements of ProVerif, a state-of-the-art tool for anaysing security protocols.

The VerCors verifier is a tool set for the verification of parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. In this talk I will first give an overview of the VerCors verifier, and how it has been used for the verification of many different parallel and concurrent algorithms. In the second part of my talk I will zoom in on verification of GPU programs, as they are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone. In my talk I introduce Alpinist, an annotation-aware GPU program optimizer. It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. We evaluate Alpinist, in combination with the VerCors program verifier, to automatically optimize a collection of verified programs and reverify them.