A Decidable Notion of Timed Non-Interference

• Autorzy: Barbuti R. , Tesei L.
• Języki publikacji: EN

Abstrakty

EN

We present a notion of non-interference which embodies the notion of time. It is useful to verify the strength of a system against attacks depending on the frequency of certain actions. In particular we give a decidable definition of non-interference which can be checked by using existing verification tools. We show an application example of our notion of non-interference by defining a variant of the classical Fischer's mutual exclusion protocol and by analyzing its strength against attacks.

Słowa kluczowe

EN

Timed Automata; timed non-interference

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 54, nr 2,3
• Strony: 137--150
• Opis fizyczny: bibliogr. 20 poz.

Twórcy

autor

Barbuti R.

autor

Tesei L.

• Dipartimento di Informatica, Universita di Pisa, Via F. Buonarroti, 2, 56127 Pisa, Italy,

Bibliografia

• [1] Aceto, L., Bouyer, P., Burgue˜no, A. and Guldstrand Larsen, K. (1998) The Power of Reachability Testing for Timed Automata. In Proceedings of Foundations Software Technology and Theoretical Computer Science, Springer LNCS 1530, 245-256.
• [2] Aceto, L., Burgue˜no, A. and Guldstrand Larsen, K. (1998) Model Checking via Reachability Testing for Timed Automata. In Proceedings of TACAS’98, Springer LNCS 1384, 263-280.
• [3] Alur, R., Courcoubetis, C. and Dill, D.L. (1993) Model-Checking in Dense Real-time. Information and Computation, 104, 2-34.
• [4] Alur, R. and Dill, D.L. (1994) A Theory of Timed Automata. Theoretical Computer Science, 126, 183-235.
• [5] Alur, R. and Henzinger, T.A. (1994) A Really Temporal Logic. Journal of ACM, 41, 181-204.
• [6] Abdulla, P.A. and Jonsson, B. (1998) Networks of timed processes. In Proceedings of TACAS’98, Springer LNCS 1384, 298-312.
• [7] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J. and Yovine, S. (1995) The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science, 138, 3-34.
• [8] Barbuti, R., De Francesco, N., Santone, A. and Tesei, L. A Notion of non-Interference for Timed Automata (2001) In Proceedings of Concurrency, Specification and Programming Workshop (CS&P’2001), (L. Czaja ed.), Warsaw, Poland, October 2001.
• [9] Dhem, J-F., Koeune, F., Leroux, P-A., Mestr, P., Quisquater, J-J. and Willems, J-L. (2000) A Practical Implementation of the Timing Attack. In Proceedings of CARDIS 1998, Springer LNCS 1820, 167-182.
• [10] Focardi, R. and Gorrieri, R. (1996) Automatic Compositional Verification of Some Security Properties. In Proceedings of TACAS’96, Springer LNCS 1055, 167-186.
• [11] Focardi, R. and Gorrieri, R. (1997) The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties. IEEE Transactions on Software Engineering, 23(9), 550-571.
• [12] Focardi, R., Gorrieri, R. and Martinelli, F. (2000) Information Flow in a Discrete Time Process Algebra. In Proceedings of 13th IEEE Computer Security Foundations Workshop (CSFW’00), (P. Syverson ed.), IEEE press, Cambridge, England, July 2000.
• [13] Henzinger, T.A. and Kopke, P.W. (1994) Verification Methods for the Divergent Runs of Clock Systems. In Proceedings of Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer LNCS 863, 351-372.
• [14] Henzinger, T.A., Nicollin, X., Sifakis, J. and Yovine, S. (1994) Symbolic Model Checking for Real-Time Systems. Information and Computation, 111, 193-244.
• [15] Kocher, P.C. (1996) Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In proceedings of CRYPTO 1996, Springer LNCS 1109, 104-113.
• [16] Lamport, L. (1987) A Fast Mutual Exclusion Algorithm. ACM TOPLAS, 5, 1-11.
• [17] P. Y. A. Ryan, S. A. Schneider. (2001) Process Algebra and Non-Interference. Journal of Computer Security, 9(1/2), 75-103.
• [18] A.W. Roscoe, J.C.P. Woodcock, L. Wulf. (1996) Non-Interference Through Determinism. Journal of Computer Security, 4(1).
• [19] Schindler, W. (2000) A Timing Attack against RSA with the Chinese Remainder Theorem. In Proceedings of CHES 2000, Springer LNCS 1965, 109-124.
• [20] Yovine, S. (1996) Model Checking Timed Automata. Lectures on Embedded Systems, Springer LNCS 1494, 114-152.