ARBITER & UPSAT: Assuring Open Source Software
Howard Reubenstein (STR) and Greg Eakman(STR), howard.reubenstein@str.us
The ARBITER system (developed as part of the DARPA ARCOS program) provides support for the development of evidence-based system assurance cases. ARBITER has been applied to subsystems of the open source UPSat satellite system (https://upsat.gr/). Analysis of the Watchdog timer subsystem revealed latent errors in the communications subsystem.
ARBITER formulates assurance arguments based on the use of reasoning templates which encapsu-late vetted reasoning strategies thus avoiding the temptation to just “make stuff up” using the under-lying claims, argument, evidence (CAE) representation. Evidence, such as systems engineering arti-facts, requirements, SysML models, static analysis, and test results support the assurance claims. Evidence-based assurance focuses on analysis of the system and models (causal and evidentiary) of the system as opposed to weaker arguments based on, e.g., process compliance or other checklists.
Safety and security requirements must often be written as a negative, such as “shall not”, but these are difficult to verify. To support the assurance of these requirements for UPSat, we developed causal models to compute confidence in the intended software behavior based on contract-driven specifications and Bayesian probability reasoning. Using evidence from instrumentation traces, the confidence measures detected a weakness in the communication system’s Watchdog without directly observing the faulty behavior.
Assurance activities start with definition of mission critical claims to be supported. While systems can be compromised due to fundamental programming vulnerabilities, the system can also have its in-tended functionality used against it and this requires assurance of system specific claims. Evidentiary support for these claims is derived from models underlying the template library. Templates are used to harvest evidence from underlying artifact repositories and include queries that return information that provides the required evidentiary support. The confidence measures associated with causal models are combined with support measures to provide an overall evidentiary support measure for the assur-ance case.
Evidence can be introduced into ARBITER incrementally to support the overall CONOPS of continu-ous assurance. Evidentiary support behind claims will increase over time and problems based on counter-evidence may be discovered. The goal is to asymptotically increase support for mission criti-cal claims so that assurance is no longer a from scratch, “all at once” effort tacked on to the end of system development.
We view the informal argumentation of assurance cases as providing the glue for multiple types of ev-idence including formal proofs. There is no single proof that verifies all the mission critical claims as-sociated with a system. The assurance case can put proof results into a context that highlights their importance and impact on system claims. Leaf claims in the assurance case can also represent proof obligations.
Distribution Statement `A' (Approved for Public Release, Distribution Unlimited). The views,
opinions, and/or findings expressed are those of the author(s) and should not be interpreted as rep-resenting the official views or policies of the Department of Defense or the U.S. Government.
Dr. Howard Reubenstein has more than 25 years experience leading projects related to secure software design, implementation and analysis. At STR he serves as the PI for the ARBITER assurance project under DARPA’s ARCOS program and as co-PI for a project focusing on supporting independent verification and validation of software. He also served as the PI for the Verified Autonomous Agents for Controlled Cleansing of Infected NEtworks (VACCINE) project – the anti-bot-net agent; and the Minimizing Attack Surface thru configuration OptimizatioN (MASON) project -- a DARPA project to derive secure configurations for complex systems. He also served as deputy PI on DARPA’s CRASH/SAFE program leading program demonstration efforts and guiding interaction with “voice of the offense.” Dr Reubenstein received his PhD from MIT's Artificial Intelligence laboratory exploring the application of logical reasoning systems to software requirements acquisition.