Abstract
A multilevel security policy is considered in the scenario of mobile systems, and modeled within “pure” Mobile Ambients calculus, in which no communication channels are present and the only possible actions are represented by the moves performed by mobile processes. The information flow property of interest is defined in terms of the possibility for a confidential ambient/data to move outside a security boundary. In a previous paper, we gave a very simple syntactic property that is sufficient to imply the absence of unwanted information flows. In this paper, a control flow analysis is defined, as a refinement of the Hansen-Jensen-Nielsons’s CFA, that allows to capture boundary crossings with better accuracy.
Partially supported by MURST Projects “Interpretazione Astratta, Type Systems e Analisi Control-Flow”, and “Certificazione automatica di programmi mediante interpretazione astratta”.
Chapter PDF
Similar content being viewed by others
References
Cortesi, A. and Focardi, R. (2001). Information Flow Security in Mobile Ambients. In Proc. of International Workshop on Concurrency and Coordination CONCOORD’01, Lipari Island, July 2001, volume 54 of Electronic Notes in Theoretical Computer Science, Elsevier.
Bodei, C., Degano, P., Nielson, F. and Nielson, H. R. (1999). Static Analysis of Processes for No Read-Up and No-Write-Down. In Proc. FoSSaCS’99, volume 1578 of Lecture Notes in Computer Science,pages 120–134, Springer-Verlag.
Bugliesi, M. and Castagna, G. (2001). “Secure Safe Ambients”. Proc. 28th ACM Symposium on Principles of Programming Languages (POPL’01), pp. 222–235, London.
Cardelli, L. and Gordon, A. (1998). “Mobile Ambients”. In Proc. FoSSaCS’98, volume 1378 of Lecture Notes in Computer Science,pages 140–155, Springer-Verlag.
Degano, P., Levi, F. and Bodei, C. (2000). Safe Ambients: Control Flow Analysis and Security. In proceedings of ASIAN’00, LNCS 1961, 2000, pages 199–214.
Focardi, R. and Gorrieri, R. (1995). “A Classification of Security Properties for Process Algebras”, Journal of Computer Security, 3 (1): 5–33.
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, Vol. 23, No. 9.
Focardi, R., Gorrieri, R. and Martinelli, F. (2000). “Information Flow Analysis in a Discrete Time Process Algebra”, in Proc. of 13th IEEE Computer Security Foundations Workshop (CSFW 13 ), ( P.Syverson ed ), IEEE CS Press, 170–184.
Hansen, R. R., Jensen, J. G., Nielson, F. and Nielson, H. R. (1999). Abstract Interpretation of Mobile Ambients. In Proc. Static Analysis Symposium SAS’99, volume 1694 of Lecture Notes in Computer Science,pages 134–148, Springer-Verlag.
Hennessy, M. and Riely, J. (2000). “Information Flow vs. Resource Access in the Asynchronous Pi-Calculus”. ICALP 2000: 415–427.
Smith, G. and Volpano, D. M. (1998). “Secure Information Flow in a Multi-Threaded Imperative Language”. In Proc. of POPL 1998: 355–364.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 IFIP International Federation for Information Processing
About this paper
Cite this paper
Braghin, C., Cortesi, A., Focardi, R. (2002). Control Flow Analysis of Mobile Ambients with Security Boundaries. In: Jacobs, B., Rensink, A. (eds) Formal Methods for Open Object-Based Distributed Systems V. FMOODS 2002. IFIP — The International Federation for Information Processing, vol 81. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35496-5_14
Download citation
DOI: https://doi.org/10.1007/978-0-387-35496-5_14
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5268-7
Online ISBN: 978-0-387-35496-5
eBook Packages: Springer Book Archive