BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Language Based Security for Functional Active Objects - Florian Ka
 mmueller\, Middlesex University\, London and Technische Universitaet\, Ber
 lin
DTSTART:20101115T130000Z
DTEND:20101115T140000Z
UID:TALK25465@talks.cam.ac.uk
CONTACT:Andrew Rice
DESCRIPTION:Programming in large networks of computers\, like the Internet
 \, poses new\nproblems of safely implementing parallel activities\, code d
 istribution\, and\ncomplex communication structures. This talk presents cu
 rrent work on the\nsecurity analysis of active objects in ASPfun -- our ca
 lculus for\nfunctional distributed objects that communicate asynchronously
 .\n\nIn ASPfun\, requests to objects are method calls represented by so-ca
 lled\nfutures\; replies finally return the result to the object containing
  the\nfuture.\nWe have developed and completely formalized ASPfun and its 
 properties\nin the interactive theorem prover Isabelle/HOL. This includes 
 a type system\nand a proof of type safety. We also provide a prototype int
 erpreter for\nASPfun\nwritten in Erlang.\n\nThis talk motivates security i
 ssues for distributed active objects:\nit introduces ASPfun using a simple
  running example to present the language\nand the security problem we addr
 ess. We introduce a formal notion of\ninformation\nflow security. The main
  novelty presented is a type system that enables\nstatic\nsecurity analysi
 s of ASPfun programs.\nWe wrap up by presenting our future plans on develo
 ping a language based\nmodular\nassembly kit for security centered around 
 ASPfun and security type systems.
LOCATION:SS03\, William Gates Building
END:VEVENT
END:VCALENDAR