We have open positions to work for 3 years as a postdoc on advanced abstract interpretation techniques for binary code verification.
Our work combine SSA-based abstract interpretation POPL 2023, memory analysis based on type VMCAI 2022 or separation logic SAS 2020 to verify security properties of binary executable, for instance operating system kernels RTAS 2021.
TOPIC - Machine code verification is hard, because machine code lacks high-level concepts that normally helps the analyzer – instead, these concepts have to be recovered during the analysis. Further, an insufficient precision in an analysis can snowball catastrophically, leading the analyser to being unable to complete the analysis.
We investigate abstract interpretation as a way to solve this problem. In particular, abstract interpretation allows modular combination of analyses that help each other to be more precise, allowing to reach the sufficient precision to analyze the program. We have in particular developped a SSA-based abstract interpretation framework POPL 2023 which decompiles machine code in a higher-level SSA representation on which the other analyses are made, and a semantic type system VMCAI 2022 that helps the analyzer to precisely and efficiently represent the memory; and demonstrated that the resulting analysis could fully automatically prove security properties of an embedded system kernel, like absence of privilege escalation, from its executable RTAS 2021. The goal of the postdoc is to further study, both theoretically and experimentally, extensions of this framework (new SSA-based abstract domains, new typing rules, combination with analysis based on separation logic, more efficient and precise inter-procedural analysis, new security properties, etc.) to address challenging case studies that are out of the reach of current methods.
KEYWORDS - abstract interpretation, SSA, type systems, non-interference, operating system kernels, separation logic
SUPERVISION - Supervision will be provided by Matthieu Lemerre, typically in collaboration with other researchers from the team and outside of it, to provide an optimal combination of expertise, availability and seniority.
HOSTING - You will be hosted at the CEA offices, part of the Paris-Saclay research cluster.
To apply, send an email directly to matthieu.lemerre at cea.fr.
When to apply - As soon as possible! We process applications as soon as they arrive (depending on our own availability ^^), so don’t be too late.