Czasopismo
2003
|
Vol. 54, nr 2,3
|
137-150
Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Warianty tytułu
Języki publikacji
Abstrakty
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
Czasopismo
Rocznik
Tom
Strony
137-150
Opis fizyczny
bibliogr. 20 poz.
Twórcy
autor
autor
- Dipartimento di Informatica, Universita di Pisa, Via F. Buonarroti, 2, 56127 Pisa, Italy, {barbuti,tesei}@di.unipi.it
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.
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS2-0004-0085