Synthesizing Verified Components for Cyber Assured Systems Engineering
Cyber-physical systems, such as avionics, must be tolerant to cyber-attacks in the same way they are tolerant to random faults: they recover or safely shut down as requirements dictate. The DARPA Cyber Assured Systems Engineering program is developing design, analysis, and verification tools that enable systems engineers to design-in this cyber-resiliency in a Model-Based Systems Engineering environment. This paper discusses the automated model transformations that add in high-assurance components. These components are filters and monitors that prevent malicious input and detect supply chain attacks respectively. A formal specification defines each component and is used to verify that the component addresses system level cyber-requirements. Implementations are synthesized from the specification, and that synthesis is proven to preserve the exact meaning of the specification. The transformations are integrated into the Open Source AADL Tool Environment (OSATE). The paper further reports a case study applying these transformations to a UAV system that uses the Air Force Research Laboratory’s OpenUxAS services for route planning. Here the transforms add filters to guard against malformed input and monitors to guard against ground station spoofing and malicious flight plans from OpenUxAS.
Sat 16 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
00:00 - 01:00
|Model-Based Development of Engine Control Systems: Experiences and Lessons LearntP&I
|Exploring Architectural Design Decisions in Industry 4.0: A Literature Review and TaxonomyFT
|Synthesizing Verified Components for Cyber Assured Systems EngineeringP&I