Description
In the recent years, formals methods for security and their associated tools have been used successfully both to find novel and complex attacks on many protocols [A] and to help in their standardization process. They however face a new challenge with the increasing probability of quantum computers coming into the real-world: we need to be able to provide guarantees against quantum attackers.In this talk, we will first present a broad overview of formal methods, outlining what is the general goal of the field and how we have strived toward it. We will then focus on the post-quantum issue by presenting the corresponding concrete challenges, and thus multiple ways current computational proofs of security (proof for any Polynomial Time Turing Machine attacker) can fail against a quantum attacker. We will then present the first-order logic over which Squirrel is built, the BC logic, and show based on the first part where it fails at post-quantum soundness. In a third part, we will finally present our contribution: how we made the logic and thus the Squirrel prover post-quantum sound. We will conclude by discussing some more general challenges the field may be facing in the coming years.[A] see, e.g., https://www.bbc.co.uk/news/technology-58719891 for a recent example[B] https://squirrel-prover.github.io/
Infos pratiques
Prochains exposés
-
Towards privacy-preserving and fairness-aware federated learning framework
Orateur : Nesrine Kaaniche - Télécom SudParis
Federated Learning (FL) enables the distributed training of a model across multiple data owners under the orchestration of a central server responsible for aggregating the models generated by the different clients. However, the original approach of FL has significant shortcomings related to privacy and fairness requirements. Specifically, the observation of the model updates may lead to privacy[…]-
Cryptography
-
SoSysec
-
Privacy
-
Machine learning
-
-
NEAT: A Nile-English Aligned Translation Corpus based on a Robust Methodology for Intent Based Networking and Security
Orateur : Pierre Alain - IUT de Lannion
The rise of Intent Based Networking (IBN) has paved the way for more efficient network and security management, reduced errors, and accelerated deployment times by leveraging AI processes capable of translating natural language intents into policies or configurations. Specialized neural networks could offer a promising solution at the core of translation operations. Still, they require dedicated,[…]-
SoSysec
-
Network
-
Security policies
-
-
Black-Box Collision Attacks on Widely Deployed Perceptual Hash Functions and Their Consequences
Orateur : Diane Leblanc-Albarel - KU Leuven
Perceptual hash functions identify multimedia content by mapping similar inputs to similar outputs. They are widely used for detecting copyright violations and illegal content but lack transparency, as their design details are typically kept secret. Governments are considering extending the application of these functions to Client-Side Scanning (CSS) for end-to-end encrypted services: multimedia[…]-
Cryptography
-
SoSysec
-
-
Malware Detection with AI Systems: bridging the gap between industry and academia
Orateur : Luca Demetrio - University of Genova
With the abundance of programs developed everyday, it is possible to develop next-generation antivirus programs that leverage this vast accumulated knowledge. In practice, these technologies are developed with a mixture of established techniques like pattern matching, and machine learning algorithms, both tailored to achieve high detection rate and low false alarms. While companies state the[…]-
SoSysec
-
Intrusion detection
-
Machine learning
-
-
CHERIoT RTOS: An OS for Fine-Grained Memory-Safe Compartments on Low-Cost Embedded Devices
Orateur : Hugo Lefeuvre - The University of British Columbia
Embedded systems do not benefit from strong memory protection, because they are designed to minimize cost. At the same time, there is increasing pressure to connect embedded devices to the internet, where their vulnerable nature makes them routinely subject to compromise. This fundamental tension leads to the current status-quo where exploitable devices put individuals and critical infrastructure[…]-
SoSysec
-
Compartmentalization
-
Operating system and virtualization
-
Hardware/software co-design
-
Hardware architecture
-