Project Descriptions

Title: Security Guarantee in Mobile Agents

Supervisor: Nobuko Yoshida

Prequisites

This project requires knowledge of concurrency programming, types and semantics in general. In particular (a bit of) knowledge of process algebra such as FSP (Finite State Processes) taught in Concurrency Programming course, CCS, CSP or the pi-calculus is required. It is also recommended that a student doing this project should also take Distributed Systems , Models of Concurrent Computation , Compilers , Type Systems for Programming Languages and Multi-Agent Systems .

Aims of Project

This project investigates and implements a type-checking system to guarantee security and safety in distributed mobile computing.

This project is built-on a recent study of a typing theory in mobile computing. During your project, you will be able to learn a powerful concurrent formalism called the (higher-order) pi-calculus. (Recently the pi-calculus is used to design a shipping server product, the XLang Scheduler in Microsoft BizTalk Server 2000 . Also the pi-calculus was introduced as a key formal model for XML in a major XML text book, Professional XML 2nd Edition, Wrox Press 2001).

Thus this project is very challenging and fun because you can learn both the pi-calculus (advanced theory) and type-checking (implementation).

Learning Outcomes

To learn about type-checking of higher-order mobile processes.
To specify, design and implement a type-checker to guarantee confidentiality and access controls.

Project Timetable

Term 1

To learn about concurrent mobile processes; to learn about type-checking; to specify and design a type-checker.

Term 2

Implementation of the type-checker.

References

Available from Nobuko Yoshida (yoshida@doc.ic.ac.uk).
http://www.doc.ic.ac.uk/~yoshida/ (click secure information analysis and access control of mobile processes ).

Calculi for Mobile Processes