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:
Buchtitelbild

2017 | OriginalPaper | Buchkapitel

Modular Verification of Information Flow Security in Component-Based Systems

verfasst von : Simon Greiner, Martin Mohr, Bernhard Beckert

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We propose a novel method for the verification of information flow security in component-based systems. The method is (a) modular w.r.t. services and components, i.e., overall security is proved to follow from the security of the individual services provided by the components, and (b) modular w.r.t. attackers, i.e., verified security properties can be re-used to demonstrate security w.r.t. different kinds of attacks.
In a first step, user-provided security specifications for individual services are verified using program analysis techniques. In a second step, first-order formulas are generated expressing that component non-interference follows from service-level properties and in a third step that global system security follows from component non-interference. These first-order proof obligations are discharged with a first-order theorem prover. The overall approach is independent of the programming language used to implement the components. We provide a soundness proof for our method and highlight its advantages, especially in the context of evolving systems.
As a proof of concept and to demonstrate the usability of our method, we present a case study, where we verify the security of a system implemented in Java against two types of attackers. We apply the program verification system KeY and the program analysis tool Joana for analyzing individual services; modularity of our approach allows us to use them in parallel.

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
Fußnoten
1
We omit discussion of high messages here, and refer to [13].
 
Literatur
1.
Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book: From Theory to Practice. Springer, Heidelberg (2016)
2.
Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13–17 July 2015
3.
Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference Java bytecode verifier. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-71316-6_​10CrossRef
4.
Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Information flow in object-oriented software. In: Gupta, G., Peña, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 19–37. Springer, Heidelberg (2013). doi:10.​1007/​978-3-319-14125-1_​2CrossRef
5.
Chong, S., Vikram, K., Myers, A.C., et al.: SIF: Enforcing confidentiality and integrity in web applications. In: USENIX Security, vol. 7 (2007)
6.
Clark, D., Hunt, S.: Non-interference for deterministic interactive programs. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 50–66. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-01465-9_​4CrossRef
7.
Cohen, E.: Information transmission in computational systems. SIGOPS Oper. Syst. Rev. 11, 133–139 (1977)CrossRef
8.
9.
Ereth, S., Mantel, H., Perner, M.: Towards a common specification language for information-flow security in RS3 and beyond: RIFL 1.0 - the language. Technical Report TUD-CS-2014-0115, TU Darmstadt (2014)
10.
Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Security and Privacy (1982)
11.
Graf, J., Hecker, M., Mohr, M.: Using Joana for information flow control in Java programs - a practical guide. In: ATPS, February 2013
12.
Greiner, S., Grahl, D.: Non-interference with what-declassification in component-based systems. In: CSF (2016)
13.
Greiner, S., Mohr, M., Beckert, B.: Modular verification of information flow security in component-based systems - proofs and proof of concept (2017)CrossRef
14.
Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8, 399–422 (2009)CrossRef
15.
16.
Johnson, A., Waye, L., Moore, S., Chong, S.: Exploring and enforcing security guarantees via program dependence graphs. In: PLDI, June 2015
17.
Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006). doi:10.​1007/​11813040_​19CrossRef
18.
Küsters, R., Truderung, T., Beckert, B., Bruns, D., Kirsten, M., Mohr, M.: A hybrid approach for proving noninterference of Java programs. In: CSF, July 2015
19.
Lovat, E., Fromm, A., Mohr, M., Pretschner, A.: SHRIFT system-wide hybrid information flow tracking. In: Federrath, H., Gollmann, D. (eds.) SEC 2015. IAICT, vol. 455, pp. 371–385. Springer, Cham (2015). doi:10.​1007/​978-3-319-18467-8_​25CrossRef
20.
Mantel, H.: Possibilistic definitions of security – an assembly kit. In: CSFW (2000)
21.
Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF (2011)
22.
Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: CSF (2016)
23.
Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1999)
24.
Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: IEEE Security and Privacy, May 2011
25.
O’Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: CSFW, Jul 2006
26.
Rafnsson, W., Hedin, D., Sabelfeld, A.: Securing interactive programs. In: CSF (2012)
27.
Sabelfeld, A., Mantel, H.: Static confidentiality enforcement for distributed programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 376–394. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45789-5_​27CrossRefMATH
28.
Sabelfeld, A., Sands, D.: A PER model of secure information flow in sequential programs. Higher-Order Symbolic Comput. 14, 59–91 (2001)CrossRef
29.
Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17, 517–548 (2009)CrossRef
30.
Scheben, C., Schmitt, P.H.: Verification of information flow properties of Java programs without approximations. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 232–249. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-31762-0_​15CrossRef
31.
Scheben, C., Schmitt, P.H.: Efficient self-composition for weakest precondition calculi. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 579–594. Springer, Cham (2014). doi:10.​1007/​978-3-319-06410-9_​39CrossRef
32.
Sheldon, M.A., Gifford, D.K.: Static dependent types for first class modules. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming. ACM (1990)
33.
34.
Wasserrab, D., Lohner, D.: Proving information flow noninterference by reusing a machine-checked correctness proof for slicing. In: VERIFY (2010)
Metadaten
Titel
Modular Verification of Information Flow Security in Component-Based Systems
verfasst von
Simon Greiner
Martin Mohr
Bernhard Beckert
Copyright-Jahr
2017
Buch
Software Engineering and Formal Methods

Print ISBN: 978-3-319-66196-4

Electronic ISBN: 978-3-319-66197-1

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66197-1_19

Premium Partner

    Bildnachweise