Abstract
We investigate a timed non-interference property for security systems modeled as timed automata, in which a low-security level user should not be able to deduce the occurrence of some high-security level actions. We assume an attack model in which the malicious (low-level) user has the ability to partially observe and memorize the set of runs of the timed automaton modeling the system.
We first formalize a non-interference property that ensures the system security under such an attack model and we then prove the undecidability of that property when the attacker can have an arbitrarily big memory, i.e., when they are able to memorize sequences of previous observations, with time-stamps, of any length. We next assume bounded memory for the attacker and show that the property can then be decided in PSPACE for a subclass of timed automata ensuring finite duration between distinct observations.
This work has been partially funded by ANR project ProMiS ANR-19-CE25-0015.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Regions without c-approximation, i.e. each point represent a reachable state of location \( \ell _{(A,B)}\) associated with given values of \(x_{new}\) and \(x_{old}\)
- 2.
On this figure, regions are represented according to the original definition proposed by Alur & Dill ( [AD94]), that is with c-approximation, c being the largest synthaxic value used to define the automaton)
- 3.
We also say the automaton is FDO w.r.t. \(\mathcal {O}\).
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Ammar, I., El Touati, Y., Yeddes, M., Mullins, J.: Bounded opacity for timed systems. J. Inf. Secur. Appl. 61, 102926 (2021)
André, É., Kryukov, A.: Parametric non-interference in timed automata. In: Proceedings of the 2020 25th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 37–42. IEEE (2020)
André, É., Lime, D., Marinho, D., Sun, J.: Guaranteeing timed opacity using parametric timed model checking. ACM Trans. Softw. Eng. Methodol. 31(4), 1–36 (2022)
Arnold, A.: Finite Transition Systems. Prentice Hall (1994)
Bortz, A., Boneh, D.: Exposing private information by timing web applications. In: Proceedings of the 16th International Conference on World Wide Web, pp. 621–628 (2007)
Benattar, G., Cassez, F., Lime, D., Roux, O.H.: Control and synthesis of non-interferent timed systems. Int. J. Control 88(2), 217–236 (2015)
Bryans, J., Koutny, M., Mazare, L., Ryan, Peter, Y.A.: Opacity generalised to transition systems. Int. J. Inf. Secur. 7(6), 421–435 (2008)
Barbuti, R., Tesei, L.: A decidable notion of timed non-interference. Fundam. Inform. 54(2–3), 137–150 (2003)
Felten, E.W., Schneider, M.A.: Timing attacks on web privacy. In: Proceedings of the 7th ACM Conference on Computer and Communications Security, CCS 2000, pp. 25–32. Association for Computing Machinery, New York (2000)
Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proceedings of the 1984 IEEE Symposium on Security and Privacy, pp. 75–75. IEEE (1984)
Gardey, G., Mullins, J., Roux, O.H.: Non-interference control synthesis for security timed automata. Electron. Notes Theor. Comput. Sci. 180(1), 35–53 (2007)
Gerking, C., Schubert, D., Bodden, E.: Model checking the information flow security of real-time systems. In: Payer, M., Rashid, A., Such, J.M. (eds.) ESSoS 2018. LNCS, vol. 10953, pp. 27–43. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94496-8_3
Kocher, PC.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104–113. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-68697-5_9
Kotcher, R., Pei, Y., Jumde, P., Jackson, C.: Cross-origin pixel stealing: timing attacks using CSS filters. In: Proceedings of the 2013 ACM SIGSAC conference on Computer & Communications Security, pp. 1055–1062 (2013)
Wang, L., Zhan, N.: Decidability of the initial-state opacity of real-time automata. In: Jones, C., Wang, J., Zhan, N. (eds.) Symposium on Real-Time and Hybrid Systems. LNCS, vol. 11180, pp. 44–60. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01461-2_3
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Spriet, A., Lime, D., Roux, O.H. (2023). Timed Non-interference Under Partial Observability and Bounded Memory. In: Petrucci, L., Sproston, J. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2023. Lecture Notes in Computer Science, vol 14138. Springer, Cham. https://doi.org/10.1007/978-3-031-42626-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-031-42626-1_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-42625-4
Online ISBN: 978-3-031-42626-1
eBook Packages: Computer ScienceComputer Science (R0)