Program Synthesis for Cyber-Resilience
Néstor Cataño · IEEE Transactions on Software Engineering · 2022
Architectural tactics enable stakeholders to achieve cyber-resilience requirements. They permit systems to react, resist, detect, and recover from cyber incidents. This paper presents an approach to generate source code for architectural tactics typically used in safety and mission-critical systems. Our approach extensively relies on the use of theEvent-Bformal method and theEventB2Javacode generation plugin of the Rodin platform. It leverages the modeling of architectural tactics in theEvent-Bformal language and uses a set ofEventB2Javatransformation rules to generate certified code implementations for the said tactics. Since resilience requirements are statements about a system over time, and because of the fact that theEvent-Blanguage does not provide (native) support for the writing of temporal specifications, we have implemented a novel Linear Temporal Logic (LTL) extension forEvent-B. We support several architectural tactics for availability, performance, and security. The generated code is certified in the following sense: discharging proof obligations in Rodin - the platform we use for writing theEvent-Bmodels - attests to the soundness of the architectural tactics modelled inEvent-B, and the soundness of the translation encoded by theEventB2Javatool attests to the code correctness. Finally, we demonstrate the usability of our resilience validation approach with the aid of an Autonomous Vehicle System. It further helped us increase our confidence in the soundness of our Event-B LTL extension.