diff --git a/_data/publications.yml b/_data/publications.yml index 46ee519..5131f0f 100644 --- a/_data/publications.yml +++ b/_data/publications.yml @@ -1,6 +1,16 @@ --- - year: 2024 publications: + - title: "Quantitative Robustness for Vulnerability Assessment" + authors: + - name: Guillaume Girol + - name: Guilhem Lacombe + - name: Sébastien Bardin + venue: 45th ACM-SIGPLAN Symposium on Programming Language Design and Implementation + venue-acronym: PLDI + ranking: A* + easy-summary: nutshells/pldi-24-qrse.html + pdf: /assets/publications/papers/2024-pldi-qrse.pdf - title: "Compiling with Abstract Interpretation" authors: - name: Dorian Lesbre diff --git a/assets/publications/papers/2024-pldi-qrse.pdf b/assets/publications/papers/2024-pldi-qrse.pdf new file mode 100644 index 0000000..1a73842 Binary files /dev/null and b/assets/publications/papers/2024-pldi-qrse.pdf differ diff --git a/nutshells/pldi-24-qrse.md b/nutshells/pldi-24-qrse.md new file mode 100644 index 0000000..c88dc37 --- /dev/null +++ b/nutshells/pldi-24-qrse.md @@ -0,0 +1,108 @@ +--- + layout: post + title: "PLDI'24, research paper" + categories: new publication + paper-title: "Quantitative Robustness for Vulnerability Assessment" + topic: "program reliability and security; reachability; symbolic execution;" + pdf: "/assets/publications/papers/2024-pldi-qrse.pdf" + date: 2024-05-31 +--- + + +# Quantitative Robustness for Vulnerability Assessment + +## Motivation + +Most software analysis techniques focus on bug reachability, i.e., proving the existence of inputs triggering a bug. +However, this approach is not ideal for security evaluation as it does not take into account how reliably said bugs can be triggered. +Indeed, some inputs may not be easily controlled by an attacker in practice, such as sources of randomness for instance. + +**Robust reachability.** +To tackle this issue, we introduced the notion of *robust reachability* in a previous paper (*put link here*). +Given a partition of inputs between *controlled* and *uncontrolled* ones, a program location is *robustly reachable* if and only if it can always be reached regardless of the value of uncontrolled inputs. + +While robust reachability is a strong indicator of reliability, it suffers from its lack of nuance. +Indeed, some bugs may not be robustly reachable, yet "easy enough" to trigger to be exploitable. + +## Example + +``` +/* main privilege levels */ +# define DEFAULT_LEVEL 1 +# define OPERATOR_LEVEL 100 +# define ADMIN_LEVEL 9000 +/* commands */ +# define DROP_PRIVILEGE 0 +# define DROP_PRIVILEGE_LEGACY 1 +# define GET_VERSION 2 +# define SUDO 3 + +uint32_t uninit ; /* random data */ +uint32_t privilege_level = DEFAULT_LEVEL ; + +void set_privilege_level ( uint32_t new) { + privilege_level = new; +} + +uint32_t get_privilege_level () { + // bug: return uninitialized memory + return uninit ; +} + +void prog1 ( uint32_t command , uint32_t argument ) { + if ( command == GET_VERSION ) { + /* harmless */ + } else { + /* command is sudo */ + if ( get_privilege_level () == OPERATOR_LEVEL ) { + set_privilege_level ( ADMIN_LEVEL ); + } + } +} + +void prog2 ( uint32_t command , uint32_t argument ) { + switch ( command ) { + case GET_VERSION : /* harmless */ break ; + case DROP_PRIVILEGE : + case DROP_PRIVILEGE_LEGACY : + if ( argument < get_privilege_level ()) { + set_privilege_level ( argument ); + } + } +} +``` + +In prog1, when attackers play perfectly by choosing command = 1, they need to be lucky to : only one value of uninit out of $2^{32}$ grants them admin privileges. +However in prog2, for command = 1 and argument = 9000 over 99% of the values that uninit can take will let attackers achieve their goal. + +## Quantitative Robustness + +In this paper, we define a new, *quantitative* notion of robust reachability, *quantitative robustness*, as the maximum proportion of uncontrolled inputs triggering the bug for a chosen controlled input. +Using this definition, we can now distinguish the two bugs from the previous example. + +**Quantitative Robust Symbolic Execution (QRSE).** +To determine the quantitative robustness of a bug, we first use symbolic execution to obtain constraints for the execution paths reaching it. +We can then compute quantitative robustness either for each path separately, or on a single, merged constraint. +Since it is often enough to shown that overall quantitative robustness exceeds a threshold in practice, we can stop exploring new paths once this condition is met. + +**Measuring quantitative robustness.** +Quantitative robustness can be reduced to the *f-E-MAJSAT* problem, which previously had applications in some AI-related fields. +Existing algorithms can thus be used and we also propose a new approximate one called *Relax*. + +**Experiments** +We applied QRSE to the benchmark from our previous robust reachability paper, which includes several real-world vulnerabilities, as well as to a fault analysis benchmark. +The results showcase the usefulness of the increase in precision from robust reachability to quantitative robustness. +In addition, we compared the performance of existing f-E-MAJSAT solvers as well as Relax on 117 formulas from our previous experiments. +Overall, most existing algorithms perform poorly in the context of quantitative robustness, except for the most naive one, surprisingly. +Relax also proves useful in approximately solving additional instances. + +## Contributions + +In summary, we make the following contributions: +- We define a quantitative pendant of robust reachability called quantitative robustness, which generalize both reachability and robust reachability. +- We propose Quantitative Robust Symbolic Execution (QRSE), a variant of symbolic execution for computing quantitative robustness. We show that QRSE does not strictly require path merging, contrary to robust reachability analysis. +- We propose a method reducing path-wise quantitative robustness with finite variable domains (e.g., bitvectors and arrays) to f-E-MAJSAT, a counting problem studied in some sub-fields of AI. +As off-the-shelf methods turn out to be too inefficient or imprecise for our purposes, we introduce a new approximate algorithm called Relax. +- We have implemented these ideas in two tools: BINSEC/QRSE and the Popcon solver. +First experiments on security-oriented case studies demonstrate that QRSE enables fine-grained bug triage compared to symbolic execution and robust symbolic execution. +In addition, Relax solves more problems arising from QRSE than prior techniques while minimizing approximation.