Architectural and Behavioral Analysis for Cyber Security

The asymmetric nature and ever-increasing degree of sophistication of cyber threats drive the need for assurance of critical infrastructure and systems. Current approaches that can help counter these cyber threats include the application of tools with the ability to analyze system behavior in its most general form and in the presence of wide classes of threats-at design time. In this paper we describe our tool for incorporating cyber security resiliency analysis and recommendations in the system design process that are automated, scalable, provide rich feedback, specify trade-offs and are easy to use by system architects. The architecture models and design knowledge are captured in formalisms that are expressive and amenable to automated reasoning, analysis, and analysis for cyber security. The two main components developed are Model-Based Architectural Analysis and Cyber-resiliency Verifier. The Model-Based Architectural Analysis identifies threats against the architecture and the potential tradeoffs of their mitigations. Threats are identified from attack patterns from Mitre's Common Attack Pattern Enumeration and Classification (CAPEC) and defenses are suggested based on controls from NIST's Security and Privacy Controls list. After the threats and defenses are identified, an attack-defense tree is generated along with cutsets that describe attack scenarios and associated defenses. The identified threats as well as the attack-defense trees are visualized to provide a concise and informative view of the analysis. There may be multiple ways of addressing a threat and the system architect can decide which defense to implement. After the architecture has been revised to be secure, we then consider cyber-resiliency behavioral properties of the system. For this we abstract threat models in terms of an instrumentor that incorporates the effects of the threats. This allows us to aggregate classes of threats with the same effect so that they can be addressed at the effects level as opposed to treating them individually. The cyber-resiliency properties are then verified by an extension of the proven model checker Kind 2 which identifies the system components responsible for a property violation and provides localized diagnostic information. This enables the system architect to rework the vulnerable portions of the design to discharge required resiliency obligations. In case of resiliency property violations, the tool can recommend placement of runtime monitors sufficient to discharge specific proof obligations. Finally, our tool automatically generates test cases and procedure to check the conformance between the design and implementation.