Abstract
Microcontrollers storing valuable data or using security functions are vulnerable to fault injection attacks. Among the various types of faults, instruction skips induced at runtime proved to be effective against identification routines or encryption algorithms. Until recently, most research papers assessed a fault model that consists in a single instruction skip, i.e. the ability to prevent one chosen instruction in a program from being executed. This seminar reports experimental results that extend the complexity and versatility of the instruction-skip fault model. It shows how using laser or EM fault injection makes it possible to induce several consecutive instructions skips or to skip instructions from different parts of a program. It focuses on results obtained on custom test circuits and general purpose microcontrollers at different technology nodes. An analysis of the involved injection mechanisms is also provided.

Short bio
Prof. Jean-Max Dutertre received the M.S. and Ph. D. degrees in microelectronics from the University of Science of Montpellier, France, in 1998 and 2002, respectively. He is head of the Secured Architectures and Systems (SAS) research department of Mines Saint-Etienne from Institut Mines-Télécom, which is part of a joint R&D team with the CEA Leti. His research interests are with hardware attack techniques and the design of the related counter-measures (either hardware or software). He has been studying fault injection attacks of secure integrated circuits for 15 years.

Abstract:

This presentation will first introduce the FragAttacks vulnerabilities (USENIX 2021). The FragAttacks findings consist of three cryptographic design flaws in the fragmentation and aggregation features of Wi-Fi. Additionally, the FragAttacks research discovered multiple widespread implementation flaws related to fragmentation and aggregation. We give a brief overview of these design and implementation vulnerabilities.
An open question is how many Wi-Fi networks in the meantime have been updated to fix these vulnerabilities. In the second part of the presentation, we will show how some of the FragAttacks vulnerabilities can be reliably detected during a Wi-Fi survey (also known as a Wi-Fi wardrive). This would enable researchers to measure how many access points have been updated, and how much of a risk the vulnerabilities still present. Most importantly, we examine the ethical aspects of possibly doing such a Wi-Fi survey, and hope to discuss the ethical aspects of this with the audience.

Short Bio:

Mathy Vanhoef is an Assistant Professor at KU Leuven University in Belgium. He’s interested in network and software security, where he studies the security of the full network stack, with a focus on Wi-Fi security and applied cryptography. In this area, he tries to bridge the gap between real-world code and theory. He previously discovered the KRACK attack against WPA2 and the Dragonblood attack against WPA3. He also collaborated with the industry to design and standardize two new Wi-Fi defenses. One of these defenses, called beacon protection, will become mandatory in Wi-Fi 7.

Bugs in software and hardware can often to catastrophic consequences. There are various ways to improve software quality, formal verification being the most rigorous of all. In formal verification, the goal is to translate programs into formulas, and then automatically prove the correctness of these formulas. Formal methods offer a vast collection of techniques to analyze and verify these systems mathematically to ensure the correctness, robustness, and safety of software and hardware systems against a specification. Despite the significant success of formal method techniques, privacy requirements are not considered in their design.

In the last two decades, we have witnessed fascinating progress in the area of automated reasoning. Modern automated reasoning tools are now applied daily to tasks in program analysis, software engineering, hardware verification, and various other domains. The efficacy of such tools allows their application to even large-scale industrial codebases.

In this talk, we will present our work on adding a privacy-aware perspective to automated reasoning. When using automated reasoning tools, the implicit requirement is that the formula to be proved is public. We propose the concept of privacy-preserving formal reasoning. In our recent work on a zero-knowledge protocol for proving the unsatisfiability of Boolean formulas in propositional logic, we developed a highly efficient protocol for knowledge of a resolution proof of unsatisfiability. We encoded verification of the resolution proof using polynomial equivalence checking, which enabled us to use fast ZKP protocols for polynomial satisfiability.

BIO:

Ruzica Piskac is an associate professor of computer science at Yale University. Her research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica’s research is improving software reliability and trustworthiness using formal techniques. Ruzica joined Yale in 2013 as an assistant professor and professor, and prior to that, she was an independent research group leader at the Max Planck Institute for Software Systems in Germany. In July 2019, she was named the Donna L. Dubinsky Associate Professor of Computer Science, one of the highest recognitions that an untenured faculty member at Yale can receive. Ruzica has received various recognitions for research and teaching, including the Patrick Denantes Prize for her PhD thesis, a CACM Research Highlight paper, an NSF CAREER award, the Facebook Communications and Networking award, the Microsoft Research Award for the Software Engineering Innovation Foundation (SEIF), the Amazon Research Award, and the 2019 Ackerman Award for Teaching and Mentoring.