About
I am a Ph.D. candidate in the Computer Science department at Cornell University advised by Prof. Justin Hsu. Previously, I worked on software-defined networking as a software engineer at Microsoft for a year and prior to that, I was an undergraduate student at BITS Pilani, India. During my undergrad, I had the pleasure to spend a semester at the Max Planck Institute for Software Systems in Germany working with Dr. Bjoern Brandenburg on a theory-oriented real-time operating system (TOROS) toward my undergraduate thesis.
Research Focus Safe<T> ✨ Project Website
My dissertation research focus is to design provably correct runtime monitoring mechanisms for enforcing safety and security properties in systems without access to the source code. I focus on systems with hierarchical execution structures, like trees, and have designed an automata-theoretic monitoring framework Safe<T> based on finite state automaton [2] and visibly pushdown automaton [3] (for control flow properties). A central theme of this monitoring mechanism is that it is distributed, non-invasive, and treats the system as a blackbox. To demonstrate the practical impact of my research, I’ve implemented the runtime monitors — SafeTree [3] and SafeNom [4] — for microservice applications. The class of safety properties enforceable by this framework naturally transfer to various domains, like finance, healthcare, and safety-critical cyber-physical systems.
Selected First-Author Publications
-
(Submitted)Karuna Grewal, Brighten Godfrey, Justin Hsu
Talks
-
Automaton-Based Expressive Monitoring of Blackbox Systems[Abstract ▾]
Safety-critical systems in domains like healthcare, finance, and autonomous systems are increasingly built from black-box components whose source code is unavailable for inspection. To certify safe and secure inter-component interactions in such systems, security and compliance teams must enforce policies over sequential and nested call/return patterns in the inter-component interactions, along with the data values exchanged between the components. Furthermore, the blackbox setting necessitates decoupling the policy enforcement mechanism from the system implementation. To this end, we design an expressive specification language for control and data-aware policies and an automaton-based enforcement mechanism. Our technique is blackbox and non-invasive, i.e., it does not require any access or changes to the system’s code. To realize our method, we build a distributed runtime monitor on top of an emerging network infrastructure layer that can control inter-component communication during deployment.
- Cornell PL Discussion Group, Apr 2026
- Purdue PL Seminar, Apr 2026
- UPenn PLClub Discussion Group, May 2026
-
SafeTree: Expressive Tree Policies for Microservices[Abstract ▾]
A microservice-based application is composed of self-contained components called services that collectively process a request. Controlling inter-service communications is key to enforcing safety properties in such applications. Presently, only a limited class of single-hop properties can be specified. These policies can be overly permissive because they ignore the rich service tree structure of the inter-service communications. Policies that can express the service tree structure will offer fine-grained control over communication patterns to development and security teams. In this talk, firstly, I will present an expressive policy language to specify service tree structures. Then, I will focus on our visibly pushdown automata-based runtime monitoring technique for enforcing service tree policies. Finally, I will present our engineering solution for a distributed monitor on top of an existing microservice deployment framework.
- OOPSLA, Oct 2025
- Upstate Programming Languages Seminar, Aug 2025
- UIUC Formal Methods Seminar, Apr 2025
- New Jersey Programming Languages and Systems Seminar, Dec 2024
-
Expressive Policies for Microservice Networks[Abstract ▾]
Microservice-based application deployments need to administer safety properties while serving requests. However, today such properties can be specified only in limited ways that can lead to overly permissive policies and the potential for illegitimate flow of information across microservices, or ad hoc policy implementations. We argue that a range of use cases require safety properties for the flow of requests across the whole microservice network, rather than only between adjacent hops. To begin specifying such expressive policies, we propose a system for declaring and deploying service tree policies. These policies are compiled down into declarative filters that are inserted into microservice deployment manifests. We use a light-weight dynamic monitor based enforcement mechanism, using ideas from automata theory. Experiments with our preliminary prototype show that we can capture a wide class of policies that we describe as case studies.
- UCSC Languages, Systems, and Data Seminar, Mar 2024
- HotNets, Nov 2023
- UIUC Service Layer Networking Workshop, Oct 2023
P4BID: Information Flow Control in P4[Abstract ▾]
Modern programmable network switches let developers write complex packet processing pipelines that can run at speeds of 6.5Tbps, and the programming language P4 provides high-level constructs that make programming such switches fairly simple. The increase in speed and programmability has started a new era of network programming where many complex functionalities, e.g., key-value stores and load balancers, are being moved to these fast switches. We show that this increased programmability enables a new family of security bugs, that is, information leaks that can lead to broken confidentiality, integrity, and isolation in the network. We then present a new information-flow control type system for dataplane programming in P4 that can detect this family of security bugs. Our type system contains rules that are completely specific to the P4 language and can therefore handle complex constructs such as P4 tables. We implement our type system in a tool, P4bid, which extends the type checker in the p4c compiler, the reference compiler for P4_16, the latest version of P4. We present a number of case studies and show that P4bid can successfully detect information flow violations in all of them, while correctly type-checking corrected versions of these programs where the information leaks are removed.
- Bloomberg NYC, Sep 2023
- PLDI, Jun 2022
- Bellairs Network Verification Workshop, May 2022
Service
Currently, I am serving as a PLTea organizer and the Czar for the Cornell PL Discussion Group. I have also served on the artifact evaluation committee for POPL'{24, 25}.
News
-
Jun'26
-
May'26🏅 I have been awarded the LinkedIn Ph.D. fellowship!
-
Aug'25🎉 "SafeTree: Expressive Tree Policies for Microservices" has been accepted to OOPSLA'25.
This paper highlights the central theme of my dissertation research!! -
Apr'24🎉 I passed my A exam! Thanks to my advisor and collaborators---Justin, Brighten, and Loris!
-
Mar'24🎉 I'll spend this summer as an Applied Scientist intern at Amazon Science's Automated Reasoning research group.
-
Sep'23🎉 "Expressive Policies for Microservice Networks" with Brighten Godfrey and Justin Hsu to appear at HotNets'23.
-
May'23I will be organizing the PLTea social events at PLDI'23. Do join us!
-
Apr'23I am joining the organizational team of PLTea, a meetup for programming languages enthusiasts.
-
May'22I'll be attending the Bellairs Network Verification Workshop.
-
Feb'22🎉 P4BID: Information Flow Control in P4 got accepted to PLDI’22.
-
Sep'21I started my Ph.D. at Cornell (advised by Prof. Justin Hsu).
Teaching
- Spring'26 - CS3410: Computer System Organization and Programming, by Prof. Adrian Sampson
- Spring'22 - CS5412: Topics in Cloud Computing, by Prof. Ken Birman
Contact
You can reach me at: [(λx.x @ cs.cornell.edu) kgrewal]; LinkedIn; or GitHub.