University of Cambridge > Talks.cam > Computer Laboratory Digital Technology Group (DTG) Meetings > Language Based Security for Functional Active Objects

Language Based Security for Functional Active Objects

Add to your list(s) Download to your calendar using vCal

  • UserFlorian Kammueller, Middlesex University, London and Technische Universitaet, Berlin
  • ClockMonday 15 November 2010, 13:00-14:00
  • HouseSS03, William Gates Building.

If you have a question about this talk, please contact Andrew Rice.

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.

This talk is part of the Computer Laboratory Digital Technology Group (DTG) Meetings series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity