Room P3.10, Mathematics Building

Nobuko Yoshida, Imperial College, UK

Security analysis and controls for mobile code via types

The talk starts from a general background to illustrate the usage of mobile processes as an analysis tool for security issues in ubiquitous computing. In wide area distributed systems it is now common for mobile code to be transferred from one domain to another; the receiving host may initialise parameters and then execute the code in its local environment. We show that our fine-grained typing system for mobile processes can be used to control the effect of such migrating code on local environments. Processes may be assigned different interface types depending on their intended use. The advanced channel dependent types facilitate the management of access rights and provide host protection from potentially malicious behaviour. I shall also describe various applications of this type-based approach, including Secure Information Flow Analysis of Mobile Code, an analysis of correctness of optimised Distributed Java Code and safety guarantee of business protocols written in Web Services Languages.