Formal Synthesis of Monitoring and Detection Systems for Secure CPS Implementations
Ipsita Koley1,a, Saurav Kumar Ghosh1,b, Soumyajit Dey1,c, Debdeep Mukhopadhyay1,d, Amogh Kashyap K N2,e, Sachin Kumar Singh2,f, Lavanya Lokesh2,g, Jithin Nalu Purakkal2,h and Nishant Sinha2,i
1Indian Institute of Technology, Kharagpur
aipsitakoley@iitkgp.ac.in
bsaurav.kumar.ghosh@cse.iitkgp.ernet.in
csoumyajit@iitkgp.ac.in
ddebdeep@iitkgp.ac.in
2Robert Bosch Engineering and Business Solutions Private Limited
eAmogh.Kashyap@in.bosch.com
fSachinKumar.Singh@in.bosch.com
gLokesh.Lavanya@in.bosch.com
hJithin.NaluPurakkal2@in.bosch.com
iSinha.Nishant@in.bosch.com
ABSTRACT
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 exists various detection schemes which 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.
Keywords: Cyber Physical System, False data injection attack, Formal method, Residue based detector.
