Abstract
In this paper, we focus on the synthesis of secure timed systems which are given by timed automata. The security property that the system must satisfy is a non-interference property. Various notions of non-interference have been defined in the literature, and in this paper we focus on Strong Non-deterministic Non-Interference (SNNI) and we study the two following problems: (1) check whether it is possible to enforce a system to be SNNI; if yes (2) compute a sub-system which is SNNI.
Work supported by the French Government under grant ANR-SETI-003.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Focardi, R., Gorrieri, R.: Classification of security properties. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Focardi, R., Gorrieri, R.: The compositional security checker: A tool for the verification of information flow security properties. IEEE Trans. Softw. Eng. 23(9), 550–571 (1997)
Focardi, R., Ghelli, A., Gorrieri, R.: Using non interference for the analysis of security protocols. In: Proceedings of DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)
van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. Elec. Notes in Theo. Comp. Science 168(1), 61–75 (2006); Proceedings of the Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) (2006)
D’Souza, D., Raghavendra, K.R., Sprick, B.: An automata based approach for verifying information flow properties. Elec. Notes in Theo. Comp. Science 135, 39–58 (2005)l; Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysison (ARSPA 2005) (2005)
Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1) (2003)
Gardey, G., Mullins, J., Roux, O.H.: Non-interference control synthesis for security timed automata. Elec. Notes in Theo. Comp. Science 180(1), 35–53 (2005); Proceedings of the 3rd International Workshop on Security Issues in Concurrency (SecCo 2005) (2005)
Cassez, F., Mullins, J., Roux, O.H.: Synthesis of non-interferent systems. In: Proceedings of the 4th Int. Conf. on Mathematical Methods, Models and Architectures for Computer Network Security (MMM-ACNS 2007). Communications in Computer and Inform. Science, vol. 1, pp. 307–321. Springer, Heidelberg (2007)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Finkel, O.: On decision problems for timed automata. Bulletin of the European Association for Theoretical Computer Science 87, 185–190 (2005)
Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)
D’Souza, D., Madhusudan, P.: Timed control synthesis for external specifications. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 571–582. Springer, Heidelberg (2002)
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: STOC, pp. 1–9. ACM, New York (1973)
Henzinger, T., Kopke, P.: Discrete-time control for rectangular hybrid automata. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 582–593. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benattar, G., Cassez, F., Lime, D., Roux, O.H. (2009). Synthesis of Non-Interferent Timed Systems . In: Ouaknine, J., Vaandrager, F.W. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2009. Lecture Notes in Computer Science, vol 5813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04368-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-04368-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04367-3
Online ISBN: 978-3-642-04368-0
eBook Packages: Computer ScienceComputer Science (R0)