OS and C Language Security
My postdoc is with the CTSRD project, which is funded by DARPA's CRASH program. I am currently focussed on TESLA: Temporally Enhanced Security Logic Assertions. TESLA allows programmers to make assertions about their code that are temporal in nature: rather than asserting that "x is non-negative", programmers can assert that "between the beginning of the system call and now, an access control check was done" or "the life cycle of this structure follows an explicit finite-state automaton". This allows programmers to succinctly describe complex systemic invariants (e.g. locking, access control) whose violations are difficult to detect with conventional bug-finding tools.
This project grew out of lessons learned during the Capsicum project, which brought capability-based confinement to a real operating system (FreeBSD) running real code today. Capsicum allows applications as simple as tcpdump or as complex as Chromium to be properly sandboxed, with robust confinment and a usable API (a POSIX subset).
Capsicum provided process-based isolation that worked well but did not scale to thousands of security domains. At that scale, the use of virtual-memory–based protection (UNIX processes) collided with limitations of today's translation lookaside buffers (TLBs). To go further requires new hardware primitives; this is the research territory of the CTSRD project.
Robert Watson and I have merged Capsicum into mainline FreeBSD, but a kernel compile option is required to turn it on.
Privacy in Social Networks
My PhD research focussed on privacy in social entworking. We all know how useful today's online social networking tools can be, but they often have the unfortunate side effect of sharing your life with people and companies that you haven't chosen. Aside from demonstrating problems with the status quo, I designed an architecture and prototype implementation to prove that it's possible to have both privacy and the benefits of social networking.
Without trusting any provider to enforce users' desired sharing and security policies, this work provided:
- a scheme for secure, sharable storage that costs less than $1/user/year,
- a platform for least-privileged social applications that can do useful work and
- a distributed authentication scheme that can be used with very weak passwords.
University of Cambridge
15 JJ Thomson Avenue
Cambridge CB3 0FD
Phone: +44 1223 763747
Email: [my first name].[my last name]@cl.cam.ac.uk
Before coming to Cambridge, I completed a Bachelor of Engineering and a Master of Engineering (under the supervision of Howard Heys) in the Faculty of Engineering, Memorial University of Newfoundland.