Model-Based Cyber Security

This paper presents an approach for automatically verifying the correctness of cyber security applications through formal analysis guided by hierarchical models of the network, its applications, and potential attacks. This work is motivated by the need for a more intuitive, automated systems-level approach to determining the overall security characteristics of a large network. Given the complex nature of security tools and their general lack of interoperability, it is difficult for system designers to make definitive statements about the nature of their network defense. Our work focuses on creating an environment in which security experts can model the security aspects of complex networks using a graphical notation that is intuitive and natural for them, then automatically perform security activities such as formally verifying the safety of the network against known threats and exploring the network design for potential vulnerabilities. The environment is designed to utilize third party tools for performing these activities and concentrates on integration of these tools within a common modeling framework