Skip to main content
Springer Nature Link
Log in

Opportunities and Challenges in Monitoring Cyber-Physical Systems Security

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice (ISoLA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11247))

Included in the following conference series:

Abstract

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 is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
CHF34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
CHF 24.95
Price includes VAT (Switzerland)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
CHF 47.00
Price excludes VAT (Switzerland)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
CHF 59.00
Price excludes VAT (Switzerland)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  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. 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). https://doi.org/10.1007/978-3-642-19835-9_21

    Chapter  MATH  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-75632-5_5

    Chapter  Google Scholar 

  4. Berkovich, S., Bonakdarpour, B., Fischmeister, S.: Runtime verification with minimal intrusion through parallelism. Form. Methods Syst. Des. 46(3), 317–348 (2015)

    Article  MATH  Google Scholar 

  5. Blaze, M., et al.: Dynamic trust management. Computer 42(2), 44–52 (2009)

    Article  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-46982-9_4

    Chapter  Google Scholar 

  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. 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. 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). https://doi.org/10.1007/978-3-662-54580-5_5

    Chapter  Google Scholar 

  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. Checkoway, S., et al.: Comprehensive experimental analyses of automotive attack surfaces. In: USENIX Security Symposium, San Francisco (2011)

    Google Scholar 

  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). https://doi.org/10.1007/978-3-642-54792-8_15

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-24953-7_35

    Chapter  MATH  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-11164-3_19

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-67531-2_12

    Chapter  Google Scholar 

  18. Greenberg, A.: Hackers remotely kill a jeep on the highway? With me in it. Wired 7, 21 (2015)

    Google Scholar 

  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. 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. 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. Jovanov, I., Pajic, M.: Relaxing integrity requirements for resilient control systems. CoRR, abs/1707.02950 (2017)

    Google Scholar 

  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 2017

    Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  25. Kolias, C., Kambourakis, G., Stavrou, A., Voas, J.: DDoS in the IoT: mirai and other botnets. Computer 50(7), 80–84 (2017)

    Article  Google Scholar 

  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. 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 2017

    Google Scholar 

  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)

    Article  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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). https://doi.org/10.1007/978-3-540-30206-3_12

    Chapter  MATH  Google Scholar 

  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. 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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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 2014

    Google Scholar 

  37. Savage, S.: Modern automotive vulnerabilities: causes, disclosures, and outcomes (2016)

    Google Scholar 

  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). https://doi.org/10.1007/978-3-319-23820-3_15

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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 2010

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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 

Download references

Acknowledgment

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.

Author information

Authors and Affiliations

  1. Iowa State University, Ames, USA

    Borzoo Bonakdarpour

  2. University of Southern California, Los Angeles, USA

    Jyotirmoy V. Deshmukh

  3. Duke University, Durham, USA

    Miroslav Pajic

Authors
  1. Borzoo Bonakdarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jyotirmoy V. Deshmukh
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Miroslav Pajic
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Borzoo Bonakdarpour .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bonakdarpour, B., Deshmukh, J.V., Pajic, M. (2018). Opportunities and Challenges in Monitoring Cyber-Physical Systems Security. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science(), vol 11247. Springer, Cham. https://doi.org/10.1007/978-3-030-03427-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03427-6_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03426-9

  • Online ISBN: 978-3-030-03427-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation

  NODES
INTERN 6
Note 2