Constructing formal models from binaries

Details

Supervisors

Axel Legay

Faculty

Ecole polytechnique de Louvain

Degree label

Master [120] : ingénieur civil en informatique

Abstract

Software performing in hostile environment may be vulnerable to fault injection. To ensure a computer program has a failure rate below an acceptable risk level, it must be verified formally. The first step consists of reproducing hardware faults by using a software injection fault tool developed in this master's thesis. After that, two ways of verifying properties on the variations of the binaries are explored. The first one uses Lodin and the decompilation of binaries to LLVM bitcode. This way was put aside due to its many drawbacks. The second way uses plugins integrating with the statistical model checking platform Plasma Lab in order to simulate software with a debugger like GDB, check LTL properties on its execution trace and evaluate the correctness of all the possible faulty variants. Finally, this approach is illustrated and evaluated with two examples checked by the complete toolchain as a feasibility proof.