Insider Threat Detection and Response Using Formal Methods

This project will extend the Capability Acquisition Graph (CAG) model to a form that can be easily analyzed with formal methods in order to develop countermeasures for cyber attacks arising from within an organization. The extension will be based on an efficient translation of the problem to Boolean Satisfiability (SAT), in order to exploit the both the speed and capacity of SAT solvers. Extensions of the model will be explored to improve its robustness, including its response to insider threats from system administrators. Formal techniques will be implemented to automatically generate plausible attacks and to develop recommendations for network hardening. Commercial Applications and other Benefits as described by the awardee Besides the DOE, the resulting technology should be of benefit to the DoD and all other organizations that need to protect high-value information, such as the banking industry, high-tech companies developing expensive intellectual property, and civilian government infrastructures