Home Detail

Lecturer: Dr. Florian Kammüller (Middlesex University in London und TU Berlin)




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 addresses 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.

back