Synthesizing verified components for cyber assured systems engineering

Safety-critical systems such as avionics need to be engineered to be cyber resilient meaning that systems are able to detect and recover from attacks or safely shutdown. As there are few development tools for cyber resiliency, designers rely on guidelines and checklists, sometimes missing vulnerabilities until late in the process where remediation is expensive. Our solution is a model-based approach with cyber resilience-improving transforms that insert high-assurance components such as filters to block malicious data or monitors to detect and alarm anomalous behavior. Novel is our use of model checking and a verified compiler to specify, verify, and synthesize these components. We define code contracts as formal specifications that designers write for high-assurance components, and test contracts as tests to validate their behavior. A model checker proves whether or not code contracts satisfy test contracts in an iterative development cycle. The same model checker also proves whether or not a system with the inserted components, assuming they adhere to their code contracts, provides the desired cyber resiliency for the system. We define an algorithm to synthesize implementations for code contracts in a semantics-preserving way that is backed by a verified compiler. The entire workflow is implemented as part of the open source BriefCASE toolkit. We report on our experience using BriefCASE with a case study on a UAV system that is transformed to be cyber resilient to communication and supply chain cyber attacks. Our case study demonstrates that writing code contracts and then synthesizing correct implementations from them are feasible in real-world systems engineering for cyber resilience.