Skip to main content
Erschienen in:
Buchtitelbild

2017 | OriginalPaper | Buchkapitel

Information Flow for Timed Automata

verfasst von : Flemming Nielson, Hanne Riis Nielson, Panagiotis Vasilikos

Erschienen in: Models, Algorithms, Logics and Tools

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

One of the key demands of cyberphysical systems is that they meet their safety goals. Timed Automata has established itself as a formalism for modelling and analysing the real-time safety aspects of cyberphysical systems. Increasingly it is also demanded that cyberphysical systems meet a number of security goals for confidentiality and integrity. Information Flow Control is an approach to ensuring that there are no flows of information that violate the stated security policy.
We develop a language based approach to the modelling and analysis of timed systems that allows to incorporate considerations of information flow control. We define a type system for information flow that takes account of the non-determinism and clocks of timed systems. The adequacy of the type system is ensured by means of a non-interference result.

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
1.
Zurück zum Zitat Aceto, L., Ingolfsdottir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)CrossRefMATH Aceto, L., Ingolfsdottir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)CrossRefMATH
2.
Zurück zum Zitat Agat, J.: Transforming out timing leaks. In: Proceedings of the POPL, pp. 40–53 (2000) Agat, J.: Transforming out timing leaks. In: Proceedings of the POPL, pp. 40–53 (2000)
4.
Zurück zum Zitat Apt, K.R.: Ten years of Hoare’s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)CrossRefMATH Apt, K.R.: Ten years of Hoare’s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)CrossRefMATH
5.
Zurück zum Zitat Banâtre, J.-P., Bryce, C., Métayer, D.: Compile-time detection of information flow in sequential programs. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 55–73. Springer, Heidelberg (1994). doi:10.1007/3-540-58618-0_56 Banâtre, J.-P., Bryce, C., Métayer, D.: Compile-time detection of information flow in sequential programs. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 55–73. Springer, Heidelberg (1994). doi:10.​1007/​3-540-58618-0_​56
6.
Zurück zum Zitat Barbuti, R., De Francesco, N., Santone, A., Tesei, L.: A notion of non-interference for timed automata. Fundam. Inform. 51(1–2), 1–11 (2002)MathSciNetMATH Barbuti, R., De Francesco, N., Santone, A., Tesei, L.: A notion of non-interference for timed automata. Fundam. Inform. 51(1–2), 1–11 (2002)MathSciNetMATH
7.
Zurück zum Zitat Barbuti, R., Tesei, L.: A decidable notion of timed non-interference. Fundam. Inform. 54(2–3), 137–150 (2003)MathSciNetMATH Barbuti, R., Tesei, L.: A decidable notion of timed non-interference. Fundam. Inform. 54(2–3), 137–150 (2003)MathSciNetMATH
8.
Zurück zum Zitat Bordbar, B., Okano, K.: Testing deadlock-freeness in real-time systems: a formal approach. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 95–109. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31848-4_7 CrossRef Bordbar, B., Okano, K.: Testing deadlock-freeness in real-time systems: a formal approach. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 95–109. Springer, Heidelberg (2005). doi:10.​1007/​978-3-540-31848-4_​7 CrossRef
9.
Zurück zum Zitat Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)CrossRefMATH Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)CrossRefMATH
10.
11.
Zurück zum Zitat Focardi, R., Gorrieri, R., Martinelli, F.: Real-time information flow analysis. IEEE J. Sel. Areas Commun. 21(1), 20–35 (2003)CrossRef Focardi, R., Gorrieri, R., Martinelli, F.: Real-time information flow analysis. IEEE J. Sel. Areas Commun. 21(1), 20–35 (2003)CrossRef
12.
Zurück zum Zitat Gardey, G., Mullins, J., Roux, O.H.: Non-interference control synthesis for security timed automata. Electr. Notes Theor. Comput. Sci. 180(1), 35–53 (2007)CrossRefMATH Gardey, G., Mullins, J., Roux, O.H.: Non-interference control synthesis for security timed automata. Electr. Notes Theor. Comput. Sci. 180(1), 35–53 (2007)CrossRefMATH
13.
Zurück zum Zitat Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Time and probability-based information flow analysis. IEEE Trans. Softw. Eng. 36(5), 719–734 (2010)CrossRefMATH Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Time and probability-based information flow analysis. IEEE Trans. Softw. Eng. 36(5), 719–734 (2010)CrossRefMATH
14.
Zurück zum Zitat Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: ACM Symposium on Operating System Principles, SOSP 1997, pp. 129–142. ACM (1997) Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: ACM Symposium on Operating System Principles, SOSP 1997, pp. 129–142. ACM (1997)
15.
Zurück zum Zitat Hanne Riis Nielson and Flemming Nielson: Content dependent information flow control. J. Log. Algebr. Meth. Program. 87, 6–32 (2017)MathSciNetCrossRefMATH Hanne Riis Nielson and Flemming Nielson: Content dependent information flow control. J. Log. Algebr. Meth. Program. 87, 6–32 (2017)MathSciNetCrossRefMATH
17.
Zurück zum Zitat Volpano, D.M., Smith, G., Irvine, C.E.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)CrossRef Volpano, D.M., Smith, G., Irvine, C.E.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)CrossRef
18.
Zurück zum Zitat Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of the CSFW, pp. 29–43 (2003) Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of the CSFW, pp. 29–43 (2003)
Metadaten
Titel
Information Flow for Timed Automata
verfasst von
Flemming Nielson
Hanne Riis Nielson
Panagiotis Vasilikos
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-63121-9_1