Abstract
We present two main contributions: (i) an encoding of Boxed Ambients into a variant of Safe Ambients; (ii) a new Control Flow Analysis for Safe Ambients. Then, we show that the analysis, when applied to the encoded processes, permits to accurately verify Mandatory Access Control policies of the source processes.
Work partially supported by EU-project DEGAS (IST-2001-32072)
Chapter PDF
References
Amtoft, T., Kfoury, A.J., Pericas-Geertsen, S.M.: What are Polymorphically-Typed Ambients? In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 206. Springer, Heidelberg (2001)
Braghin, C., Cortesi, A., Focardi, R.: Control Flow Analysis for information flow security in mobile ambients. In: Proc. of FMOODS 2002, pp. 197–212 (2002)
Bugliesi, M., Castagna, G.: Secure safe ambients. In: Proc. of POPL 2001, pp. 222–235 (2001)
Bugliesi, M., Castagna, G., Crafa, S.: Boxed Ambients. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 38–61. Springer, Heidelberg (2001)
Bugliesi, M., Castagna, G., Crafa, S.: Reasoning about Security in Mobile Ambients. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 102–120. Springer, Heidelberg (2001)
Bugliesi, M., Crafa, S., Merro, M., Sassone, V.: Communication Interference in Mobile Boxed Ambients. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 71–84. Springer, Heidelberg (2002)
Cardelli, L., Ghelli, G., Gordon, A.D.: Mobility types for mobile ambients. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 230–239. Springer, Heidelberg (1999)
Cardelli, L., Ghelli, G., Gordon, A.D.: Types for the ambient calculus. Information and Computation 177(2) (2002)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Crafa, S., Bugliesi, M., Castagna, G.: Information Flow Security in Boxed Ambients. In: Proc. of FWAN 2002. ENTCS, vol. 66(3) (2002)
Degano, P., Levi, F., Bodei, C.: Safe Ambients: Control Flow Analysis and Security. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 199–214. Springer, Heidelberg (2000)
Dezani-Ciancaglini, M., Salvo, I.: Security Types for Mobile Safe Ambients. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 215–236. Springer, Heidelberg (2000)
Feret, J.: Abstract Interpretation-Based Static Analysis of Mobile Ambients. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 412–430. Springer, Heidelberg (2001)
Guan, X., Yang, Y., You, J.: Making Ambients More Robust. In: Proc. of the International Conference on Software: Theory and Practise, pp. 377–384 (2000)
Guan, X., Yang, Y., You, J.: Typing Evolving Ambients. Inf. Processing Letters 80(5), 265–270 (2001)
Hansen, R.R., Jensen, J.G., Nielson, F., Nielson, H.R.: Abstract Interpretation of Mobile Ambients. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 134–148. Springer, Heidelberg (1999)
Levi, F.: Types for Evolving Communication in Safe Ambients. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 102–115. Springer, Heidelberg (2002)
Levi, F., Bodei, C.: A Control Flow Analysis for Safe and Boxed Ambients (Extended Version), Available at: http://www.di.unipi.it/~levifran/papers.html
Levi, F., Maffeis, S.: An Abstract Interpretation Framework for Analysing Mobile Ambients. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 395–411. Springer, Heidelberg (2001)
Levi, F., Sangiorgi, D.: Controlling Interference in Ambients. In: Proc. of POPL 2000, pp. 352–364 (2000)
Levi, F., Sangiorgi, D.: Mobile Safe Ambients. TOPLAS 25(1), 1–69 (2003)
Merro, M., Hennessy, M.: Bisimulation congruences in Safe Ambients. In: Proc. of POPL 2002 (2002)
Merro, M., Sassone, V.: Typing and Subtyping Mobility in Boxed Ambients. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 304–320. Springer, Heidelberg (2002)
Nielson, F., Nielson, H.R., Hansen, R.R.: Validating firewalls using flow logics. CONCUR 1999 283(2), 381–418 (2002) Also (joint work also with J.G. Jensen) appeared in Baeten, J.C.M., Mauw, S. (eds.): CONCUR 1999. LNCS, vol. 1664, p. 463. Springer, Heidelberg (1999)
Nielson, H.R., Nielson, F.: Shape Analysis for Mobile Ambients. In: Proc. of POPL 2000, pp. 135–148 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Levi, F., Bodei, C. (2004). A Control Flow Analysis for Safe and Boxed Ambients. In: Schmidt, D. (eds) Programming Languages and Systems. ESOP 2004. Lecture Notes in Computer Science, vol 2986. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24725-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-24725-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21313-0
Online ISBN: 978-3-540-24725-8
eBook Packages: Springer Book Archive