An efficient control flow security analysis approach for binary executables

This paper proposes a control flow based security analysis approach for binary executables. Through deeply investigating the theory of control flow security, we develop the Control Flow Security Model (CFSM) which includes the formal definitions for program semantics and security properties for control flow. CFSM specifies that program execution dynamically follows only certain paths, in accordance with a statically declared security properties specified as Control Flow Constraint Specification (CFCS). We have proposed an efficient control flow security analysis algorithm for verifying that a particular control flow model satisfies the associated security properties. Our work contributes to bridging the gap between abstract specifications of control flow security properties and actual control flow security analysis for binary executables. The effectiveness and the practical usefulness of the approach are exemplified by an illustrative analysis of heap overflow vulnerability.