[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Partially-Observable Security Games for Attack-Defence Analysis in Software Systems

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 15280))

Included in the following conference series:

  • 83 Accesses

Abstract

Given the presence of residual vulnerabilities in software systems, it is critical to apply suitable countermeasures in order to minimize the likelihood of an attack. In this paper we propose a formal approach, based on stochastic games, to threat analysis and synthesis of defence strategies for protecting systems with vulnerabilities. Crucially, we support analysis under partial observation, where some of the attacker’s activities are unobservable or undetectable by the defender. We construct a one-sided partially observable security game and transform it into a perfect game, for which formal analysis is feasible. We prove that this transformation is sound for a sub-class of security games and a subset of objectives specified in the temporal logic rPATL. We implement our approach and evaluate it by applying it to a real-life example.

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
£29.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
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 49.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 59.99
Price includes VAT (United Kingdom)
  • 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

Notes

  1. 1.

    https://www.first.org/cvss/.

  2. 2.

    https://www.prismmodelchecker.org/files/sefm24/.

References

  1. Anwar, A.H., Kamhoua, C.A., Leslie, N.O., Kiekintveld, C.: Honeypot allocation for cyber deception under uncertainty. IEEE Trans. Netw. Serv. Manag. 19(3), 3438–3452 (2022)

    Article  Google Scholar 

  2. Aslanyan, Z., Nielson, F., Parker, D.: Quantitative verification and synthesis of attack-defence scenarios. In: Proc. CSF’16, pp. 105–119 (2016)

    Google Scholar 

  3. Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL TIGA user-manual. Aalborg University (2007)

    Google Scholar 

  4. Bistarelli, S., Dall’Aglio, M., Peretti, P.: Strategic games on defense trees. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 1–15. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75227-1_1

    Chapter  Google Scholar 

  5. Bork, A., Junges, S., Katoen, J.-P., Quatmann, T.: Verification of indefinite-horizon POMDPs. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 288–304. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-59152-6_16

    Chapter  Google Scholar 

  6. Bork, A., Katoen, J.-P., Quatmann, T.: Under-approximating expected total rewards in POMDPs. In: TACAS 2022. LNCS, vol. 13244, pp. 22–40. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99527-0_2

    Chapter  Google Scholar 

  7. Carr, S., Jansen, N., Bharadwaj, S., Spaan, M.T., Topcu, U.: Safe policies for factored partially observable stochastic games. Science and System XVII, In Robotics (2021)

    Book  Google Scholar 

  8. Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.: Timed control with observation based and stuttering invariant strategies. In: Proc. ATVA’07, pp. 192–206 (2007)

    Google Scholar 

  9. Chatterjee, K., Chmelik, M., Tracol, M.: What is decidable about partially observable Markov decision processes with omega-regular objectives. In: Proc. CSL’13, pp. 165–180 (2013)

    Google Scholar 

  10. Chatterjee, K., Doyen, L.: Partial-observation stochastic games: How to win when belief fails. ACM Trans. Comput. Log. 15(2), 16:1–16:44 (2014)

    Google Scholar 

  11. Chatterjee, K., Doyen, L., Henzinger, T.A.: A survey of partial-observation stochastic parity games. Formal Methods Syst. Des. 43(2), 268–284 (2013)

    Article  Google Scholar 

  12. Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61–92 (2013)

    Article  Google Scholar 

  13. Chowdhary, A., Sengupta, S., Alshamrani, A., Huang, D., Sabur, A.: Adaptive MTD security using Markov game modeling. In: International Conference on Computing, Networking and Communications, ICNC 2019, Honolulu, HI, USA, February 18-21, 2019, pp. 577–581 (2019)

    Google Scholar 

  14. Durkota, K., Lisý, V., Bosanský, B., Kiekintveld, C.: Optimal network security hardening using attack graph games. In: Proc. IJCAI’15, pp. 526–532 (2015)

    Google Scholar 

  15. Eisentraut, J., Křetínský, J.: Expected cost analysis of attack-defense trees. In: Parker, D., Wolf, V. (eds.) QEST 2019. LNCS, vol. 11785, pp. 203–221. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30281-8_12

    Chapter  Google Scholar 

  16. Gadyatskaya, O., Hansen, R.R., Larsen, K.G.,  Legay, A., Olesen, M.C., Poulsen, D.B.: Modelling attack-defense trees using timed automata. In: Proc. FORMATS’16, pp. 35–50 (2016)

    Google Scholar 

  17. Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589–610 (2022)

    Article  Google Scholar 

  18. Hong, J.B., Kim, D.S., Chung, C.-J., Huang, D.: A survey on the usability and practical applications of graphical security models. Comput. Sci. Rev. 26, 1–16 (2017)

    Article  MathSciNet  Google Scholar 

  19. Hunt, K., Zhuang, J.: A review of attacker-defender games: Current state and paths forward. Eur. J. Oper. Res. 313(2), 401–417 (2024)

    Article  MathSciNet  Google Scholar 

  20. Khakpour, N.,  Parker, D.: Partially-observable security games for attack-defence analysis in software systems. CoRR, abs/2211.01508 (2022)

    Google Scholar 

  21. Khakpour, N., Skandylas, C., Nariman, G.S.,  Weyns, D.: Towards secure architecture-based adaptations. In: Proceedings of the 14th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS@ICSE 2019, Montreal, QC, Canada, May 25-31, 2019, pp. 114–125, 2019

    Google Scholar 

  22. Kordy, B., Piètre-Cambacédès, L., Schweitzer, P.: DAG-based attack and defense modeling: Don’t miss the forest for the attack trees. Comput. Sci. Rev. 13, 03 (2013)

    Google Scholar 

  23. Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475–487. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_25

    Chapter  Google Scholar 

  24. 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). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  25. Manshaei, M.H.,  Zhu, Q.,  Alpcan, T.,  Basar, T.,  Hubaux, J.: Game theory meets network security and privacy. ACM Comput. Surv. 45(3):25:1–25:39 (2013)

    Google Scholar 

  26. Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real-Time Syst. 53(3), 354–402 (2017)

    Article  Google Scholar 

  27. Ou, X.,  Govindavajhala, S., Appel, A.W.: Mulval: A logic-based network security analyzer. In: Proceedings of the 14th Conference on USENIX Security Symposium - Volume 14, SSYM’05, p. 8, Berkeley, CA, USA, 2005. USENIX Association (2005)

    Google Scholar 

  28. Sheyner, O.,  Haines, J., Jha, S.,  Lippmann, R., Wing, J.M.: Automated generation and analysis of attack graphs. In: Proceedings 2002 IEEE Symposium on Security and Privacy, pp. 273–284. IEEE (2002)

    Google Scholar 

  29. Simaitis, A.: Automatic Verification of Competitive Stochastic Systems. PhD thesis, Department of Computer Science, University of Oxford (2014)

    Google Scholar 

  30. Skandylas, C.,  Khakpour, N.,  Cámara, J.: Security countermeasure selection for component-based software-intensive systems. In: 22nd IEEE International Conference on Software Quality, Reliability and Security, QRS 2022, Guangzhou, China, December 5-9, 2022, pp. 63–72. IEEE (2022)

    Google Scholar 

  31. Wang, L.,  Islam, T.,  Long, T.,  Singhal, A.,  Jajodia, S.: An attack graph-based probabilistic security metric. In: Data and Applications Security XXII, 22nd Annual IFIP WG 11.3 Working Conference on Data and Applications Security, London, UK, July 13-16, 2008, Proceedings, pp. 283–296 (2008)

    Google Scholar 

  32. Weiss, J.D.: A system security engineering process. In: Proceedings of the 14th National Computer Security Conference, vol. 249, pp. 572–581 (1991)

    Google Scholar 

  33. Wideł, W.,  Audinot, M.,  Fila, B.,  Pinchinat, S.: Beyond 2014: Formal methods for attack tree–based security modeling. ACM Comput. Surv. 52(4), 75:1–75:36 (2019)

    Google Scholar 

  34. Winterer, L., et al.: Motion planning under partial observability using game-based abstraction. In: 56th IEEE Annual Conference on Decision and Control, CDC 2017, Melbourne, Australia, December 12-15, 2017, pp. 2201–2208 (2017)

    Google Scholar 

Download references

Acknowledgements

This work was funded in part by the Swedish Knowledge Foundation (No. 20160186) and the UK Engineering and Physical Sciences Research Council (EP/X037274/1).

Author information

Authors and Affiliations

  1. Newcastle University, Newcastle, NE1 7RU, UK

    Narges Khakpour

  2. University of Oxford, Oxford, OX1 2JD, UK

    David Parker

Authors
  1. Narges Khakpour
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Parker
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Narges Khakpour .

Editor information

Editors and Affiliations

  1. Campus Gualtar, University of Aveiro, Aveiro, Portugal

    Alexandre Madeira

  2. University of Augsburg, Augsburg, Germany

    Alexander Knapp

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Khakpour, N., Parker, D. (2025). Partially-Observable Security Games for Attack-Defence Analysis in Software Systems. In: Madeira, A., Knapp, A. (eds) Software Engineering and Formal Methods. SEFM 2024. Lecture Notes in Computer Science, vol 15280. Springer, Cham. https://doi.org/10.1007/978-3-031-77382-2_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-77382-2_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-77381-5

  • Online ISBN: 978-3-031-77382-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation