Opportunities and Challenges in Monitoring Cyber-Physical Systems Security

  • Borzoo BonakdarpourEmail author
  • Jyotirmoy V. Deshmukh
  • Miroslav Pajic
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11247)


Technological advances in distributed cyber-physical systems (CPS) will fundamentally alter the way present and future human societies lead their lives. From a security or privacy perspective, a (multi-agent) cyber-physical system is a network of sensors, actuators, and computation nodes, i.e., a system with multiple attack surfaces and latent exploits that originate both through software attacks and physical attacks. In this paper, we argue that we are in pressing need to bring about a paradigm shift in software development for multi-agent CPS. To this end, security and privacy policies should be made a critical ingredient of agent interfaces with a goal of ensuring both localized safety and privacy for each agent, as well as guaranteeing global system safety and security. We present our vision on new theory, algorithms, and tools to foster a culture of secure-by-design multi-agent CPS.



This research has been partially supported by the NSF SaTC-1813388, a grant from Iowa State University, NSF CNS-1652544 and the ONR under agreements number N00014-17-1-2012 and N00014-17-1-2504.


  1. 1.
    Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium, CSF, pp. 239–252 (2016)Google Scholar
  2. 2.
    Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011). Scholar
  3. 3.
    Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135–175. Springer, Cham (2018). Scholar
  4. 4.
    Berkovich, S., Bonakdarpour, B., Fischmeister, S.: Runtime verification with minimal intrusion through parallelism. Form. Methods Syst. Des. 46(3), 317–348 (2015)CrossRefGoogle Scholar
  5. 5.
    Blaze, M., et al.: Dynamic trust management. Computer 42(2), 44–52 (2009)CrossRefGoogle Scholar
  6. 6.
    Bonakdarpour, B., Finkbeiner, B.: Runtime verification for HyperLTL. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 41–45. Springer, Cham (2016). Scholar
  7. 7.
    Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties. In: Proceedings of the 31st IEEE Computer Security Foundations Symposium, CSF, pp. 162–174 (2018)Google Scholar
  8. 8.
    Bonakdarpour, B., Sanchez, C., Schneider, G.: Monitoring hyperproperties by combining static analysis and runtime verification. In: International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA (2018, to appear)Google Scholar
  9. 9.
    Brett, N., Siddique, U., Bonakdarpour, B.: Rewriting-based runtime verification for alternation-free HyperLTL. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 77–93. Springer, Heidelberg (2017). Scholar
  10. 10.
    Candea, G., Kawamoto, S., Fujiki, Y., Friedman, G., Fox, A.: Microreboot-a technique for cheap recovery. In: OSDI, vol. 4, pp. 31–44 (2004)Google Scholar
  11. 11.
    Checkoway, S., et al.: Comprehensive experimental analyses of automotive attack surfaces. In: USENIX Security Symposium, San Francisco (2011)Google Scholar
  12. 12.
    Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). Scholar
  13. 13.
    Deshmukh, J., Horvat, M., Jin, X., Majumdar, R., Prabhu, V.S.: Testing cyber-physical systems through bayesian optimization. ACM Trans. Embed. Comput. Syst. 16(5s), 170:1–170:18 (2017)CrossRefGoogle Scholar
  14. 14.
    Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Form. Methods Syst. Des. 51, 5–30 (2017)CrossRefGoogle Scholar
  15. 15.
    Deshmukh, J., Jin, X., Kapinski, J., Maler, O.: Stochastic local search for falsification of hybrid systems. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 500–517. Springer, Cham (2015). Scholar
  16. 16.
    Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231–246. Springer, Cham (2014). Scholar
  17. 17.
    Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 190–207. Springer, Cham (2017). Scholar
  18. 18.
    Greenberg, A.: Hackers remotely kill a jeep on the highway? With me in it. Wired 7, 21 (2015)Google Scholar
  19. 19.
    Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Nickovic, D.: From signal temporal logic to FPGA monitors. In: 13th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE, pp. 218–227 (2015)Google Scholar
  20. 20.
    Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: Proceedings of Hybrid Systems: Computation and Control, pp. 253–262 (2014)Google Scholar
  21. 21.
    Jin, X., Donzé, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: Proceedings of Hybrid Systems: Computation and Control (2013)Google Scholar
  22. 22.
    Jovanov, I., Pajic, M.: Relaxing integrity requirements for resilient control systems. CoRR, abs/1707.02950 (2017)Google Scholar
  23. 23.
    Jovanov, I., Pajic, M.: Sporadic data integrity for secure state estimation. In: 2017 IEEE 56th Annual Conference on Decision and Control, CDC, pp. 163–169, December 2017Google Scholar
  24. 24.
    Kapinski, J., Deshmukh, J.V., Jin, X., Ito, H., Butts, K.: Simulation-based approaches for verification of embedded control systems: an overview of traditional and advanced modeling, testing, and verification techniques. IEEE Control Syst. 36(6), 45–64 (2016)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Kolias, C., Kambourakis, G., Stavrou, A., Voas, J.: DDoS in the IoT: mirai and other botnets. Computer 50(7), 80–84 (2017)CrossRefGoogle Scholar
  26. 26.
    Koscher, K., et al.: Experimental security analysis of a modern automobile. In: 2010 IEEE Symposium on Security and Privacy, SP, pp. 447–462. IEEE (2010)Google Scholar
  27. 27.
    Lesi, V., Jovanov, I., Pajic, M.: Network scheduling for secure cyber-physical systems. In: 2017 IEEE Real-Time Systems Symposium, RTSS, pp. 45–55, December 2017Google Scholar
  28. 28.
    Lesi, V., Jovanov, I., Pajic, M.: Security-aware scheduling of embedded control tasks. ACM Trans. Embed. Comput. Syst. 16(5s), 188:1–188:21 (2017)CrossRefGoogle Scholar
  29. 29.
    Li, J., Nuzzo, P., Sangiovanni-Vincentelli, A., Xi, Y., Li, D.: Stochastic contracts for cyber-physical system design under probabilistic requirements. In: ACM/IEEE International Conference on Formal Methods and Models for System Design (2017)Google Scholar
  30. 30.
    Liang, G., Weller, S.R., Zhao, J., Luo, F., Dong, Z.Y.: The 2015 Ukraine blackout: implications for false data injection attacks. IEEE Trans. Power Syst. 32(4), 3317–3318 (2017)CrossRefGoogle Scholar
  31. 31.
    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). Scholar
  32. 32.
    Mohan, S., Bak, S., Betti, E., Yun, H., Sha, L., Caccamo, M.: S3A: secure system simplex architecture for enhanced security and robustness of cyber-physical systems. In: Proceedings of the 2nd ACM International Conference on High Confidence Networked Systems, pp. 65–74. ACM (2013)Google Scholar
  33. 33.
    Pajic, M., Lee, I., Pappas, G.J.: Attack-resilient state estimation for noisy dynamical systems. IEEE Trans. Control Netw. Syst. 4(1), 82–92 (2017)MathSciNetCrossRefGoogle Scholar
  34. 34.
    Pajic, M., Mangharam, R., Pappas, G.J., Sundaram, S.: Topological conditions for in-network stabilization of dynamical systems. IEEE J. Sel. Areas Commun. 31(4), 794–807 (2013)CrossRefGoogle Scholar
  35. 35.
    Pajic, M., Weimer, J., Bezzo, N., Sokolsky, O., Pappas, G.J., Lee, I.: Design and implementation of attack-resilient cyberphysical systems: with a focus on attack-resilient state estimators. IEEE Control Syst. 37(2), 66–81 (2017)MathSciNetCrossRefGoogle Scholar
  36. 36.
    Pajic, M., et al.: Robustness of attack-resilient state estimators. In: ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS, pp. 163–174, April 2014Google Scholar
  37. 37.
    Savage, S.: Modern automotive vulnerabilities: causes, disclosures, and outcomes (2016)Google Scholar
  38. 38.
    Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 233–249. Springer, Cham (2015). Scholar
  39. 39.
    Seto, D., Krogh, B.H., Sha, L., Chutinan, A.: Dynamic control system upgrade using the simplex architecture. IEEE Control Syst. 18(4), 72–80 (1998)CrossRefGoogle Scholar
  40. 40.
    Sundaram, S., Pajic, M., Hadjicostis, C., Mangharam, R., Pappas, G.: The wireless control network: monitoring for malicious behavior. In: 49th IEEE Conference on Decision and Control, CDC, pp. 5979–5984, December 2010Google Scholar
  41. 41.
    Sundaram, S., Revzen, S., Pappas, G.: A control-theoretic approach to disseminating values and overcoming malicious links in wireless networks. Automatica 48(11), 2894–2901 (2012)MathSciNetCrossRefGoogle Scholar
  42. 42.
    West, A.G., et al.: QuanTM: a quantitative trust management system. In: Proceedings of the Second European Workshop on System Security, pp. 28–35. ACM (2009)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Borzoo Bonakdarpour
    • 1
    Email author
  • Jyotirmoy V. Deshmukh
    • 2
  • Miroslav Pajic
    • 3
  1. 1.Iowa State UniversityAmesUSA
  2. 2.University of Southern CaliforniaLos AngelesUSA
  3. 3.Duke UniversityDurhamUSA

Personalised recommendations