Abstract

Programming in large networks of computers, like the Internet, poses new problems of safely implementing parallel activities, code distribution, and complex communication structures. This talk presents current work on the security analysis of active objects in ASPfun—our calculus for functional distributed objects that communicate asynchronously.

In ASPfun, requests to objects are method calls represented by so-called futures; replies finally return the result to the object containing the future. We have developed and completely formalized ASPfun and its properties in the interactive theorem prover Isabelle/HOL. This includes a type system and a proof of type safety. We also provide a prototype interpreter for ASPfun written in Erlang.

This talk motivates security issues for distributed active objects: it introduces ASPfun using a simple running example to present the language and the security problem we address. We introduce a formal notion of information flow security. The main novelty presented is a type system that enables static security analysis of ASPfun programs. We wrap up by presenting our future plans on developing a language based modular assembly kit for security centered around ASPfun and security type systems.