Systematic Classification of Attackers via Bounded Model Checking

  • Eric Rothstein-MorrisEmail author
  • Jun Sun
  • Sudipta Chattopadhyay
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11990)


In this work, we study the problem of verification of systems in the presence of attackers using bounded model checking. Given a system and a set of security requirements, we present a methodology to generate and classify attackers, mapping them to the set of requirements that they can break. A naive approach suffers from the same shortcomings of any large model checking problem, i.e., memory shortage and exponential time. To cope with these shortcomings, we describe two sound heuristics based on cone-of-influence reduction and on learning, which we demonstrate empirically by applying our methodology to a set of hardware benchmark systems.


  1. 1.
  2. 2.
  3. 3.
  4. 4.
  5. 5.
    Awedh, M., Somenzi, F.: Proving more properties with bounded model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 96–108. Springer, Heidelberg (2004). Scholar
  6. 6.
    Basin, D., Cremers, C.: Know your enemy: compromising adversaries in protocol analysis. ACM Trans. Inf. Syst. Secur. 17(2), 7:1–7:31 (2014). Scholar
  7. 7.
    Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)Google Scholar
  8. 8.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). Scholar
  9. 9.
    Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1–64 (2006)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr, Linz, Austria (2011)Google Scholar
  11. 11.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). Scholar
  12. 12.
    Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 1–14. Springer, Heidelberg (2012). Scholar
  13. 13.
    Cabodi, G., et al.: To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking. Int. J. Softw. Tools Technol. Transf. 20(3), 313–325 (2018). Scholar
  14. 14.
    Cabodi, G., Nocco, S.: Optimized model checking of multiple properties. In: 2011 Design, Automation Test in Europe, pp. 1–4, March 2011Google Scholar
  15. 15.
    Cabodi, G., Camurati, P., Quer, S.: A graph-labeling approach for efficient cone-of-influence computation in model-checking problems with multiple properties. Softw.: Pract. Exp. 46(4), 493–511 (2016).
  16. 16.
    Cabodi, G., et al.: Hardware model checking competition 2014: an analysis and comparison of model checkers and benchmarks. J. Satisf. Boolean Model. Comput. 9, 135–172 (2015)MathSciNetGoogle Scholar
  17. 17.
    Cárdenas, A.A., Amin, S., Lin, Z.S., Huang, Y.L., Huang, C.Y., Sastry, S.: Attacks against process control systems: risk assessment, detection, and response. In: Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security. ASIACCS 2011, pp. 355–366. ACM, New York (2011),
  18. 18.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018).
  19. 19.
    Giraldo, J., et al.: A survey of physics-based attack detection in cyber-physical systems. ACM Comput. Surv. 51(4), 76:1–76:36 (2018). Scholar
  20. 20.
    Goldberg, E., Güdemann, M., Kroening, D., Mukherjee, R.: Efficient verification of multi-property designs (the benefit of wrong assumptions). In: 2018 Design, Automation Test in Europe Conference Exhibition (DATE), pp. 43–48, March 2018Google Scholar
  21. 21.
    Günther, C.G.: An identity-based key-exchange protocol. In: Quisquater, J.-J., Vandewalle, J. (eds.) EUROCRYPT 1989. LNCS, vol. 434, pp. 29–37. Springer, Heidelberg (1990). Scholar
  22. 22.
    Halpern, J.Y.: Actual Causality. MIT Press (2016).
  23. 23.
    Hellerman, L.: A catalog of three-variable or-invert and and-invert logical circuits. IEEE Trans. Electron. Comput. EC 12(3), 198–223 (1963)CrossRefGoogle Scholar
  24. 24.
    Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 298–309. Springer, Heidelberg (2003). Scholar
  25. 25.
    Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(12), 1377–1394 (2002)CrossRefGoogle Scholar
  26. 26.
    McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). Scholar
  27. 27.
    Menezes, A.J., Vanstone, S.A., Oorschot, P.C.V.: Handbook of Applied Cryptography, 1st edn. CRC Press Inc., Boca Raton (1996)zbMATHGoogle Scholar
  28. 28.
    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
  29. 29.
    Rothstein-Morris, E., Sun, J., Chattopadhyay, S.: Systematic Classification of Attackers via Bounded Model Checking (Extended Version). arXiv:1911.05808 (2019).
  30. 30.
    Rothstein, E., Murguia, C.G., Ochoa, M.: Design-time quantification of integrity in cyber-physical systems. In: Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, PLAS 2017, pp. 63–74. ACM, New York (2017).
  31. 31.
    Tseitin, G. S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: 2: Classical Papers on Computational Logic (1967–1970)Google Scholar
  32. 32.
    Urbina, D.I., et al.: Limiting the impact of stealthy attacks on industrial control systems. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. CCS 2016, pp. 1092–1105. ACM, New York (2016),
  33. 33.
    Weerakkody, S., Sinopoli, B., Kar, S., Datta, A.: Information flow for security in control systems. In: 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 5065–5072, December 2016Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  • Eric Rothstein-Morris
    • 1
    Email author
  • Jun Sun
    • 2
  • Sudipta Chattopadhyay
    • 1
  1. 1.Singapore University of Technology and DesignSingaporeSingapore
  2. 2.Singapore Management UniversitySingaporeSingapore

Personalised recommendations