  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.
