  We consider the problem of securing a given control loop implementation of a
cyber-physical system (CPS) in the presence of Man-in-the-Middle attacks on
data exchange between plant and controller over a compromised network. To this
end, there exist various detection schemes that provide mathematical guarantees
against such attacks for the theoretical control model. However, such
guarantees may not hold for the actual control software implementation. In this
article, we propose a formal approach towards synthesizing attack detectors
with varying thresholds which can prevent performance degrading stealthy
attacks while minimizing false alarms.
