In this paper we present an approach for the enforcement of privacy in distributed active object systems, illustrate its implementation in the language ASPfun, and formally prove privacy based on information flow security. We aim at using functional active objects as a language calculus and build a logical tool set for compositional properties. Since already on the simpler trace models the definition and theory development for a MAKS is an intrinsically complex task, we additionally employ Isabelle/HOL as a verification environment to support us. The derived LB-MAKS security properties shall be transformed into security type systems -- in the sense as described in the previous section -- to derive practically useful static analysis tools from our mechanized LB-MAKS. The presented currying concept is a first important step towards such an enforcement library. A further important stepping stone is the definition of hiding for ASPfun. It helps bridging the gap between abstract trace based semantics and more detailed language based models as illustrated in this paper.

To our knowledge no one has considered the use of futures in combination with confinement given by objects as a means to characterize information flow. The major advantage of our approach is that we are less abstract than event systems while being abstract enough to consider realistic distributed applications.