École Nationale Supérieure de
Techniques Avancées

Abstract

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.