Proof of functional equivalence of binary codes in the context of embedded program hardening

Job description: The general context of this thesis is the cyber-security of embedded systems. The research background of this thesis is tied to the automatic application of counter-measures against the so-called physical attacks, which encompass observation attacks (side-channel attacks) and perturbation attacks (fault-injection attacks). The CEA List is working on COGITO, a compiler toolchain based on LLVM for the automatic application of software counter-measures against physical attacks. Given a source-level implementation of an unprotected program, our toolchain produces an optimised binary program including targeted counter-measures, such that the compiled program is hardened against a specified threat model. Two key points are today crucial to trust the compiled programs: 1. the proof of robustness of programs produced by our toolchain, 2. the proof that adding counter-measures does not alter the functionality of the target programs. This thesis will target the second point: bringing formal guarantees about the functional correctness of the secured programs. We will use sound and exhaustive symbolic reasoning, supported by BINSEC (lt;https://binsec.github.iogt;). BINSEC is an open-source toolset developed at CEA List to help improve software security at the binary level. It relies on cutting-edge research in binary code analysis, at the intersection of formal methods, program analysis, security and software engineering. The PhD thesis will be hosted at the CEA in Saclay, within the BINSEC team. Short-term stays at CEA Grenoble will be planned throughout the three years of the thesis to collaborate with experts and developers of COGITO.

Your profile: Master in computer science, with a solid theoretical background.