Publications

In this paper we propose a new abstract domain for static analysis of binary code. Our motivation stems from the need to improve the precision of the estimation of the Worst-Case Execution Time (WCET) of safety-critical real-time code. WCET estimation requires computing information such as upper bounds on the number of loop iterations, unfeasible execution paths, etc. These estimations are usually performed on binary code, mainly to avoid making assumptions on how the compiler works. Our abstract domain, based to polyhedra and on two mapping functions that associate polyhedra variables with registers and memory, targets the precise computation of such information. We prove the correctness of the method, and demonstrate its effectiveness on benchmarks and examples from typical embedded code.

The research of a safe Worst-Case Execution Time (WCET) estimation is necessary to build reliable hard, critical real-time systems. Infeasible paths are a major cause of overestimation of the Worst-Case Execution Time (WCET): without data flow constraints, static analysis by implicit path enumeration will take into account semantically impossible, potentially expensive execution paths, making the Worst-Case Execution Path unreachable in practice. We present in this paper an approach that allows to significantly tighten the WCET by identifying infeasible paths, namely in loops, and injecting them as additional Integer Linear Programming (ILP) constraints during the WCET computation. Our entire analysis, albeit platform independent, works directly on binary programs in order to get the tightest, most reliable WCET. Impactful infeasible paths are largely found within (often nested) loops; therefore having an efficient, exploitable and reasonably scalable representation of the state of a program within loops is a key challenge of infeasible path analysis. We show ours to yield decidedly significant results on a selection of benchmarks from actual hard real-time applications as well as the classic Mälardalen suite.