Functional Active Objects: Noninterference and Distributed Consensus
Ludovic Henrio, Florian Kammüller · DepositOnce · 2009
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.