Next talks

MAY 2023

“A new symbolic analysis of WireGuard VPN ” by Sylvain Ruhault (ANSSI)

Date : 12 may 2023
Room : Pétri/Turing

WireGuard is a new Virtual Private Network (VPN), recently integrated into the Linux Kernel and in OpenBSD. It proposes a different approach from other classical VPN such as IPsec or OpenVPN because it does not let users configure cryptographic algorithms but instead relies on a close set of preconfigured algorithms. The protocol inside WireGuard is a dedicated extension of IKpsk2 protocol from Noise Framework. WireGuard and IKpsk2 protocols have gained a lot of attraction from the academic community and different analyses have been proposed, in both the symbolic and the computational model, with or without computer-aided proof assistants. These analyses however consider different adversarial models or refer to incomplete versions of the protocols. Furthermore, when proof assistants are used, protocol models also differ. In this work, we propose a new, unified formal model of WireGuard protocol in the symbolic model. Our model is fully based on processes in the applied Pi- alculus, the language used by the automatic cryptographic protocol verifier Sapic+. It allows us to automatically generate translations into ProVerif and Tamarin proof assistants. We consider a complete protocol execution, including cookie messages used for resistance against denial of service attacks. Furthermore, we model an adversary that can read or set static, ephemeral or pre-shared keys, read or set ECDH precomputations, control key distribution. Eventually, we present our results in a unified and interpretable way, allowing comparisons with previous analyses. This is joint work with Dhekra Mahmoud and Pascal Lafourcade.

MAY 2023

“Time and Availability in Trusted Execution Environments” by Jan Tobias Muehlberg (Université libre de Bruxelles, Belgium)

Date : 26 may 2023
Room : Pétri/Turing

Trusted Execution Environments (TEEs) can provide strong security guarantees in distributed systems, and even protect embedded software in the IoT or in critical control systems. Measuring the passage of time and taking actions based on such measurements is a common security-critical operation in many of these systems. Yet, few TEEs combine security with real-time processing and availability, or provide hard guarantees on the timeliness of code execution. A key difficulty here is that TEEs execute within an effectively untrusted environment, which can influence expectations on time and progress.
In this talk, I will present our research on categorising approaches to tracking the passage of time in TEEs, highlighting the respective dependability guarantees. Focusing first on the popular Intel SGX architecture, we analyse to what extend time can be securely measured and utilised. We then broaden the scope to other popular trusted computing solutions and list common applications for each notion of time and progress, concluding that not every use case requires an accurate access to real-world time.
Following this, I will present a configurable embedded security architecture that provides a notion of guaranteed real-time execution for dynamically loaded enclaves. We implement preemptive multitasking and restricted atomicity on top of strong enclave software isolation and attestation. Our approach allows the hardware to enforce confidentiality and integrity protections, while a decoupled small enclaved scheduler software component can enforce availability and guarantee strict deadlines of a bounded number of protected applications, without necessarily introducing a notion of priorities amongst these applications.