Skip to main content

2017 | OriginalPaper | Buchkapitel

Taming Message-Passing Communication in Compositional Reasoning About Confidentiality

verfasst von : Ximeng Li, Heiko Mantel, Markus Tasch

Erschienen in: Programming Languages and Systems

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

We propose a solution for verifying the information-flow security of distributed programs in a compositional manner. Our focus is on the treatment of message passing in such a verification, and our goal is to boost the precision of modular reasoning using rely-guarantee-style reasoning. Enabling a more precise treatment of message passing required the identification of novel concepts that capture assumptions about how a process’s environment interacts. Our technical contributions include a process-local security condition that allows one to exploit such assumptions when analyzing individual processes, a security type system that is sensitive in the content as well as in the availability of messages, and a soundness proof for our security type system. Our results complement existing solutions for rely-guarantee-style reasoning about information-flow security that focused on multi-threading and shared memory.

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!

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!

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!

Literatur
2.
Zurück zum Zitat Amtoft, T., Hatcliff, J., Rodríguez, E., Robby, H.J., Greve, D.: Specification and checking of software contracts for conditional information flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 229–245. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0 CrossRef Amtoft, T., Hatcliff, J., Rodríguez, E., Robby, H.J., Greve, D.: Specification and checking of software contracts for conditional information flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 229–245. Springer, Heidelberg (2008). https://​doi.​org/​10.​1007/​978-3-540-68237-0 CrossRef
3.
Zurück zum Zitat Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: CSF 2015, pp. 137–151 (2015) Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: CSF 2015, pp. 137–151 (2015)
4.
Zurück zum Zitat Askarov, A., Sabelfeld, A.: Gradual release: unifying declassification, encryption and key release policies. In: S&P 2007, pp. 207–221 (2007) Askarov, A., Sabelfeld, A.: Gradual release: unifying declassification, encryption and key release policies. In: S&P 2007, pp. 207–221 (2007)
6.
Zurück zum Zitat Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)CrossRef Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)CrossRef
7.
Zurück zum Zitat Focardi, R., Centenaro, M.: Information flow security of multi-threaded distributed programs. In: PLAS 2008, pp. 113–124 (2008) Focardi, R., Centenaro, M.: Information flow security of multi-threaded distributed programs. In: PLAS 2008, pp. 113–124 (2008)
9.
Zurück zum Zitat Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P 1982. IEEE Computer Society (1982) Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P 1982. IEEE Computer Society (1982)
10.
Zurück zum Zitat Greiner, S., Grahl, D.: Non-interference with what-declassification in component-based systems. In: CSF 2016, pp. 253–267 (2016) Greiner, S., Grahl, D.: Non-interference with what-declassification in component-based systems. In: CSF 2016, pp. 253–267 (2016)
12.
Zurück zum Zitat Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, pp. 79–90 (2006) Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, pp. 79–90 (2006)
13.
Zurück zum Zitat Jones, C.B.: Development methods for computer programs including a notion of interference. Oxford University Computing Laboratory (1981) Jones, C.B.: Development methods for computer programs including a notion of interference. Oxford University Computing Laboratory (1981)
14.
Zurück zum Zitat Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Inf. 42(4–5), 291–347 (2005)CrossRefMATH Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Inf. 42(4–5), 291–347 (2005)CrossRefMATH
17.
Zurück zum Zitat Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn, pp. 605–607. Springer, New York (2011) Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn, pp. 605–607. Springer, New York (2011)
18.
Zurück zum Zitat Mantel, H., Müller-Olm, M., Perner, M., Wenner, A.: Using dynamic pushdown networks to automate a modular information-flow analysis. In: LOPSTR 2015 (2015) Mantel, H., Müller-Olm, M., Perner, M., Wenner, A.: Using dynamic pushdown networks to automate a modular information-flow analysis. In: LOPSTR 2015 (2015)
19.
Zurück zum Zitat Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF 2011, pp. 218–232 (2011) Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF 2011, pp. 218–232 (2011)
21.
Zurück zum Zitat McCullough, D.: A hookup theorem for multilevel security. IEEE Trans. Softw. Eng. 16(6), 563–568 (1990)CrossRef McCullough, D.: A hookup theorem for multilevel security. IEEE Trans. Softw. Eng. 16(6), 563–568 (1990)CrossRef
22.
Zurück zum Zitat Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: CSF 2016 (2016) Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: CSF 2016 (2016)
23.
Zurück zum Zitat Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: SOSP 1997, pp. 129–142 (1997) Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: SOSP 1997, pp. 129–142 (1997)
24.
Zurück zum Zitat Rafnsson, W., Hedin, D., Sabelfeld, A.: Securing interactive programs. In: CSF 2012, pp. 293–307 (2012) Rafnsson, W., Hedin, D., Sabelfeld, A.: Securing interactive programs. In: CSF 2012, pp. 293–307 (2012)
25.
Zurück zum Zitat Sabelfeld, A., Mantel, H.: Securing communication in a concurrent language. In: SAS 2002, pp. 376–394 (2002) Sabelfeld, A., Mantel, H.: Securing communication in a concurrent language. In: SAS 2002, pp. 376–394 (2002)
26.
Zurück zum Zitat Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)CrossRef Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)CrossRef
27.
Zurück zum Zitat Tanenbaum, A.S., van Steen, M.: Distributed Systems - Principles and Paradigms, 2nd edn. Prentice-Hall Inc., Upper Saddle River (2007)MATH Tanenbaum, A.S., van Steen, M.: Distributed Systems - Principles and Paradigms, 2nd edn. Prentice-Hall Inc., Upper Saddle River (2007)MATH
28.
Zurück zum Zitat Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)CrossRef Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)CrossRef
29.
Zurück zum Zitat Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW 2003, pp. 29–43 (2003) Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW 2003, pp. 29–43 (2003)
30.
Zurück zum Zitat Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Sec. 6(2–3), 67–84 (2007)CrossRef Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Sec. 6(2–3), 67–84 (2007)CrossRef
Metadaten
Titel
Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
verfasst von
Ximeng Li
Heiko Mantel
Markus Tasch
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-71237-6_3