Lalaith Astor Technical Consulting House, LLC — Department of Defense SBIR Phase II: HR001121S0007-08

Description

High-risk, cyber-physical systems are open to potential anomalies, vulnerabilities, and defects that can have a significant impact on the warfighter from the perspective of security, functionality, and operational capabilities. While security and safety-critical physical devices must undergo regulatory approval, quality management system (QMS) frameworks and a reliance on manufacturer testing are insufficient to mitigate the inherent risks. In the medical domain, medical device recalls have seen a rise from 409.5 million units (2016-2017) to 595.98 million units (2018-2019. Five years ago, recalls were due to device design issues and product control; today, recalls are largely due to software anomalies, false results, and network connection issues. While medical innovation drives needed enhancements, the degradation in quality is a result of architecture-level redesigns and the failure of testing to verify that the device continues to meet its quality goals. FDA’s recall database shows that more than ten percent of Class III medical device recalls are the result of software failures in firmware. Ensuring safety, security, and viability requires a rigorous, effective, and independent verification solution. The QMS framework relies on manufacturers to meet quality requirements and does not guarantee verification of identified device states or offer independent verification outside of a review of manufacturer-provided output. Third parties will benefit from a methodology and tool set that supports the identification of anomalies and vulnerabilities.  We propose to use rigorous development and analysis technologies to enable faster and more accurate identification of software and firmware vulnerabilities and defects in physical devices and to provide direct evidence that the device implements its system, design, and user requirements. Our goal is to formalize an efficient and comprehensive Model Based Testing (MBT) methodology, abstract model, and tool sets using lightweight formal methods that can be commercialized for Government or third-party customers to test and validate resource limited, embedded systems in a small number of days. A secondary goal is to provide our product to manufacturers to enhance verification of their high-risk devices. In previous research, we showed that it is feasible to construct a reference model and an assurance case using the models and analysis artifacts. The remaining challenge is to connect reference modeling techniques with modern software analysis and model extraction techniques, which allows test groups to automate and streamline the collection of evidence and accelerate the approval process. We will create an abstract formal model of a generic AED and then map the abstract model to a low-level model of a vendor’s AED firmware. With MBT, the invariants from the abstract model will be verified to ensure that the vendor’s implementation conforms to the safety and security invariants claimed in the abstract model.