Concrete and Abstract Semantics to Check Secure Information Flow in Concurrent Programs

• Autorzy: Bernardeschi C. , De Francesco N. , Lettieri G.
• Języki publikacji: EN

Abstrakty

EN

This paper presents a technique for verifying secure information flow in concurrent programs consisting of a number of independently executing sequential processes with private memory. Communications between processes are synchronous. Moreover, processes are open systems that can accept inputs from the environment and produce outputs towards the environment. The technique is based on an abstract interpretation. First we define a concrete instrumented semantics where each value is annotated with the security level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level.

Słowa kluczowe

EN

language; security model; concrete semantics; abstract semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 60, nr 1-4
• Strony: 81--98
• Opis fizyczny: Bibliogr. 22 poz., tab.

Twórcy

autor

Bernardeschi C.

• Dipartimento di Ingegneria della Informazione, Universita di Pisa, Italy

autor

De Francesco N.

• Dipartimento di Ingegneria della Informazione, Universita di Pisa, Italy

autor

Lettieri G.

• Dipartimento di Ingegneria della Informazione, Universita di Pisa, Italy

Bibliografia

• [1] M. Abadi, A. Banerjee. N. Heintze, J.G. Riecke. A Core Calculus of dependency. Proceedings 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Conference, San Antonio. Texas, USA, 1999. pp. 147-160.
• [2] G. R. Andrews, R. P. Reitman. An axiomatic approach to information flow in programs. ACM Transactions on programming languages and systems, 2(1), 1980, pp. 56-76.
• [3] J. Banatre, C. Bryce, D. L. Metayer. Compile-time detection of information flow in sequential programs. Proceedings European Symposium on Research in Computer Security, LNCS 875. Springer Verlag, 1994, pp. 55-73.
• [4] R. Barbuti. C. Bemardeschi, N. De Francesco. Abstract Interpretation of Operational Semantics for Secure Information Flow. Information Processing Letters, 2002.
• [5] Bell, D.E. and La Padula, L.J. (1973) Secure computer systems: mathematical foundations and model. Technical Report M74-244. MITRE Corporation, Bedford, Massachusetts.
• [6] Z. Chen. B. Xu. J. Zhao An overview of Methods for Dependence Analysis of Concurrent Programs. ACM SIGPLAN Notices, 37(8), 2002.
• [7] P. Cousot, R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation. 2, pp. 511-547, 1992.
• [8] N. De Francesco, A. Santone. Checking Secure Information Flow in Concurrent languages by Abstract Interpretation plus Model Checking. Concurrency Specification & Programming, vol. 1. 105-116, Berlino 2002.
• [9] De Francesco, A. Santone, L. Tesei Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems. Fundamenta Informaticae, Vol. 54, Number 2-3, February 2003.
• [10] D. E. Denning, P. J. Denning. Certification of programs for secure information How. Communications of the ACM. 20(7). 1977, pp. 504-513.
• [11] Goguen. J. and Meseguer. J. (1982) Security policies and security models. Proceedings of 1982 EEE Symposium on Security' and Privacy, pp. 11 -20.
• [12] N. Heintze, J.G. Riecke. The Slam Calculus: programming with Secrecy and Integrity. Proceedings 25th ACM Principles of Programming Languages Conference. San Diego, USA, 1998, pp. 365-377.
• [13] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ. 1985.
• [14] N. D. Jones, F. Nielson. Abstract interpretation: a semantic based tool for program analysis, in S. Abramsky, D.M. Gabbay. T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science. Vol. 4. Oxford University Press, Oxford. 1995, 527-636.
• [15] K.R.M. Leino, R. Joshi A semantic approach to secure information flow. Science of Computer Programming, 37(1), 2000.
• [16] M. Mizuno, D. A. Schmidt. A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects of Computing 4, 1992, pp. 727-754.
• [17] A. Sabelfeld, A. C. Myers Language-Based Information-Flow Security IEEE Journal on Selected Areas in Communications, Vol. 21, No. 1, January 2003.
• [18] A. Sabelfeld, D. Sands. A PER model of secure information flow in sequential programs. Proceedings 8th European Symposium on Programming, ESOP'99, LNCS 1576, Springer-Verlag, 1999. pp. 40-58.
• [19] A. Sabelfeld, D. Sands. The impact of synchronization on secure information flow in concurrent programs. Proceedings Andrei Ershov 4th International Conference on Perspective of System Informatics. Novosibirsk, LNCS, Springer-Verlag, July 2001.
• [20] G. Smith. A New Type System for Secure Information Flow. Proc. 14th IEEE Computer Security Foundations Workshop (CSFW'01), pp. 115-125, Cape Breton. Nova Scotia, June 2001.
• [21] G. Smith, D. Volpano. Secure information flow in a multi-threaded imperative language. Proceedings 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages, San Diego California, 1998, pp. 1-10.
• [22] D. Volpano, G. Smith, C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3), 1996, pp. 167-187.