Secure-by-Construction Synthesis of Cyber-Physical Systems

TL;DR

This paper advocates for integrating security considerations into the correct-by-construction synthesis process of cyber-physical systems, emphasizing the need for security to be built into the design rather than verified post hoc.

Contribution

It presents a vision for secure-by-construction synthesis, combining recent advances in formal methods, security properties, and hyperproperties to address security in safety-critical cyber-physical systems.

Findings

Progress in scaling correct-by-construction synthesis for cyber-physical systems

Recent developments in opacity and hyperproperties for security

Open challenges in integrating security into formal synthesis processes

Abstract

Correct-by-construction synthesis is a cornerstone of the confluence of formal methods and control theory towards designing safety-critical systems. Instead of following the time-tested, albeit laborious (re)design-verify-validate loop, correct-by-construction methodology advocates the use of continual refinements of formal requirements -- connected by chains of formal proofs -- to build a system that assures the correctness by design. A remarkable progress has been made in scaling the scope of applicability of correct-by-construction synthesis -- with a focus on cyber-physical systems that tie discrete-event control with continuous environment -- to enlarge control systems by combining symbolic approaches with principled state-space reduction techniques. Unfortunately, in the security-critical control systems, the security properties are verified ex post facto the design process in a way that undermines the correct-by-construction paradigm. We posit that, to truly realize the dream of correct-by-construction synthesis for security-critical systems, security considerations must take center-stage with the safety considerations. Moreover, catalyzed by the recent progress on the opacity sub-classes of security properties and the notion of hyperproperties capable of combining security with safety properties, we believe that the time is ripe for the research community to holistically target the challenge of secure-by-construction synthesis. This paper details our vision by highlighting the recent progress and open challenges that may serve as bricks for providing a solid foundation for secure-by-construction synthesis of cyber-physical systems.