Symbolic path simulation in path-sensitive dataflow analysis

摘要

Symbolic path simulation is becoming an increasingly important component in many static analysis tasks. The emergence of inter-procedural path-sensitive dataflow algorithms has both raised the demands and posed new challenges for effective techniques in path feasibility analysis.This paper develops a general-purpose path simulator and applies it to support path-sensitive dataflow analysis. The core component of the path simulator is a simulation engine that supports a wide variety of programming language features. This simulation engine can be "wrapped" with an interface layer to support a given client application.As a concrete case study, we discuss the experiences gained in integrating the path simulator with ESP, a software validation tool for C/C++ programs. We apply ESP to validate a future version of Windows against critical security properties. Our results show that the global path simulation mechanism is both critical in improving precision and scalable enough to be of practical use.