Michele Bugliesi
Giuseppe Castagna
Abstract
Secure Safe Ambients (SSA) are a typed variant of Safe Ambients [9], whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and implicit process and ambient behavior: process types account not only for immediate behavior, but also for the behavior resulting from capabilities a process acquires during its evolution in a given context. Based on that, the type system provides for static detection of security attacks such as Trojan Horses and other combinations of malicious agents.We study the type system of SSA, define algorithms for type checking and type reconstruction, define powerful languages for expressing security properties, and study a distributed version of SSA and its type system. For the latter, we show that distributed type checking ensures security even in ill-typed contexts, and discuss how it relates to the security architecture of the Java Virtual Machine.
- 1 D. Brewer and M. Nash. The chinese wall security policy. In Proc. of lEEE Symposium on Security and Privacy, pages 206-214, 1982.Google Scholar
- 2 H. R. N. C. Bodei, E Degano and E Nielson. Static analysis of processes for no read-up and no write-down. In Porceedins of FoSSaCS'99. 1999.Google Scholar
- 3 L. Cardelli, G. Ghelli, and A. Gordon. Mobility types for mobile ambients. In Proceedings of ICALP'99, LNCS 1644, pages 230-239. 1999.Google ScholarCross Ref
- 4 L. Cardelli, G. Ghelli, and A. D. Gordon. Ambient groups and mobility types. In Int. Conf. IFIP TCS, LNCS 1872, pages 333-347. 2000.Google ScholarCross Ref
- 5 L. Cardelli and A. Gordon. Mobile ambients. In Proceedings of POPL'98. ACM Press, 1998. Google ScholarDigital Library
- 6 L. Cardelli and A. Gordon. Types for mobile ambients. In Proceedings of POPL'99, pages 79-92. ACM Press, 1999. Google ScholarDigital Library
- 7 P. J. Denning. Fault tolerant operating systems. ACM Computing Surveys, 8(4):359-389, Dec. 1976. Google ScholarDigital Library
- 8 L. Gong. Inside Java 2 Platform Security. Addison-Wesley, 1999. Google ScholarDigital Library
- 9 E Levi and D. Sangiorgi. Controlling interference in ambients. In POPL '00, pages 352-364. ACM Press, 2000. Google ScholarDigital Library
- 10 T. Lindholm and E Yellin. The Java Virtual Machine Specification. Java series. Addison-Wesley, 1997. Google ScholarDigital Library
- 11 G. Necula. Proof carrying code. In A. Press, editor, POPL '97, 1997. Google ScholarDigital Library
- 12 E Nielson, H. R. Nielson, R. R. Hansen, and J. G. Jensen. Validating firewalls in mobile ambients. In Proc. CONCUR'99, LNCS 1664, pages 463-477, 1999.Google ScholarCross Ref
- 13 H. R. Nielson and F. Nielson. Shape analysis for mobile ambients. In POPL'00, pages 135-148. ACM Press, 2000. Google Scholar
- 14 P. Sewell and J. Vitek. Secure composition of untrusted code: Wrappers and causality types. In 13th IEEE Computer Security Foundations Workshop, 2000. Google ScholarDigital Library
- 15 J. Vitek and G. Castagna. Seal: A framework for secure mobile computations. In Internet Programming Languages, LNCS 1686, 1999.Google ScholarDigital Library
Index Terms
- Secure safe ambients
Recommendations
Secure safe ambients
POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesSecure Safe Ambients (SSA) are a typed variant of Safe Ambients [9], whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and ...
Behavioural typing for safe ambients
We introduce a typed variant of Safe Ambients, named Secure Safe Ambients (SSA), whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both ...
Security Types for Mobile Safe Ambients
ASIAN '00: Proceedings of the 6th Asian Computing Science Conference on Advances in Computing ScienceThe Ambient Calculus and the Safe Ambient Calculus have been recently successfully proposed as models for the Web. They are based on the notions of ambient movement and ambient opening. Different type disciplines have been devised for them in order to ...
Comments