A Modest Security Analysis of Cyber-Physical Systems: A Case Study

  • Ruggero Lanotte
  • Massimo MerroEmail author
  • Andrei Munteanu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10854)


Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes. Although the range of applications of CPSs include several critical domains, their verification and validation often relies on simulation-test systems rather then formal methodologies. In this paper, we use a recent version of the expressive Modest Toolset to implement a non-trivial engineering application, and test its safety model checker prohver as a formal instrument to statically detect a variety of cyber-physical attacks, i.e., attacks targeting sensors and/or actuators, with potential physical consequences. We then compare the effectiveness of the Modest Toolset and its safety model checker in verifying CPS security properties when compared to other state-of-the-art model checkers.



We thank the anonymous reviewers for their insightful and careful reviews that allowed us to significantly improve the paper. We thank Fabio Mogavero for stimulating discussions on model checking tools, and Arnd Hartmanns for “tips and tricks” on the Modest Toolset. This work has been partially supported by the project “Dipartimenti di Eccellenza 2018–2022” funded by the Italian Ministry of Education, Universities and Research (MIUR).


  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: D’Argenio, P., Miner, A., Rubino, G. (eds.) QEST 2006, pp. 125–126. IEEE Computer Society (2006). DOIurl10.1109/QEST.2006.59Google Scholar
  3. 3.
    Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116–131. Springer, Cham (2014). Scholar
  4. 4.
    Bohnenkamp, H., Hermanns, H., Katoen, J.-P.: motor: the modest tool environment. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 500–504. Springer, Heidelberg (2007). Scholar
  5. 5.
    Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). Scholar
  6. 6.
    Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68–82. Springer, Heidelberg (2015). Scholar
  7. 7.
    Falliere, N., Murchu, L., Chien, E.: W32.Stuxnet Dossier (2011)Google Scholar
  8. 8.
    Frehse, G.: Phaver Language Overview v0.35 (2006).
  9. 9.
    Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. Int. J. Softw. Tools Technol. Transf. 10(3), 263–279 (2008)CrossRefGoogle Scholar
  10. 10.
    Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). Scholar
  11. 11.
    Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191–232 (2013)CrossRefGoogle Scholar
  12. 12.
    Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593–598. Springer, Heidelberg (2014). Scholar
  13. 13.
    Hennessy, M., Regan, T.: A process algebra for timed systems. Inf. Comput. 117(2), 221–239 (1995)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNetCrossRefGoogle Scholar
  15. 15.
    ICS-CERT: Cyber-Attack Against Ukrainian Critical Infrastructure.
  16. 16.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). Scholar
  17. 17.
    Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal hybrid systems. Math. Contr. Sig. Syst. 13(1), 1–21 (2000)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Lanotte, R., Merro, M.: A semantic theory of the Internet of Things. Inf. Comput. 259(1), 72–101 (2018)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Lanotte, R., Merro, M., Muradore, R., Viganò, L.: A formal approach to cyber-physical attacks. In: CSF 2017, pp. 436–450. IEEE Computer Society (2017).
  20. 20.
    Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I/O automata. Inf. Comput. 185(1), 105–157 (2003)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Nigam, V., Talcott, C., Aires Urquiza, A.: Towards the automated verification of cyber-physical security protocols: bounding the number of timed intruders. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 450–470. Springer, Cham (2016). Scholar
  22. 22.
    Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High. Order Symb. Comput. 20(1–2), 161–196 (2007)CrossRefGoogle Scholar
  23. 23.
    Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embed. Comput. Syst. 6(1), 8 (2007)CrossRefGoogle Scholar
  24. 24.
    Rocchetto, M., Tippenhauer, N.O.: CPDY: extending the Dolev-Yao attacker with physical-layer interactions. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 175–192. Springer, Cham (2016). Scholar
  25. 25.
    Rocchetto, M., Tippenhauer, N.O.: On attacker models and profiles for cyber-physical systems. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 427–449. Springer, Cham (2016). Scholar
  26. 26.
    Roohi, N.: Remedies for building reliable cyber-physical systems. Ph.D. thesis, University of Illinois at Urbana-Champaign (2017)Google Scholar
  27. 27.
    Slay, J., Miller, M.: Lessons learned from the Maroochy Water Breach. In: Goetz, E., Shenoi, S. (eds.) ICCIP 2007. IIFIP, vol. 253, pp. 73–82. Springer, Boston, MA (2008). Scholar
  28. 28.
    Vigo, R.: The cyber-physical attacker. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP 2012. LNCS, vol. 7613, pp. 347–356. Springer, Heidelberg (2012). Scholar
  29. 29.
    Vigo, R.: Availability by design: a complementary approach to denial-of-service. Ph.D. thesis, Danish Technical University (2015)Google Scholar
  30. 30.
    Vladimerou, V., Prabhakar, P., Viswanathan, M., Dullerud, G.: STORMED hybrid systems. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 136–147. Springer, Heidelberg (2008). Scholar
  31. 31.
    Zacchia Lun, Y., D’Innocenzo, A., Malavolta, I., Di Benedetto, M.D.: Cyber-Physical Systems Security: a Systematic Mapping Study. CoRR abs/1605.09641 (2016).

Copyright information

© IFIP International Federation for Information Processing 2018

Authors and Affiliations

  • Ruggero Lanotte
    • 1
  • Massimo Merro
    • 2
    Email author
  • Andrei Munteanu
    • 2
  1. 1.Dipartimento di Scienza e Alta TecnologiaUniversità dell’InsubriaComoItaly
  2. 2.Dipartimento di InformaticaUniversità degli Studi di VeronaVeronaItaly

Personalised recommendations