Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems

• Autorzy: De Francesco N. , Santone A. , Tesei L.
• Języki publikacji: EN

Abstrakty

EN

We propose a method to check secure information flow in concurrent programs with synchronization. The method is based on the combination of abstract interpretation and model checking: by abstract interpretation we build a finite representation (transition system) of the behavior of the program. Then we model check the the abstract transition system with respect to the security properties, expressed by a set of temporal logic formulae. The approach allows certifying more programs than previous methods do. The main point is that we are able to check more carefully the scope of indirect information flows.

Słowa kluczowe

EN

model checking; abstract interpretation

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

Twórcy

autor

De Francesco N.

autor

Santone A.

autor

Tesei L.

• RCOST-Research Centre on Software technology, University of Sannio, Benevento, 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. M´etayer. 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, N. De Francesco, A. Santone, G. Vaglini. Selective mu-calculus and Formula-Based Equivalence of Transition Systems. Journal of Computer and System Sciences, 59(3), 1999. pp. 537-556.
• [5] R. Barbuti, C. Bernardeschi, N. De Francesco. Abstract Interpretation of Operational Semantics for Secure Information Flow. Information Processing Letters, 2002.
• [6] T. Bolognesi, E. Brinksma. Introduction to ISO Specification Language LOTOS. Comp. Networks and ISDN Systems, 14, 1987. 25-59.
• [7] R. Cleaveland, S. Sims. The NCSU Concurrency Workbench. In Proceedings of the Eighth International Conference on Computer-Aided Verification (CAV’96), Lecture Notes in Computer Science 1102, 1996. 394-397.
• [8] The Concurrency Workbench of North Carolina home page. URL http://www4.ncsu.edu/eos/users/r/rance/WWW/ncsu-cw.html.
• [9] P. Cousot, R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2, 1992, pp. 511-547.
• [10] N. De Francesco, A. Santone. A Tool Supporting Efficient Model Checking of Concurrent Specifications. Microprocessors and Microsystems, 25(9-10), 2002. pp. 401-407.
• [11] D. E. Denning, P. J. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7), 1977, pp. 504-513.
• [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] D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, 1983. pp. 333-354.
• [16] K.R.M. Leino, R. Joshi A semantic approach to secure information flow. Science of Computer Programming, 37(1), 2000.
• [17] 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.
• [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] D. A. Schmidt. Data-flow analysis is model checking of abstract interpretations. Proc. 25th ACM Symp. Principles of Programming Languages, San Diego, 1998.
• [21] 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.
• [22] 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.
• [23] D. Volpano, G. Smith, C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3), 1996, pp. 167-187.
• [24] D. Volpano, G. Smith. Eliminating covert flows with minimum typing. Proceedings 10th IEEE Computer Security Security Foundation Workshop, June 1997, pp. 156-168.