Computer Laboratory

Khilan Gudka

I am a Research Associate in the Security Group at the University of Cambridge Computer Laboratory. Prior to this, I completed my PhD at the Department of Computing, Imperial College London. My research was generously funded by Microsoft Research Cambridge as part of their PhD Scholarship programme. You can find my old page here for reference purposes.

Research interests

  • Application compartmentalisation
  • Static/dynamic program analysis
  • Compilers/runtimes
  • Capability systems
  • Concurrency



Sandboxing technologies such as Capsicum and CHERI support the fine-grained compartmentalisation of large-scale applications such as web browsers and office suites, as well as multiple-component software such as the UNIX userspace. When deployed correctly, application compartmentalisation offers significant benefits by allowing policies to be imposed within applications, and in mitigating exploited vulnerabilities. However, application compartmentalisation remains an art rather than a science: identifying, implementing, and debugging partitioning strategies requires detailed expertise in both the application and security. SOAAP is exploring semi-automated techniques, grounded in static analysis, dynamic analysis, and automated program transformation, to improve the developer experience. This project is jointly funded by Google and DARPA, and takes place within the context of the CTSRD project.


This project is an outgrowth of our earlier Capsicum project, which explored hybrid capability models in the context of UNIX operating system design. While a successful project, we identified a number of limitations to current CPU designs that made application compartmentalisation tricky, despite enhanced operating system support. CHERI is a hardware-software interface research project seeking to revise ISA design in order to better support software compartmentalisation. CHERI transposes the Capsicum hybrid capability model into the CPU architecture space, allowing fine-grained compartmentalisation within process address spaces – while continuing to support current software designs.

We are developing a prototype of the CHERI ISA using the Bluespec Extensible RISC Implementation (BERI), a 64-bit MIPS FPGA soft core implemented in the Bluespec HDL. The FreeBSD operating system, with Capsicum support, has also been ported to CHERI in order to allow us to compare, side-by-side, traditional software compartmentalisation approaches (based on a translation look-aside buffer (TLB)), with those supported by a capability coprocessor. Using commodity software stacks, such as FreeBSD, LLVM, and the Chromium web browser, allows us to validate our hybrid design, applying capability-based compartmentalisation selectively to support both our most trusted (OS kernel, low-level language runtimes), and least trustworthy (web browsers and servers), software components.


TESLA builds on our experiences developing the TrustedBSD MAC Framework and Capsicum: our most critical security properties are frequently safety (temporal) properties rather than static invariants. Current tools for testing temporal properties are largely static, and unable to work effectively on extremely large C-language software bases, such as multi-million lines-of-code operating system kernels and web browsers. TESLA borrows ideas from model checking, applying them in a dynamic context using compiler-assisted instrumentation to continuously validate temporal security assertions during software execution. We have implemented a prototype of TESLA based on clang/LLVM AST transforms, which is able to test both explicit automata against C implementations (such as protocol state machines in the kernel and OpenSSL) and inline assertions checking for missing access control checks in OS logic.


  • Efficient Tagged Memory
    Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon. W. Moore, Alex Bradbury, Hongyan Xia, Robert N. M. Watson, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alfredo Mazzinghi, Alex Richardson, Stacey Son and A. Theodore Markettos.
    ICCD 2017, November 2017
  • CHERI JNI: Sinking the Java security model into the C
    David Chisnall, Brooks Davis, Khilan Gudka, David Brazdil, Alexandre Joannouand, Jonathan Woodruff, A. Theodore Markettos, J. Edward Maste, Robert Norton, Stacey Son, Michael Roe, Simon W. Moore, Peter G. Neumann, Ben Laurie, and Robert N. M. Watson
    ASPLOS 2017, April 2017
  • Fast Protection-Domain Crossing in the CHERI Capability-System Architecture
    Robert N. M. Watson, Robert M. Norton, Jon Woodruff, Simon W. Moore, Peter G. Neumann, Jon Anderson, David Chisnall, Brooks Davis, Ben. Laurie, Michael Roe, Nirav H. Dave, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, J. Edward Maste, Steven J. Murdoch, Colin Rothwell, Stacey D. Son and Munraj Vadera. Fast Protection-Domain Crossing in the CHERI Capability-System Architecture.
    IEEE Micro 36, 5 (2016), 38–49.
  • Clean Application Compartmentalization with SOAAP
    Khilan Gudka, Robert N. M. Watson, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Ilias Marinos, Peter G. Neumann, and Alex Richardson
    ACM CCS 2015, October 2015
  • CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization
    Robert N. M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera
    IEEE Symposium on Security and Privacy (IEEE S&P 2015), May 2015
  • TESLA: Temporally Enhanced System Logic Assertions
    Jonathan Anderson, Robert N. M. Watson, David Chisnall, Khilan Gudka, Brooks Davis, Ilias Marinos
    EuroSys 2014, April 2014
  • Towards a Theory of Application Compartmentalisation
    Robert N. M. Watson, Steven J. Murdoch, Khilan Gudka, Jonathan Anderson, Peter G. Neumann, Ben Laurie
    Security Protocols Workshop, March 2013
  • Lock Inference for Java
    Khilan Gudka
    PhD Thesis, Imperial College London, December 2012
    (Nominated for the BCS Distinguished Dissertation award)
  • Exploring Compartmentalisation Hypotheses with SOAAP (Slides)
    Khilan Gudka, Robert N. M. Watson, Steven Hand, Ben Laurie, Anil Madhavapeddy
    Workshop on Adaptive Host and Network Security (AHANS 2012), September 2012
  • Lock Inference in the Presence of Large Libraries (Slides)
    Khilan Gudka, Tim Harris, Susan Eisenbach
    ECOOP 2012, June 2012
  • Fast Multi-Level Locks for Java: A Preliminary Performance Evaluation (Slides)
    Khilan Gudka, Susan Eisenbach
    EC2 2010: Workshop on Exploiting Concurrency Efficiently and Correctly, July 2010
  • Keep Off The Grass: Locking the Right Path for Atomicity (Slides)
    David Cunningham, Khilan Gudka, Susan Eisenbach
    Compiler Construction 2008, October 2008

Contact details


Khilan Gudka
Computer Laboratory
15 JJ Thomson Avenue
Cambridge CB3 0FD
United Kingdom




+44 (0) 1223 763 602