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 andrecover from attacks or safely shutdown. As there are few development tools for cyber resiliency, designers rely on guidelinesand checklists, sometimes missing vulnerabilities until late in the process where remediation is expensive. Our solution is amodel-based approach with cyber resilience-improving transforms that insert high-assurance components such as filters toblock malicious data or monitors to detect and alarm anomalous behavior. Novel is our use of model checking and a verifiedcompiler to specify, verify, and synthesize these components. We define code contracts as formal specifications that designerswrite for high-assurance components, and test contracts as tests to validate their behavior. A model checker proves whetheror not code contracts satisfy test contracts in an iterative development cycle. The same model checker also proves whether ornot a system with the inserted components, assuming they adhere to their code contracts, provides the desired cyber resiliencyfor the system. We define an algorithm to synthesize implementations for code contracts in a semantics-preserving way thatis backed by a verified compiler. The entire workflow is implemented as part of the open source BriefCASE toolkit. Wereport on our experience using BriefCASE with a case study on a UAV system that is transformed to be cyber resilient tocommunication and supply chain cyber attacks. Our case study demonstrates that writing code contracts and then synthesizingcorrect implementations from them are feasible in real-world systems engineering for cyber resilience.