MAY 2023
|
“A new symbolic analysis of WireGuard VPN ” by Sylvain Ruhault (ANSSI) Date : 12 may 2023 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 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. |