About

I apply Programming Language Techniques to Security Research.

I am currently a Postdoctoral Researcher at ETH Zurich, where I work in the Information Security Group headed by Prof. David Basin. I am currently investigating the following questions:

• Can intrinsic typing be applied to prove compiler correctness for ML compilers as well as WASM interpreters/compilers?
  • Starting with standard safety properties like type soundness, can we verify hyperproperties like noninterference?
• Can MLIR's concept of dialects, capable of expressing multiple levels of abstraction in one IR, be the ultimate tool for semantic-preserving property compilation?

Researchers or students interested in these fields are welcome to send me an email.

I completed my PhD from Chalmers University, Gothenburg, under the supervision of Prof. Mary Sheeran, where I worked extensively on compilers and language runtimes, focussing on functional programming languages.

My PhD produced tools like - HasTEE+, a Haskell DSL for programming Trusted Execution Environments that enforces Information Flow Control, and SynchronVM, a soft real-time virtual machine supporting functional programming on microcontrollers.

Topic-wise, I am broadly interested in the following in no particular order:

• All aspects of programming language implementation - compilers, runtimes, memory management, type systems, etc.
• Information Flow Control
• Certified Programming with proof assistants such as Agda, Lean, Isabelle/HOL
• Compiler Verification
• Operating Systems and their Security
• Computer Architecture (specifically Microarchitectural Security)
• Concurrency and Parallelism

I sporadically read about logic and philosophy in my spare time.

Contact me at my ETH email

Recommended Reading:

The Computer Scientist as Toolsmith.

Reflections on Trusting Trust.