Nicole, M. Olivier (2018) Automatic Formal Verification of a Kernel Binary Executable using Abstract Symbolic Execution PFE - Project Graduation, ENSTA.



We present a new static analysis method to compute safe control flow graphs and memory footprints of binary executable. This analysis uses a novel technique, abstract symbolic execution, and a new data flow elimination algorithm. We apply our analysis to the binary executable of an embedded kernel. This enables us to verify, under some hypotheses on memory, some safety and security properties: the absence of kernel crashes and the impossibility for applications to read kernel memory or tamper the kernel control flow.

Item Type:Thesis (PFE - Project Graduation)
Subjects:Mathematics and Applications
ID Code:7291
Deposited By:Olivier Nicole
Deposited On:01 avr. 2019 11:15
Dernière modification:01 avr. 2019 11:15

Repository Staff Only: item control page