CETIC has defined a subset of C language adapted for hardening techniques for which it has developed software hardening tool (i.e. code transformation technique to prevent against errors due to hardware faults). The output of this tool is hardened C code which needs to be compiled.
Compilers for C language make optimization of the code in order to increase the performance of the binaries. However this optimization step doesn’t produce an intermediary C code and cannot be configured in order to respect specific constraints of the code. Particularly in the scope of software hardening, the optimization realized by C compilers doesn’t give guarantee that the modified code preserves correctly the fault detection mechanism. So it cannot be used, or only for very specific and validated optimisation.
The goal of this thesis is to study which kind of optimization can be done on this subset of C language in order to increase the performance of the executable code. The optimization step will be performed before de hardening step. A tool will be written to apply these optimizations to the input code. The tool should be developed with a functional language such as OCAML or Scala. An important part of the work will be to identify the transformations of the code and also to develop assurance techniques showing the optimisation is safe (i.e. it preserves the semantics or in the case it does not this would be detected possibily by the robustification mechanism).
The thesis can be coupled with a MS thesis in a university. The work will be performed within the department "Software and System Engineering"
Contact : Gautier Dallons (email@example.com)