Rice's theorem stating that no method can automatically tell whether a property of a program is true or not has led to the separation of verification tools into two groups: sound tools operating by over-approximation, such as abstract interpretation, are able to automatically prove that certain properties are true, but are sometimes unable to conclude and produce alarms; conversely, complete tools operating by under-approximation, such as symbolic execution, are able to produce counter-examples, but are unable to demonstrate whether a property is true.

*The general aim of the thesis is to study the combination of sound and complete methods of programanalysis, and in particular static analysis by abstract interpretation and the generation of underapproximated formulae by symbolic execution*.

We are particularly interested in the combination of over- and sub-approximating abstractions, especially for memory. The priority applications envisaged concern the analysis of code at the binary level, as achieved by the combination of the BINSEC and CODEX analysis platforms, so as to automatically discover new security vulnerabilities, or prove their absence.

Providing assurances that autonomous systems will operate in a safe and secure manner is a prerequisite for their deployment in mission-critical and safety-critical application domains. Typically, assurances are provided in the form of assurance cases, which are auditable and reasoned arguments that a high-level claim (usually concerning safety or other critical properties) is satisfied given a set of evidence concerning the context, design, and implementation of a system. Assurance case development is traditionally an analytic activity, which is carried out off-line prior to system deployment and its validity relies on assumptions/predictions about system behavior (including its interactions with its environment). However, it has been argued that this is not a viable approach for autonomous systems that learn and adapt in operation. The proposed PhD will address the limitations of existing assurance approaches by proposing a new class of security-informed safety assurance techniques that are continually assessing and evolving the safety reasoning, concurrently with the system, to provide through-life safety assurance. That is, safety assurance will be provided not only during initial development and deployment, but also at runtime based on operational data.

Software vulnerabilities due to memory management errors are among the easiest to exploit. To prevent an attacker from injecting its own arbitrary code (shellcode), modern systems commonly enforce a Data Execution Prevention (DEP), often implemented as segment permissions (Write xor Execute – W^E).
Yet, Code-Reuse Attacks have emerged to circumvent the DEP protections. Thanks to a memory logic issue, the attacker hijacks the control flow of the target program and chains small code fragments referred to as gadgets to build the desired behavior, through so-called Return-Oriented Programming (ROP) or Jump-Oriented Programming (JOP).
In the past years, several research efforts have explored how to automate the construction of code reuse attacks from basic "on stack" attacks, lowering the barrier to such advanced methods. On the other side, program hardening relies on randomized memory layout (e.g. Address Space Layout Randomization – ASLR), Control Flow Integrity (CFI) or stack protection mechanism (e.g. Shadow Stack) to keep the
attacker in check. Still, some of these protection may be costly (execution time, specialized hardware, etc.).

The general goal of this PhD topic is to improve the state of the art of the automatic exploit generation landscape for the purpose of security assessment of anti-code-reuse protection. We will follow two trend:
(1) on the one hand the candidate will push automated code-reuse automation methods, by taking into account the knowledge of the protection to guide the research to valid exploit only, prospectively cutting-off in the search space, and by looking for synergies between the ROP/JOP chaining and program synthesis methods such as syntax guided synthesis or stochastic synthesis methods;
(2) on the other hand, once the potential of such methods is better understood, the candidate will design effective defense against them, based on a comprehensive analysis of their main strengths and weaknesses.