NICTA Embedded Systems Public Seminar
Analysing the Information Flow Properties of Object-Capability Patterns
Toby Murray, Oxford
Time/Venue
2:30pm
Wednesday, 28th November, 2009
NICTA, Neville Roach Laboratory, Level 1 Seminar Room, 223 Anzac Parade (Building L5), Kensington NSW 2052
Abstract
Object-capability systems, such as the seL4 microkernel or Google's Cajita JavaScript dialect, are becoming an increasingly popular platform for the deployment of highly secure systems. Security policies are enforced in object-capability systems by deploying security-enforcing abstractions, known as patterns, in much the same way that ordinary functional concerns are managed by programmers deploying functional abstractions.
In this talk, we will consider how to analyse the information flow properties of object-capability patterns using the process algebra CSP. We identify a basic assumption that any object-capability system must meet in order to talk sensibly about the information flow properties of the patterns that might be deployed within it. We formalise this assumption in terms of CSP's theory of refinement, which leads to a natural definition of information flow under this assumption that can be automatically tested using CSP's refinement checker FDR. We demonstrate this by modelling and analysing Miller's Data-Diode pattern, which can be used for example to control the flow of data between compartments in a Multi-Level Secure (MLS) system, allowing us to detect and correct covert channels within it.
Biography:
Toby Murray is a research student who is currently undertaking a PhD at the University of Oxford, investigating the formal analysis of security in object-capability systems. He holds a Bachelor of Computer Science with First Class Honours from the University of Adelaide. Before coming to Oxford, he worked as a research scientist for the Defence Science and Technology Organisation, where he worked on the Annex project researching and developing security architectures for ubiquitous Defence systems.