Project Descriptions

Title: Programming Language-Based Security by Type-Checking

Supervisor: Nobuko Yoshida

Prequisites

This project requires knowledge of Java, concurrency programming, typing system and semantics in general. It is also recommended that a student doing this project should also take Models of Concurrent Computation , Type Systems for Programming Languages , Advanced Issues in Object Oriented Programming and Compilers .

Aims of Project

The increasing use of wide area networks by industry, government and individual customers means that a malicious attack or a bug of software could have immediate, widespread and irrecoverable consequences. However, current systems and programming languages lack the technology base to identify and detect potentially malicious mobile software.

Recently a promising new approach called information-flow analysis has been developed to guarantee the end-to-end confidentiality policy. This project is aimed to use a programming-language technique for specifying and enforcing information-flow policies.

Learning Outcomes

To learn about secure information analysis of programming languages and types of concurrent languages.
To specify, design and implement a type-checker to gurantee confidenciality of programming languages.

Project Timetable

Term 1

To learn about secrecy and confidentiality of programming languages; to learn about type-checking; to learn implementation of type-checking in Java; to specify and design a type-checker.

Term 2

Implementation of the type-checker.

References

Available from Nobuko Yoshida (yoshida@doc.ic.ac.uk).
Language-Based Information Flow Security (IEEE J-SAC). See page 7.

http://www.doc.ic.ac.uk/~yoshida/ (click secure information analysis).