Headshot

Khilan Gudka

I am a Research Associate in the Security Group at the University of Cambridge Computer Laboratory supervised by Dr. Robert N. M. Watson.

Prior to this, I completed my PhD at the Department of Computing, Imperial College London supervised by Professor Susan Eisenbach and Professor Sophia Drossopoulou. My research was generously funded by Microsoft Research Cambridge as part of their PhD Scholarship programme. My mentor at Microsoft was Dr. Tim Harris.

Email: [firstname].[lastname]@cl.cam.ac.uk
Profiles: Google Scholar, LinkedIn

Research interests

Security, Program Analysis, Compilers, Concurrency

Projects

Capability Hardware Enhanced RISC Instructions (CHERI)

CHERI is a hardware-software interface research project seeking to revise ISA design in order to provide fine-grained memory protection and better support for software compartmentalisation within process address spaces. Through commodity software stacks, such as FreeBSD, LLVM, and the Chromium web browser, we 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. I am currently researching into using CHERI to protect C++ applications, such as web browsers, mail readers, database engines and office suites.

Security-Oriented Analysis of Application Programs (SOAAP)

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 (and yet-to-be-discovered) 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. Part of this problem is the semantic gap between security policies that programmers understand and intend to implement, and the mechanisms and abstractions provided by the underlying platform, such as the OS. SOAAP is exploring semi-automated techniques, grounded in static analysis, dynamic analysis, and automated program transformation, to improve the developer experience and help better understand the security, performance and complexity tradeoffs with compartmentalisation.

Temporally Enhanced Security Logic Assertions (TESLA)

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.

Publications

Talks

Posters

Reports