Amphitéatre MJK
2 December 2024 - 14h00
Quantitative analysis for adaptive attackers (Phd Defense)
Thomas Vigouroux from Verimag
2 December 2024 - 14h00
Quantitative analysis for adaptive attackers (Phd Defense)
Thomas Vigouroux from Verimag
Abstract: Evaluating the security of a program is a notoriously difficult task, but of paramount importance considering the prevalence of computer systems in today’s world.
A possible path towards security evaluation proceeds in steps: first search for vulnerabilities or bugs within the program, then evaluate how to turn said bugs into profit, whether it be information or capabilities with respect to the program. In order to perform security evaluation of the program, one has thus to consider what is called an attacker model. We propose in this thesis an attacker hierarchy, with increased reasoning capabilities as we go up the hierarchy: non-adaptive, adaptive, or multiple adaptive attackers. We study the elements of the hierarchy depending on the attacker’s objective, whether it be triggering a bug or gaining information.
While qualitative criteria for evaluating the security of a program exist, their quantitative counterparts are relatively less studied. The interest behind quantitative criteria is twofold: one could easily compare two programs in order to, for example, assess that a given vulnerability has been addressed properly, or to schedule bugs to be fixed in priority; or one could provide a quantitative goal that the program has to reach which depends on the target application domain, and enforce the security policy this way.
The goal of this thesis is thus to develop new quantitative criteria for program security, based on quantitative attacker’s objectives, which yields so-called counting problems. Counting problems are, as their name implies, problems related to computing the size of a set. We focus our interest on one counting problem for each level of the hierarchy: Max#SAT for non-adaptive, SSAT for adaptive, and DQMax#SAT for multiple attackers. In this thesis, we define formally two quantitative attacker’s objectives, and develop encodings of said attacker’s objective as a counting problem. We then resolve these combinatorial optimization problem, which corresponds to answering the question ”how easy is it for the attacker to fulfill this goal?”.
