Security Threat Modeling and Automated Analysis for System Design

Despite more and more rigorous defense mechanisms in place for cyber-physical systems, cybercriminals are increasingly attacking systems for benefits using a variety of means including malware, phishing, ransomware, and denial of service. Cyberattacks could not only cause significant economic loss but also disastrous consequences for individuals and organizations. Therefore, it is advantageous to detect and fix potential cyber vulnerabilities before the system is fielded. To this end, this article presents a language, VERDICT, and a novel framework, Cyber Vulnerability Analysis Framework (CyVAF) to (i) define cyber threats and mitigation defenses based on system properties, (ii) detect cyber vulnerabilities of system architecture automatically, and also (iii) suggest mitigation defenses. VERDICT is developed as an annex to the Architecture Analysis and Design Language (AADL) but can also be used independently. It enables users to define customized cyber threats and defenses, as well as from known libraries such as Common Attack Pattern Enumeration and Classification (CAPEC) and National Institute of Standards and Technology Recommended Security Controls for Federal Information Systems and Organizations (NIST 800-53). CyVAF translates a core fragment of AADL model annotated with properties along with VERDICT threats to Alloy specifications, leverages Alloy Analyzer to check whether components of the system are susceptible to threats and suggest defenses. In this article, we describe the language—VERDICT—and the translation mappings in the framework and demonstrate the capability and effectiveness of CyVAF using an unmanned aerial vehicle (UAV) example.