Code-level security analysis: what about the attacker?
Program analysis techniques have made tremendous progress in the past decades, and while their initial application fields were mostly safety-critical systems, they are now routinely used in security-related evaluations. Yet, somehow, the typical design of program analyzers and their associated techniques did not change that much, and they are still rooted in safety. In this talk, I will argue that fully embracing a security-oriented view of program analysis opens new interesting (and fun!) challenges. I will especially focus on how to take the attacker into account in code-level security analysis, and describe several recent advances in this direction, with applications to hardware/software attacks and vulnerability priorization.
The talk will be mainly structured around the following key points:
a quick overview of formal methods and the basics of automated program analysis, as well as their historical success in safety (e.g., avionics) and some of their current successes in security
some reflections on the differences between safety and security, and why we need to go beyond safety-centric program analysis. Especially, the attacker is a key difference
the presentation of several scenarios where taking the attacker into account is necessary, how we have done it and practical results obtained.
We will especially discuss code-level security evaluation against hardware/software attacks (fault injection, side channel attacks) and vulnerability priorization (given a set of vulnerabilities together with associated triggering input, which ones are the most important to fix), and present some results obtained on the evaluation of cryptographic implementations (classic and post-quantum), secure boot and base of fuzzing-discovered vulnerabilities.
We will also quickly explain how these notions have been integrated into the open-source BINSEC platform for binary-level security analysis. https://binsec.github.io/
The talk will build on material and results obtained over 5 years by the BINSEC group at CEA LIST (Saclay, France) and published in top-tiers academic venues for system security [IEEE Security & Privacy 2020, ACM Conference on Computer and Communications Security 2023, Usenix Security 2025], Formal Methods [Computer-Aided Verification 2021] and Programming Languages [POPL 2024, PLDI 2024].
Sébastien Bardin is a senior researcher at CEA LIST (Saclay, Paris area, France), where he has initiated and now leads the binary-level security analysis group. His research interests lay at the crossroad of formal methods and program analysis, security and software engineering. Especially, Sébastien is interested in automating binary-level code security analysis, with applications to vulnerability analysis, software-hardware attacks, reverse, deobfuscation and code protection. He is the main designer of the (open-source) BINSEC platform for binary-level code analysis. Sébastien regularly publishes articles in top-ranked international academic conferences and he occasionally gives talks at industrial venues such as Black Hat or the Meta TAV Symposium. Sébastien has co-chaired for many years the French national working group on Formal Methods & Security, and he co-leads SECUREVAL, a major initiative for security-oriented program analysis. Sébastien is a CEA Fellow.
https://scholar.google.com/citations?user=5tee-l8AAAAJ
https://binsec.github.io/