nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Secure Information Flow Analysis Using the PRISM Model Checker

verfasst von : Ali A. Noroozi, Khayyam Salehi, Jaber Karimpour, Ayaz Isazadeh

Erschienen in: Information Systems Security

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Secure information flow checks whether sensitive information leak to public outputs of a program or not. It has been widely used to analyze the security of various programs and protocols and guarantee their confidentiality and robustness.

In this paper, the problem of verifying secure information flow of concurrent probabilistic programs is discussed. Programs are modeled by Markovian processes and secure information flow is specified by observational determinism. Then, two algorithms are proposed to verify observational determinism in the Markovian model. The algorithms employ a trace-based approach to traverse the model and check for satisfiability of observational determinism. The proposed algorithms have been implemented into a tool called PRISM-Leak, which is constructed on the PRISM model checker. An anonymity protocol, the dining cryptographers, is discussed as a case study to show how PRISM-Leak can be used to evaluate the security of programs. The scalability of the tool is demonstrated by comparing it to the state-of-the-art information flow tools.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel An Introduction to the CellTree Paradigm (Invited Paper)

Nächstes Kapitel Selective End-To-End Data-Sharing in the Cloud

Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE Workshop on Computer Security Foundations, CSFW 2004, pp. 100–114. IEEE Computer Society (2004)

Biondi, F., Enescu, M.A., Heuser, A., Legay, A., Meel, K.S., Quilbeuf, J.: Scalable approximation of quantitative information flow in programs. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 71–93. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73721-8_4CrossRef

Biondi, F., Kawamoto, Y., Legay, A., Traonouez, L.-M.: HyLeak: hybrid analysis tool for information leakage. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 156–163. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_11CrossRef

Biondi, F., Legay, A., Quilbeuf, J.: Comparative analysis of leakage tools on scalable case studies. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 263–281. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23404-5_17CrossRef

Bischof, S., Breitner, J., Graf, J., Hecker, M., Mohr, M., Snelting, G.: Low-deterministic security for low-nondeterministic programs. J. Comput. Secur. 3, 335–366 (2018)CrossRef

Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptol. 1(1), 65–75 (1988)MathSciNetCrossRef

Chothia, T., Kawamoto, Y., Novakovic, C.: LeakWatch: estimating information leakage from Java programs. In: Kutyłowski, M., Vaidya, J. (eds.) ESORICS 2014. LNCS, vol. 8713, pp. 219–236. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11212-1_13CrossRef

Dabaghchian, M., Abdollahi Azgomi, M.: Model checking the observational determinism security property using promela and spin. Form. Asp. Comput. 27(5–6), 789–804 (2015)MathSciNetCrossRef

10.

Giffhorn, D., Snelting, G.: A new algorithm for low-deterministic security. Int. J. Inf. Secur. 14(3), 263–287 (2015)CrossRef

11.

Graf, J., Hecker, M., Mohr, M., Snelting, G.: Tool demonstration: JOANA. In: Piessens, F., Viganò, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 89–93. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49635-0_5CrossRef

12.

Huisman, M., Blondeel, H.-C.: Model-checking secure information flow for multi-threaded programs. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 148–165. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27375-9_9CrossRef

13.

Huisman, M., Ngo, T.M.: Scheduler-specific confidentiality for multi-threaded programs and its logic-based verification. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 178–195. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31762-0_12CrossRef

14.

Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Proceedings of the 19th IEEE Workshop on Computer Security Foundations, CSFW 2006. IEEE Computer Society (2006)

15.

Karimpour, J., Isazadeh, A., Noroozi, A.A.: Verifying observational determinism. In: Federrath, H., Gollmann, D. (eds.) 30th IFIP International Information Security Conference (SEC). ICT Systems Security and Privacy Protection, Hamburg, Germany, Part 1: Privacy, vol. AICT-455, pp. 82–93, May 2015CrossRef

16.

Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72522-0_6CrossRef

17.

McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37–57 (1992)CrossRef

18.

Ngo, T.M.: Qualitative and quantitative information flow analysis for multi-thread programs. Ph.D. thesis, University of Twente (2014)

19.

Minh Ngo, T., Stoelinga, M., Huisman, M.: Confidentiality for probabilistic multi-threaded programs and its verification. In: Jürjens, J., Livshits, B., Scandariato, R. (eds.) ESSoS 2013. LNCS, vol. 7781, pp. 107–122. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36563-8_8CrossRef

20.

Ngo, T.M., Stoelinga, M., Huisman, M.: Effective verification of confidentiality for multi-threaded programs. J. Comput. Secur. 22(2), 269–300 (2014)CrossRef

21.

Noroozi, A.A., Karimpour, J., Isazadeh, A.: Bisimulation for secure information flow analysis of multi-threaded programs. Math. Comput. Appl. 24(2), 64 (2019). https://doi.org/10.3390/mca24020064MathSciNetCrossRef

22.

Noroozi, A.A., Karimpour, J., Isazadeh, A.: Information leakage of multi-threaded programs. Comput. Electr. Eng. 78, 400–419 (2019). https://doi.org/10.1016/j.compeleceng.2019.07.018. http://www.sciencedirect.com/science/article/pii/S0045790618331549CrossRef

23.

Noroozi, A.A., Karimpour, J., Isazadeh, A., Lotfi, S.: Verifying weak probabilistic noninterference. Int. J. Adv. Comput. Sci. Appl. 8(10) (2017). https://doi.org/10.14569/IJACSA.2017.081026

24.

Noroozi, A.A., Salehi, K., Karimpour, J., Isazadeh, A.: Prism-leak - a tool for computing information leakage of concurrent probabilistic programs (2018). https://github.com/alianoroozi/PRISM-Leak

25.

Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham (2002)

26.

Roscoe, A.W.: CSP and determinism in security modelling. In: IEEE Symposium on Security and Privacy, pp. 114–127. IEEE Computer Society (1995)

27.

Russo, A., Hughes, J., Naumann, D., Sabelfeld, A.: Closing internal timing channels by transformation. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 120–135. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77505-8_10CrossRef

28.

Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)CrossRef

29.

Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proceedings 13th IEEE Computer Security Foundations Workshop, CSFW-13, pp. 200–214, July 2000

30.

Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: Proceedings of the 16th IEEE Workshop on Computer Security Foundations, CSFW 2003, pp. 3–13. IEEE Computer Society (2003)

31.

Terauchi, T.: A type system for observational determinism. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, pp. 287–300. IEEE Computer Society (2008)

32.

Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: 2003 Proceedings of the 16th IEEE Computer Security Foundations Workshop, pp. 29–43, June 2003. https://doi.org/10.1109/CSFW.2003.1212703

Titel: Secure Information Flow Analysis Using the PRISM Model Checker
verfasst von: Ali A. Noroozi
Khayyam Salehi
Jaber Karimpour
Ayaz Isazadeh
Verlag: Springer International Publishing
Buch: Information Systems Security
Print ISBN: 978-3-030-36944-6

Electronic ISBN: 978-3-030-36945-3

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-36945-3_9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner