  In this paper, we provide a formal framework for the security of distributed
active objects. Active objects communicate asynchronously implementing method
calls via futures. We base the formal framework on a security model that uses a
semi-lattice to enable multi-lateral security crucial for distributed
architectures. We further provide a security type system for the programming
model ASPfun of functional active objects. Type safety and a confinement
property are presented. ASPfun thus realizes secure down calls.

Cryptography and Security