{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:56:56Z","timestamp":1764784616072,"version":"build-2065373602"},"reference-count":54,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2021,3,3]],"date-time":"2021-03-03T00:00:00Z","timestamp":1614729600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-18-C-4006"],"award-info":[{"award-number":["N66001-18-C-4006"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems"],"abstract":"<jats:p>The ever-increasing complexity of cyber-physical systems is driving the need for assurance of critical infrastructure and embedded systems. However, traditional methods to secure cyber-physical systems\u2014e.g., using cyber best practices, adapting mechanisms from information technology systems, and penetration testing followed by patching\u2014are becoming ineffective. This paper describes, in detail, Verification Evidence and Resilient Design In anticipation of Cybersecurity Threats (VERDICT), a language and framework to address cyber resiliency. When we use the term resiliency, we mean hardening a system such that it anticipates and withstands attacks. VERDICT analyzes a system in the face of cyber threats and recommends design improvements that can be applied early in the system engineering process. This is done in two steps: (1) Analyzing at the system architectural level, with respect to cyber and safety requirements and (2) by analyzing at the component behavioral level, with respect to a set of cyber-resiliency properties. The framework consists of three parts: (1) Model-Based Architectural Analysis and Synthesis (MBAAS); (2) Assurance Case Fragments Generation (ACFG); and (3) Cyber Resiliency Verifier (CRV). The VERDICT language is an Architecture Analysis and Design Language (AADL) annex for modeling the safety and security aspects of a system\u2019s architecture. MBAAS performs probabilistic analyses, suggests defenses to mitigate attacks, and generates attack-defense trees and fault trees as evidence of resiliency and safety. It can also synthesize optimal defense solutions\u2014with respect to implementation costs. In addition, ACFG assembles MBAAS evidence into goal structuring notation for certification purposes. CRV analyzes behavioral aspects of the system (i.e., the design model)\u2014modeled using the Assume-Guarantee Reasoning Environment (AGREE) annex and checked against cyber resiliency properties using the Kind 2 model checker. When a property is proved or disproved, a minimal set of vital system components responsible for the proof\/disproof are identified. CRV also provides rich and localized diagnostics so the user can quickly identify problems and fix the design model. This paper describes the VERDICT language and each part of the framework in detail and includes a case study to demonstrate the effectiveness of VERDICT\u2014in this case, a delivery drone.<\/jats:p>","DOI":"10.3390\/systems9010018","type":"journal-article","created":{"date-parts":[[2021,3,3]],"date-time":"2021-03-03T20:33:57Z","timestamp":1614803637000},"page":"18","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System"],"prefix":"10.3390","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3284-1969","authenticated-orcid":false,"given":"Baoluo","family":"Meng","sequence":"first","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"Daniel","family":"Larraz","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Iowa, Iowa City, IA 52242, USA"}]},{"given":"Kit","family":"Siu","sequence":"additional","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"Abha","family":"Moitra","sequence":"additional","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"John","family":"Interrante","sequence":"additional","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"William","family":"Smith","sequence":"additional","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"Saswata","family":"Paul","sequence":"additional","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"Daniel","family":"Prince","sequence":"additional","affiliation":[{"name":"GE Aviation, 3290 Patterson Ave SE, Grand Rapids, MI 49512, USA"}]},{"given":"Heber","family":"Herencia-Zapana","sequence":"additional","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"M. Fareed","family":"Arif","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Iowa, Iowa City, IA 52242, USA"}]},{"given":"Moosa","family":"Yahyazadeh","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Iowa, Iowa City, IA 52242, USA"}]},{"given":"Vidhya","family":"Tekken Valapil","sequence":"additional","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"Michael","family":"Durling","sequence":"additional","affiliation":[{"name":"GE Research, 1 Research Cir, Niskayuna, NY 12309, USA"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Iowa, Iowa City, IA 52242, USA"}]},{"given":"Omar","family":"Chowdhury","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Iowa, Iowa City, IA 52242, USA"}]}],"member":"1968","published-online":{"date-parts":[[2021,3,3]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Siu, K., Abha, M., Meng, L., Michael, D., Heber, H.-Z., John, I., Baoluo, M., Cesare, T., Omar, C., and Daniel, L. (2019, January 8\u201312). Architectural and Behavioral Analysis for Cyber Security. Proceedings of the 2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC), San Diego, CA, USA.","key":"ref_1","DOI":"10.1109\/DASC43569.2019.9081652"},{"doi-asserted-by":"crossref","unstructured":"Papp, D., Ma, Z., and Buttyan, L. (2015, January 21\u201323). Embedded Systems Security: Threats, Vulnerabilities, and Attack Taxonomy. Proceedings of the 13th Annual Conference on Privacy, Security and Trust (PST), Izmir, Turkey.","key":"ref_2","DOI":"10.1109\/PST.2015.7232966"},{"unstructured":"MITRE Corporation (2020, November 12). Common Vulnerabilities and Exposures. Available online: https:\/\/cve.mitre.org\/.","key":"ref_3"},{"doi-asserted-by":"crossref","unstructured":"Kordy, B., Kordy, P., Mauw, S., and Schweitzer, P. (2013, January 27\u201330). ADTool: Security analysis with attack\u2013defense trees. Proceedings of the International Conference on Quantitative Evaluation of Systems, Buenos Aires, Argentina.","key":"ref_4","DOI":"10.1007\/978-3-642-40196-1_15"},{"doi-asserted-by":"crossref","unstructured":"Pinchinat, S., Acher, M., and Vojtisek, D. (2015, January 13). ATSyRa: An integrated environment for synthesizing attack trees. Proceedings of the International Workshop on Graphical Models for Security, Verona, Italy.","key":"ref_5","DOI":"10.1007\/978-3-319-29968-6_7"},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Gethin, N., and David, P. (2011, January 14\u201320). PRISM 4.0: Verification of probabilistic real-time systems. Proceedings of the International Conference on Computer Aided Verification, Snowbird, UT, USA.","key":"ref_6","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1016\/j.cose.2009.01.002","article-title":"Probabilistic model checking for the quantification of DoS security threats","volume":"28","author":"Basagiannis","year":"2009","journal-title":"Comput. Secur."},{"doi-asserted-by":"crossref","unstructured":"Alexiou, N., Basagiannis, S., Katsaros, P., Dashpande, T., and Smolka, S.A. (2010, January 3\u20134). Formal analysis of the kaminsky DNS cache-poisoning attack using probabilistic model checking. Proceedings of the 2010 IEEE 12th International Symposium on High Assurance Systems Engineering, San Jose, CA, USA.","key":"ref_8","DOI":"10.1109\/HASE.2010.25"},{"unstructured":"Celik, Z.B., McDaniel, P., and Tan, G. (2018, January 18\u201323). Soteria: Automated iot safety and security analysis. Proceedings of the 2018 USENIX Annual Technical Conference (USENIX ATC 18), Boston, MA, USA.","key":"ref_9"},{"doi-asserted-by":"crossref","unstructured":"Manolios, P., Siu, K., Noorman, M., and Liao, H. (2019, January 28\u201331). A model-based framework for analyzing the safety of system architectures. Proceedings of the 2019 Annual Reliability and Maintainability Symposium (RAMS), Orlando, FL, USA.","key":"ref_10","DOI":"10.1109\/RAMS.2019.8769216"},{"doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., and Albert, O. (2006, January 12\u201315). On SAT modulo theories and optimization problems. Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, Seattle, WA, USA.","key":"ref_11","DOI":"10.1007\/11814948_18"},{"unstructured":"Papadopoulos, Y. (2013). HiP-HOPS Automated Fault Tree, FMEA and Optimisation Tool\u2014User Manual, University of Hull.","key":"ref_12"},{"unstructured":"Batteux, M., Prosvirnova, T., and Rauzy, A. (2020, February 01). AltaRica 3.0 Language Specification; Altarica Association Report. Available online: http:\/\/www.altarica-association.org\/Documentation\/pdf\/AltaRica%203.0%20Language%20Specification%20-%20v1.2.pdf.","key":"ref_13"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"127","DOI":"10.3182\/20130904-3-UK-4041.00028","article-title":"The AltaRica 3.0 Project for Model-Based Safety Assessment","volume":"Volume 46","author":"Prosvirnova","year":"2013","journal-title":"IFAC Proceedings Volumes"},{"unstructured":"Feller, P., Hudak, J., Delange, J., and Gluch, D. (2016). Architecture Fault Modeling and Analysis with the Error Model Annex, Software Engineering Institute, Carnegie Mellon University. [2nd ed.].","key":"ref_15"},{"doi-asserted-by":"crossref","unstructured":"Delange, J., and Feiler, P. (2014, January 27\u201329). Architecture fault modeling with the AADL error-model annex. Proceedings of the EUROMICRO Conference on Software Engineering and Advanced Applications, Verona, Italy.","key":"ref_16","DOI":"10.1109\/SEAA.2014.20"},{"unstructured":"Warg, F., and Skoglund, M. (2019, January 9\u201312). Argument Patterns for Multi-Concern Assurance of Connected Automated Driving Systems. Proceedings of the 4th International Workshop on Security and Dependability of Critical Embedded Real-Time Systems (CERTS 2019), Stuttgart, Germany.","key":"ref_17"},{"unstructured":"Taguchi, K., Souma, D., and Nishihara, H. (2014, January 10\u201312). Safe & sec case patterns. Proceedings of the International Conference on Computer Safety, Reliability, and Security, Florence, Italy.","key":"ref_18"},{"doi-asserted-by":"crossref","unstructured":"Martin, H., Bramberger, R., Schmittner, C., Ma, Z., Gruber, T., Ruiz, A., and Macher, G. (2017, January 12\u201315). Safety and security co-engineering and argumentation framework. Proceedings of the International Conference on Computer Safety, Reliability, and Security, Trento, Italy.","key":"ref_19","DOI":"10.1007\/978-3-319-66284-8_24"},{"doi-asserted-by":"crossref","unstructured":"Sljivo, I., Gallina, B., Carlson, J., Hansson, H., and Puri, S. (2018, January 18\u201322). Tool-supported safety-relevant component reuse: From specification to argumentation. Proceedings of the Ada-Europe International Conference on Reliable Software Technologies, Lisbon, Portugal.","key":"ref_20","DOI":"10.1007\/978-3-319-92432-8_2"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/s10515-017-0230-5","article-title":"Tool support for assurance case development","volume":"25","author":"Denney","year":"2018","journal-title":"Autom. Softw. Eng."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2692956.2663177","article-title":"Resolute: An assurance case language for architecture models","volume":"34","author":"Gacek","year":"2014","journal-title":"ACM SIGAda Ada Lett."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/MC.2018.2876051","article-title":"A formal approach to constructing secure air vehicle software","volume":"51","author":"Cofer","year":"2018","journal-title":"Computer"},{"unstructured":"Hart, E.L. (2020, February 01). Introduction to Model-Based System Engineering (MBSE) and SysML. Available online: https:\/\/www.incose.org\/docs\/default-source\/delaware-valley\/mbse-overview-incose-30-july-2015.pdf.","key":"ref_24"},{"unstructured":"Feiler, P.H., and Gluch, D.P. (2012). Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, Addison-Wesley.","key":"ref_25"},{"doi-asserted-by":"crossref","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., and Sha, L. (2012, January 3\u20135). Compositional verification of architectural models. Proceedings of the NASA Formal Methods Symposium, Norfolk, VA, USA.","key":"ref_26","DOI":"10.1007\/978-3-642-28891-3_13"},{"doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., and Plaice, J. (1987, January 21\u201323). Lustre: A Declarative Language for Programming Synchronous Systems. Proceedings of the Fourteenth Annual {ACM} Symposium on Principles of Programming Languages, Munich, Germany.","key":"ref_27","DOI":"10.1145\/41625.41641"},{"unstructured":"(2021, February 01). VERDICT Github Repository. Available online: https:\/\/github.com\/ge-high-assurance\/VERDICT.","key":"ref_28"},{"unstructured":"Siu, K., Herencia-Zapana, H., Manolios, P., Noorman, M., and Haadsma, R. (2021, February 27). Safe and Optimal Techniques Enabling Recovery, Integrity, and Assurance; NASA Contractor Report, Available online: https:\/\/ntrs.nasa.gov\/citations\/20190027401.","key":"ref_29"},{"doi-asserted-by":"crossref","unstructured":"Banach, R., and Bozzano, M. (2006, January 27\u201329). Retrenchment, and the generation of fault trees for static, dynamic and cyclic systems. Proceedings of the International Conference on Computer Safety, Reliability, and Security SAFECOMP, Gdansk, Poland.","key":"ref_30","DOI":"10.1007\/11875567_10"},{"unstructured":"(2019, September 23). Safety Analysis with Error Model V2. Available online: https:\/\/github.com\/osate\/osate2\/blob\/master\/emv2\/org.osate.aadl2.errormodel.help\/markdown\/safetyanalysis.md.","key":"ref_31"},{"unstructured":"Delange, J., and Hugues, J. (2020, November 12). Safety Analysis with AADL. Available online: http:\/\/www.openaadl.org\/downloads\/tutorial_models15\/part5-safety.pdf.","key":"ref_32"},{"doi-asserted-by":"crossref","unstructured":"Hugues, J., and Delange, J. (2017). Model-Based Design and Automated Validation of ARINC653 Architectures Using the AADL. Cyber-Physical System Design from an Architecture Analysis Viewpoint, Springer.","key":"ref_33","DOI":"10.1007\/978-981-10-4436-6_2"},{"unstructured":"MITRE (2020, November 16). Common Attack Pattern Enumeration and Classification. Available online: https:\/\/capec.mitre.org\/.","key":"ref_34"},{"unstructured":"National Institute of Standards and Technology (NIST) (2017). NIST Special Publication (SP) 800-53 Revision 5 (Draft), Security and Privacy Controls for Systems and Organizations, National Institute of Standards and Technology.","key":"ref_35"},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"11-03-02-0005","DOI":"10.4271\/11-03-02-0005","article-title":"Threat Identification and Defense Control Selection for Embedded Systems","volume":"3","author":"Moitra","year":"2020","journal-title":"SAE Int. J. Transp. Cyber. Priv."},{"unstructured":"(2021, February 01). NIST 800-53 Controls, Available online: https:\/\/nvd.nist.gov\/800-53\/Rev4.","key":"ref_37"},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1142\/S1793351X13500025","article-title":"Toward a unified English-like representation of semantic models, data, and graph patterns for subject matter experts","volume":"7","author":"Crapo","year":"2013","journal-title":"Int. J. Semant. Comput."},{"unstructured":"(2021, February 12). OWL: Web Ontology Language. Available online: https:\/\/www.w3.org\/OWL\/.","key":"ref_39"},{"unstructured":"(2020, November 16). Xtext: Language Engineering for Everyone! . Available online: http:\/\/www.eclipse.org\/Xtext\/.","key":"ref_40"},{"unstructured":"Schneier, B. (2021, February 27). Attack Trees. Available online: https:\/\/www.schneier.com\/academic\/archives\/1999\/12\/attack_trees.html.","key":"ref_41"},{"doi-asserted-by":"crossref","unstructured":"Jurgenson, A., and Willemson, J. (2007). Processing multi-parameter attack trees with estimated parameter values. Information and Computer Security, Springer.","key":"ref_42","DOI":"10.1007\/978-3-540-75651-4_21"},{"doi-asserted-by":"crossref","unstructured":"Kordy, B., Radomirovic, S., Mauw, S., and Schweitzer, P. (2010). Foundations of attack-defense trees. Workshop on Formal Aspects of Security and Trust, Springer.","key":"ref_43","DOI":"10.1007\/978-3-642-19751-2_6"},{"key":"ref_44","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1093\/logcom\/exs029","article-title":"Attack\u2013defense trees","volume":"24","author":"Kordy","year":"2014","journal-title":"J. Log. Comput."},{"doi-asserted-by":"crossref","unstructured":"Siu, K., Herencia-Zapana, H., Prince, D., and Moitra, A. (2020, January 31). A model-based framework for analyzing the security of system architectures. Proceedings of the Reliability and Maintainability Symposisum, Palm Springs, CA, USA.","key":"ref_45","DOI":"10.1109\/RAMS48030.2020.9153607"},{"unstructured":"(2020, November 12). Bayes for Beginners: Probability and Likelihood. Available online: https:\/\/www.psychologicalscience.org\/observer\/bayes-for-beginners-probability-and-likelihood.","key":"ref_46"},{"doi-asserted-by":"crossref","unstructured":"Javaid, A., Sun, W., Devabhaktuni, V., and Alam, M. (2012, January 13\u201315). Cyber Security Threat Analysis and Modeling of an Unmanned Aerial Vehicle System. Proceedings of the IEEE Conference on Technology for Homeland Security (HST), Waltham, MA, USA.","key":"ref_47","DOI":"10.1109\/THS.2012.6459914"},{"unstructured":"De Moura, L., and Nikolaj, B. (April, January 29). Z3: An efficient SMT solver. Proceedings of the International conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Hungary.","key":"ref_48"},{"doi-asserted-by":"crossref","unstructured":"Bloomfield, R., and Netkachova, K. (2014, January 15). Building Blocks for Assurance Cases. Proceedings of the IEEE International Symposium on Software Reliability Engineering Workshops, Naples, Italy.","key":"ref_49","DOI":"10.1109\/ISSREW.2014.72"},{"unstructured":"Baoluo, M., Meng, B., Moitra, A., Crapo, A.W., Paul, S., Siu, K., Durling, M., Prince, D., and Herencia-Zapana, H. (2020, January 11\u201315). Towards Developing Formalized Assurance Cases. Proceedings of the 2020 IEEE\/AIAA 39th Digital Avionics Systems Conference (DASC), San Antonio, TX, USA.","key":"ref_50"},{"unstructured":"Kelly, T., and Weaver, R. (2004, January 1). The Goal Structuring Notation\u2014A Safety Argument Notation. Proceedings of the Dependable Systems and Networks 2004 Workshop on Assurance Cases, Florence, Italy.","key":"ref_51"},{"doi-asserted-by":"crossref","unstructured":"Hawkins, R., Habli, I., Kolovos, D., Paige, R., and Kelly, T. (2015, January 8\u201310). Weaving an Assurance Case from Design: A Model-Based Approach. Proceedings of the IEEE 16th International Symposium on High Assurance Systems Engineering, Daytona Beach Shores, FL, USA.","key":"ref_52","DOI":"10.1109\/HASE.2015.25"},{"doi-asserted-by":"crossref","unstructured":"Champion, A., Alain, M., Christoph, S., and Cesare, T. (2016, January 17\u201323). The Kind 2 model checker. Proceedings of the International Conference on Computer Aided Verification, Toronto, ON, Canada.","key":"ref_53","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Inf. Comput."}],"container-title":["Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2079-8954\/9\/1\/18\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T05:32:10Z","timestamp":1760160730000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2079-8954\/9\/1\/18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,3]]},"references-count":54,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2021,3]]}},"alternative-id":["systems9010018"],"URL":"https:\/\/doi.org\/10.3390\/systems9010018","relation":{},"ISSN":["2079-8954"],"issn-type":[{"type":"electronic","value":"2079-8954"}],"subject":[],"published":{"date-parts":[[2021,3,3]]}}}