Security boundaries in mobile ambients. (English) Zbl 1028.68004
Summary: A new notion of security boundary is introduced to model multilevel security policies in the scenario of mobile systems, within Cardelli and Gordon’s “pure” mobile ambients calculus. Information leakage may be expressed in terms of the possibility for a hostile ambient to access confidential data that are not protected inside a security boundary. A control flow analysis is defined, as a refinement of the Hansen-Jensen-Nielsons’s CFA, that allows to properly capture boundary crossings. In this way, direct information leakage may be statically detected.
MSC:
| 68M10 | Network design and communication in computer systems |
| 68P25 | Data encryption (aspects in computer science) |
References:
| [1] | Braghin, C.; Cortesi, A.; Focardi, R., Control flow analysis of mobile ambients with security boundaries, (Jacobs, B.; Rensink, A., Proceedings of Fifth IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS ’02) (2002), Kluwer Academic Publisher: Kluwer Academic Publisher Dordrecht), 197-212 · Zbl 1048.68025 |
| [2] | Cortesi A, Focardi R. Information flow security in mobile ambients. In: Proceedings of International Workshop on Concurrency and Coordination (ConCoord ’01), Electronic Notes on Theoretical Computer Science, ENTCS, vol. 54. Amsterdam: Elsevier, July 6-8, 2001.; Cortesi A, Focardi R. Information flow security in mobile ambients. In: Proceedings of International Workshop on Concurrency and Coordination (ConCoord ’01), Electronic Notes on Theoretical Computer Science, ENTCS, vol. 54. Amsterdam: Elsevier, July 6-8, 2001. · Zbl 1147.68330 |
| [3] | Cardelli L, Gordon AD. Mobile ambients. In: Nivat M, editor. Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS), Lecture Notes in Computer Science, vol. 1378, Berlin, Germany, Springer, March 1998, p. 140-55.; Cardelli L, Gordon AD. Mobile ambients. In: Nivat M, editor. Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS), Lecture Notes in Computer Science, vol. 1378, Berlin, Germany, Springer, March 1998, p. 140-55. |
| [4] | Bodei C, Degano P, Nielson F, Nielson HR. Static analysis of processes for No read-up and No write-down. In: Proceedings of FoSSaCS ’99, Lecture Notes in Computer Science, No. 1578. Berlin: Springer, 1999. p. 120-34.; Bodei C, Degano P, Nielson F, Nielson HR. Static analysis of processes for No read-up and No write-down. In: Proceedings of FoSSaCS ’99, Lecture Notes in Computer Science, No. 1578. Berlin: Springer, 1999. p. 120-34. |
| [5] | Focardi R, Gorrieri G, Martinelli F. Information flow analysis in a discrete-time process algebra. In: Proceedings of the 13th Computer Security Foundations Workshop (CSFW). Silver Spring, MD: IEEE Computer Society Press, 2000. p. 170-84.; Focardi R, Gorrieri G, Martinelli F. Information flow analysis in a discrete-time process algebra. In: Proceedings of the 13th Computer Security Foundations Workshop (CSFW). Silver Spring, MD: IEEE Computer Society Press, 2000. p. 170-84. |
| [6] | Focardi, R.; Gorrieri, R., A classification of security properties for process algebras, Journal of Computer Security, 3, 1, 5-33 (1995) |
| [7] | Focardi, R.; Gorrieri, R., The compositional security checkera tool for the verification of information flow security properties, IEEE Transactions on Software Engineering, 23, 9, 550-571 (1997) |
| [8] | Hennessy M, Riely J. Information flow vs. resource access in the asynchronous pi-calculus. In: Montanari U, Rolim J, Welzl E, editors. Proceedings of the International Colloquium on Automata Languages and Programming, Lecture Notes in Computer Science, vol. 1853. Berlin, Geneva: Springer, August 2000, p. 415-27.; Hennessy M, Riely J. Information flow vs. resource access in the asynchronous pi-calculus. In: Montanari U, Rolim J, Welzl E, editors. Proceedings of the International Colloquium on Automata Languages and Programming, Lecture Notes in Computer Science, vol. 1853. Berlin, Geneva: Springer, August 2000, p. 415-27. · Zbl 0973.68519 |
| [9] | Smith G, Volpano D. Secure information flow in a multi-threaded imperative language. In: Conference Record of POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, New York, NY, 1998. p. 355-64.; Smith G, Volpano D. Secure information flow in a multi-threaded imperative language. In: Conference Record of POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, New York, NY, 1998. p. 355-64. |
| [10] | Bugliesi M, Castagna G, Crafa S. Boxed ambients. In: Proceedings of the Fourth International Conference on Theoretical Aspects of Computer Science (TACS ’01), Lecture Notes in Computer Science, vol. 2215. Berlin: Springer, 2000. p. 38-63.; Bugliesi M, Castagna G, Crafa S. Boxed ambients. In: Proceedings of the Fourth International Conference on Theoretical Aspects of Computer Science (TACS ’01), Lecture Notes in Computer Science, vol. 2215. Berlin: Springer, 2000. p. 38-63. · Zbl 1087.68541 |
| [11] | Levi F, Sangiorgi D. Controlling interference in ambients. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL ’01), 2000. p. 352-64.; Levi F, Sangiorgi D. Controlling interference in ambients. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL ’01), 2000. p. 352-64. · Zbl 1323.68411 |
| [12] | Hansen, R. R.; Jensen, J. G.; Nielson, F.; Nielson, H. R., Abstract interpretation of mobile ambients, (Cortesi, A.; File’, G., Proceedings of Static Analysis Symposium (SAS ’99). Proceedings of Static Analysis Symposium (SAS ’99), Lecture Notes in Computer Science, No. 1694 (1999), Springer: Springer Berlin), 134-148 · Zbl 0957.68079 |
| [13] | Nielson F, Hansen RR, Nielson HR. Abstract interpretation of mobile ambients. In: Cortesi A, File’ G, editors. Science of computer programming (Special Issue on Static Analysis), to appear.; Nielson F, Hansen RR, Nielson HR. Abstract interpretation of mobile ambients. In: Cortesi A, File’ G, editors. Science of computer programming (Special Issue on Static Analysis), to appear. · Zbl 1047.68080 |
| [14] | Bodei C, Degano P, Nielson F, Nielson HR. Control flow analysis for the \(π\); Bodei C, Degano P, Nielson F, Nielson HR. Control flow analysis for the \(π\) |
| [15] | Cardelli L, Ghelli G, Gordon AD. Ambient groups and mobility types. In: van Leeuwen J, Watanabe O, Hagiya M, Mosses PD, Ito T, editors. Theoretical computer science: exploring new frontiers of theoretical informatics. Proceedings of the International IFIP Conference TCS 2000 (Sendai, Japan), Lecture Notes in Computer Science, vol. 1872. New York, Berlin: IFIP, Springer, August 2000. p. 333-47.; Cardelli L, Ghelli G, Gordon AD. Ambient groups and mobility types. In: van Leeuwen J, Watanabe O, Hagiya M, Mosses PD, Ito T, editors. Theoretical computer science: exploring new frontiers of theoretical informatics. Proceedings of the International IFIP Conference TCS 2000 (Sendai, Japan), Lecture Notes in Computer Science, vol. 1872. New York, Berlin: IFIP, Springer, August 2000. p. 333-47. · Zbl 0998.68536 |
| [16] | Dezani-Ciancaglini M, Salvo I. Security types for mobile safe ambients. In: He J, Sato M, editors. Proceedings of Advances in Computing Science—ASIAN ’00 (Sixth Asian Computing Science Conference, Penang, Malaysia), Lecture Notes in Computer Science, vol. 1961, Berlin, Springer, December 2000, p. 215-36.; Dezani-Ciancaglini M, Salvo I. Security types for mobile safe ambients. In: He J, Sato M, editors. Proceedings of Advances in Computing Science—ASIAN ’00 (Sixth Asian Computing Science Conference, Penang, Malaysia), Lecture Notes in Computer Science, vol. 1961, Berlin, Springer, December 2000, p. 215-36. · Zbl 0988.68544 |
| [17] | Degano P, Levi F, Bodei C. Safe ambients: control flow analysis and security. In: He J, Sato M, editors. Proceedings of Advances in Computing Science—ASIAN ’00 (Sixth Asian Computing Science Conference, Penang, Malaysia), Lecture Notes in Computer Science, vol. 1961, Berlin, Springer, December 2000, p. 199-214.; Degano P, Levi F, Bodei C. Safe ambients: control flow analysis and security. In: He J, Sato M, editors. Proceedings of Advances in Computing Science—ASIAN ’00 (Sixth Asian Computing Science Conference, Penang, Malaysia), Lecture Notes in Computer Science, vol. 1961, Berlin, Springer, December 2000, p. 199-214. · Zbl 0988.68543 |
| [18] | Bugliesi M, Castagna G. Secure safe ambients. In: Proceedings of 28th ACM Symposium on Principles of Programming Languages (POPL ’01). New York: ACM Press, 2001. p. 222-35.; Bugliesi M, Castagna G. Secure safe ambients. In: Proceedings of 28th ACM Symposium on Principles of Programming Languages (POPL ’01). New York: ACM Press, 2001. p. 222-35. · Zbl 1323.68404 |
| [19] | Bugliesi M, Castagna G. Behavioural typing of safe ambients. Journal of Computer Security, this issue.; Bugliesi M, Castagna G. Behavioural typing of safe ambients. Journal of Computer Security, this issue. · Zbl 1028.68005 |
| [20] | Levi F, Bodei C. Security analysis for mobile ambients. In: Electronic Proceedings of IFIP WG 1.7 Workshop on Issues on the Theory of Security (WITS ’00), Geneve, 2000.; Levi F, Bodei C. Security analysis for mobile ambients. In: Electronic Proceedings of IFIP WG 1.7 Workshop on Issues on the Theory of Security (WITS ’00), Geneve, 2000. · Zbl 0988.68543 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
