Reasoning with Assurance Arguments under Uncertainty – Composing Formal and Non-Formal
A significant challenge in automating certification of software intensive complex computing systems is information heterogeneity that runs the gamut from non-formal artifacts such as safety analyses, operational guidance, unit tests, and simulation runs to, more recently, formal artifacts. An emerging approach to certification of such software systems is the use of assurance cases to provide goal-based arguments supported by evidence. Confidence in the assurance case is dependent on the uncertainty associated with context, modeling assumptions and simplifications, inherent uncertainty in the underlying evidence, and just as importantly, the uncertainty in the logical reasoning used to compose the information into an argumentation structure. We present a calculus to analyze assurance cases involving multiple types of evidence holistically in the presence of uncertainty, a necessary initial step towards automated reasoning capability that will reduce the time and effort necessary to certify software through its evolutionary cycle while increasing confidence in the results. We leverage recent work in integrating formal methods as evidence in assurance cases [1, 2] and reusable argument patterns to help guide automating assurance analysis [3]. Our approach explores a fusion of type theory, argumentation logic, and error propagation that enables us to reason over various forms of evidence and argument structures including formal and non-formal evidence influenced by both statistical and epistemic uncertainty within a single assurance case. We illustrate this technique through a case study based on real-world avionics certification evidence.
References:
[1] Denney, Ewen, and Ganesh Pai. "Evidence arguments for using formal methods in software certification." 2013 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). IEEE, 2013.
[2] Fisher, Kathleen. “Using Formal Methods to Enable More Secure Vehicles: DARPA's HACMS Program.” http://verificationinstitute.org/wp-content/uploads/sites/28/2014/05/HACMS-Fisher.pdf, 16 September, 2014
[3] Szczygielska, Monika, and Aleksander Jarzębowicz. "Assurance case patterns on-line catalogue." Advances in Dependability Engineering of Complex Systems. Springer, Cham, 2017. 407-417.
Sumit Ray is the Principal Investigator leading BAE Systems Fast-Labs cyber-resilience systems research protecting military weapons platforms and commercial vehicles from cyber-attacks. He has over 26 years of experience with high confidence embedded systems and seven years as a lead cyberwarfare researcher at Fast-Labs. He has led several DARPA programs researching a wide variety of topics from network traffic analysis on EdgeCT to semantically aware secure hosts on CRASH and adaptive model-based software on DMT. On the DARPA Disruptive Manufacturing Technologies (DMT) program, Sumit and his team developed and demonstrated a model-based tool integration, adaptation, formal verification and reverse engineering infrastructure to enable an order-of-magnitude improvement in time and cost of manufacturing complex, control system software. For this work, he and his team was awarded the BAE Systems Chairman’s
Dr. Cathey is a Sr. Principal Research Scientist at BAE Systems/FAST Labs. She has over fifteen years of experience in machine learning and network traffic analysis. Dr. Cathey received her PhD from Illinois Institute of technology where she led the Information Retrieval laboratory in a variety of machine learning projects. Dr. Cathey has experience with a variety of DoD projects including a) PI on DARPA APAC where she applied clustering to binary analysis; b) co-PI on AFRL ADCO where she built models of network traffic behavior; c) PI on IARPA CAUSE where she applied machine learning to open source analytics; and d) currently, co-PI on DARPA EdgeCT.
Dr. Paul Vines is a Principal Scientist in the Cyber Technology product line of FAST Labs, with over six years of experience in software and networking security. Dr. Vines received his PhD from University of Washington where he performed research on information flow assurance of software using type-based static analysis to detect malicious application. He also conducted research on network security and privacy, including pioneering a new form of digital surveillance (ADINT). At BAE he has performed network graph inference and analysis research in conjunction with participation in the DARPA EdgeCT program to provide resilient networking.
Dr. Allyson O’Brien is a Principal Scientist in the Cyber Technology product line of FAST Labs, with over nine years of experience in mathematical modeling. Dr. O’Brien has performed on several cyber security research projects, and is formerly a commercial helicopter pilot who has worked with FAA maintenance regulations.