Function Extraction (FX) Research for Computation of Software Behavior: 2010 Development and Application of Semantic Reduction Theorems for Behavior Analysis

For several years, the Software Engineering Institute (SEI) at Carnegie Mellon University has been engaged in a project to compute the behavior of software with mathematical precision to the maximum extent possible. Air Force Office of Scientific Research (AFOSR) sponsorship has played a key role in this effort. The general thrust of the research for AFOSR has been in technology for (1) overcoming difficult aspects of behavior computation and (2) analyzing and manipulating computed behavior. In 2009, the research focused on computing the behavior of loops, a process subject to theoretical limitations. This resulted in practical methods for loop computation that minimize the effects of these constraints. The 2010 research focused on foundations and implementations of algorithms that employ computed behavior and semantic reduction theorems to determine the true control flow of malware programs as an essential first step in computing overall malware behavior. Determining the true control flow of a program in the presence of computed jumps and jump table operations has been a difficult problem for some time. Syntactic methods of control flow analysis exhibit limitations that reduce their effectiveness. The semantic methods employed by behavior computation can produce improved results. The findings of this research have been implemented in a system for malware analysis and have improved capabilities for behavior computation in other applications. At the same time, the research has revealed a potential new approach to both reverse engineer and forward engineer software based on rigorous specification and verification in the context of behavior computation.