Functional Active Objects: Noninterference and Distributed Consensus

In this report, we present recent work on the language of functional active objects ASPfun. We first introduce briefly the language ASPfun, its syntax and semantics. Then, we present a method for static security checking for our functional distributed active object language. We show how the type system of ASPfun is easily extensible for noninterference: a type system that enables analyzing an ASPfun program statically – prior to execution – detects information flows that contradict a given security policy. To prove this conjecture, we introduce the definition of an indistinguishability relation and prove the noninterference theorem that shows that this indistinguishability relation is a bisimulation on ASPfun executions. In a second part, we investigate the question of distributed consensus in ASPfun. We implement Paxos, a distributed consensus algorithm due to Lamport, in ASPfun. This implementation illustrates how functional active objects behave when stateful operations occur