Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Extending Parikh’s Theorem to Weighted and Probabilistic Context-Free Grammars Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage

verfasst von : Marco Baldi, Ezio Bartocci, Franco Chiaraluce, Alessandro Cucchiarelli, Linda Senigagliesi, Luca Spalazzi, Francesco Spegni

Erschienen in: Quantitative Evaluation of Systems

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Recent developments in cloud architectures have originated new models of online storage clouds based on data dispersal algorithms. According to these algorithms the data is divided into several slices that are distributed among remote and independent storage nodes. Ensuring confidentiality in this context is crucial: only legitimate users should access any part of information they distribute among storage nodes.
To the best of our knowledge, the security analysis and assessment of existing solutions always assume homogeneous networks and honest-but-curious nodes as attacker model. We analyze more complex scenarios with heterogeneous network topologies and a passive attacker eavesdropping the channel between user and storage nodes.
We use parameterized Markov Decision Processes to model such a class of systems and Probabilistic Model Checking to assess the likelihood of breaking the confidentiality. Even if, generally speaking, the parameterized model checking is undecidable, in this paper, however, we proved a Small Model Theorem that makes such a problem decidable for the class of models adopted in this work. We discovered that confidentiality is highly affected by parameters such as the number of slices and the number of write and read requests. At design-time, the presented methodology helps to determine the optimal values of parameters affecting the likelihood of a successful attack to confidentiality.

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 A Hybrid Multi-trajectory Simulation Algorithm for the Performance Evaluation of Stochastic Petri Nets
Nächstes Kapitel On the Cost of Diagnosis with Disambiguation
Fußnoten
Literatur
1.
Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 109–124. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-44584-6_​9
2.
Baier, C., Katoen, J.P.: Principles of Model Checking. Springer, Heidelberg (2008)MATH
3.
Baldi, M., Cucchiarelli, A., Senigagliesi, L., Spalazzi, L., Spegni, F.: Parametric and probabilistic model checking of confidentiality in data dispersal algorithms. In: Proceedings of HPCS 2016: International Conference on High Performance Computing and Simulation, pp. 476–483 (2016)
4.
Baldi, M., Maturo, N., Montali, E., Chiaraluce, F.: AONT-LT: a data protection scheme for cloud and cooperative storage systems. In: Proceedings of HPCS 2014: International Conference on High Performance Computing and Simulation, pp. 566–571 (2014)
5.
Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326–340. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-19835-9_​30 CrossRef
6.
Basin, D.A., Cremers, C., Meadows, C.A.: Model checking security protocols. In: Handbook of Model Checking. Springer, Heidelberg (2017)
7.
Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: Proceedings of FSTTCS 2013: The IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 24, pp. 501–513 (2013)
8.
Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability in parameterized verification. SIGACT News 47(2), 53–64 (2016)MathSciNetCrossRef
9.
Bowers, K.D., Juels, A., Oprea, A.: Hail: a high-availability and integrity layer for cloud storage. In: Proceedings of the 16th ACM Conference on Computer and Communications Security, pp. 187–198. ACM (2009)
10.
Chung, J.Y., Joe-Wong, C., Ha, S., Hong, J.W.K., Chiang, M.: Cyrus: towards client-defined cloud storage. In: Proceedings of the 10th European Conference on Computer Systems, p. 17. ACM (2015)
11.
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)CrossRef
12.
13.
14.
Durumeric, Z., Kasten, J., Adrian, D., Halderman, J.A., Bailey, M., Li, F., Weaver, N., Amann, J., Beekman, J., Payer, M., Paxson, V.: The matter of heartbleed. In: Proceedings of the 2014 Internet Measurement Conference, pp. 475–488. ACM (2014)
15.
Escobar, S., Meadows, C.A., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theor. Comput. Sci. 367(1–2), 162–202 (2006)MathSciNetCrossRefMATH
16.
Georgiev, M., Iyengar, S., Jana, S., Anubhai, R., Boneh, D., Shmatikov, V.: The most dangerous code in the world: validating SSL certificates in non-browser software. In: Proceedings of the ACM Conference on Computer and Communications Security, pp. 38–49 (2012)
17.
Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE-2012. LNCS, vol. 7273, pp. 18–34. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-30793-5_​2 CrossRef
18.
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). doi:10.​1007/​978-3-642-22110-1_​47 CrossRef
19.
20.
Lengál, O., Lin, A.W., Majumdar, R., Rümmer, P.: Fair termination for parameterized probabilistic concurrent systems. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 499–517. Springer, Heidelberg (2017). doi:10.​1007/​978-3-662-54577-5_​29 CrossRef
21.
Lenzini, G., Mauw, S., Ouchani, S.: Security analysis of socio-technical physical systems. Comput. Electr. Eng. 47, 258–274 (2015)CrossRef
22.
Li, M., Qin, C., Li, J., Lee, P.P.: CDstore: toward reliable, secure, and cost-efficient cloud storage via convergent dispersal. IEEE Internet Comp. 20(3), 45–53 (2016)CrossRef
23.
24.
Merani, M.L., Barcellona, C., Tinnirello, I.: Multi-cloud privacy preserving schemes for linear data mining. In: Proceedings of ICC 2015: IEEE International Conference on Communications, pp. 7095–7101 (2015)
25.
Ouchani, S., Debbabi, M.: Specification, verification, and quantification of security in model-based systems. Computing 97(7), 691–711 (2015)MathSciNetCrossRef
26.
Pagliarecci, F., Spalazzi, L., Spegni, F.: Model checking grid security. Fut. Gener. Comput. Syst. 29(3), 811–827 (2013)CrossRef
27.
Panti, M., Spalazzi, L., Tacconi, S., Valenti, S.: Automatic verification of security in payment protocols for electronic commerce. In: ICEIS 2002, Proceedings of the 4th International Conference on Enterprise Information Systems, pp. 968–974 (2002)
28.
29.
Resch, J., Plank, J.: AONT-RS: blending security and performance in dispersed storage systems. In: Proceedings 9th FAST Conference (2011)
30.
Seidel, S.Y., Rappaport, T.S.: 914 MHz path loss prediction models for indoor wireless communications in multifloored buildings. IEEE Trans. Microwave Theory Tech. 40(2), 202–217 (1992)CrossRef
31.
32.
Shen, L., Feng, S., Sun, J., Li, Z., Wang, G., Liu, X.: CloudS: a multi-cloud storage system with multi-level security. In: Wang, G., Zomaya, A., Perez, G.M., Li, K. (eds.) ICA3PP 2015. LNCS, vol. 9530, pp. 703–716. Springer, Cham (2015). doi:10.​1007/​978-3-319-27137-8_​51 CrossRef
33.
Shmatikov, V.: Probabilistic analysis of an anonymity system. J. Comput. Secur. 12(3–4), 355–377 (2004)CrossRefMATH
34.
Spalazzi, L., Spegni, F.: Parameterized model-checking of timed systems with conjunctive guards. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 235–251. Springer, Cham (2014). doi:10.​1007/​978-3-319-12154-3_​15
35.
Strunk, A., Mosch, M., Groß, S., Thoß, Y., Schill, A.: Building a flexible service architecture for user controlled hybrid clouds. In: Proceedings of the 2012 Seventh International Conference on Availability, Reliability and Security (ARES), pp. 149–154. IEEE (2012)
36.
Tang, H., Liu, F., Shen, G., Jin, Y., Guo, C.: Unidrive: synergize multiple consumer cloud storage services. In: Proceedings of the 16th Annual Middleware Conference, pp. 137–148. ACM (2015)
37.
Yang, F., Yang, G., Hao, Y.: The modeling library of eavesdropping methods in quantum cryptography protocols by model checking. Int. J. Theor. Phys. 55(7), 3414–3427 (2016)MathSciNetCrossRefMATH
Metadaten
Titel
A Probabilistic Small Model Theorem to Assess Confidentiality of Dispersed Cloud Storage
verfasst von
Marco Baldi
Ezio Bartocci
Franco Chiaraluce
Alessandro Cucchiarelli
Linda Senigagliesi
Luca Spalazzi
Francesco Spegni
Copyright-Jahr
2017
Buch
Quantitative Evaluation of Systems

Print ISBN: 978-3-319-66334-0

Electronic ISBN: 978-3-319-66335-7

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66335-7_8