User-directed analysis and verification of modified binaries

In the Phase I and II efforts on Galois' Attack Sensitive Brittle Software (Brittle) SBIR project, we implemented Software Fault Enhancement (SFE), a binary modification technique for improving the robustness of existing binary code, without requiring access to source code or other documentation.  This work is promising enough that the toolset is now being commercialized.  On this sequential Phase II project, we will extend and integrate recent work on symbolic, concrete, and timed trace analysis to implement new means of providing assurance to the user that binary modifications made for SFE do not result in additional, unwanted changes in behavior.  This specifically includes changes in timed behavior, important in the operation of embedded systems such as digital control systems. The results of this project will be useful for providing such assurance for a range of applications of localized binary modification.  In addition to SFE, these include patching bugs or removing possible execution paths (e.g., removing application features), or instrumenting binaries to gather run-time information for further testing and analysis.  In all of these cases, potential end-users need assurance that the modified binaries will behave as before, except in circumscribed ways related to the goal of the modification as above.