About me

I am a Postdoctoral Research Associate in the Systems Software Research Group, Bradley Department of Electrical and Computer Engineering at Virginia Tech, VA, United States, working with Professor Binoy Ravindran in the domain of application of formal methods in the area of systems and security.

I obtained my Ph.D. degree from Inria, Sophia Antipolis and Université Côte d'Azur, France. I was the member of STAMP and SPLiTS team working with Yves Bertot and Benjamin Grégoire. I worked on applying formal methods in the security domain. More generally, I worked on designing a secure formally verified compiler, which includes machine-checked, formally verified mitigations against timing-based side-channel attacks.

I was also awarded "Young Talent Women in Science" award for my research work in the domain of Formal Methods by UNESCO-L'Oréal in the year 2023 during my Ph.D.

I obtained my master's degree in Computer Science from Iowa State University, United States. During my master's thesis, I designed a programming language for Message Passing Concurrency with an intensional receive and also provided machine-checked soundness proof.

I obtained my bachelor's degree in Electronics and Instrumentation from West Bengal University, India.

Research

My research interests include formal methods, programming languages and type systems, software security, and applications of formal methods in various domains like security, blockchain, etc. I firmly believe in providing machine-checked guarantees (using the theorem prover Coq) for absence of bugs and the preservation of critical properties in various domains. I am a pleased user of Coq proof assistant.

Research during Post-Doc.

I am working on designing an end-to-end formally verified framework to write safe and correct eBPF programs. It involves designing a verification-friendly language, a strong type system (reasons about most of the eBPF properties at compile time), and a formally verified compiler (incorporates CompCert on its way to produce BPF bytecode). All the development is done using Coq. The development is present here

I am also working on developing a formally verified semantic equivalence checker between x86 and CHERI architectures. This work is motivated by the goal of safely porting legacy x86 binaries to CHERI-enabled platforms (ARM/RISC-V), leveraging CHERI’s fine-grained memory protection and capability-based security model. My focus is on ensuring semantic correctness between the original x86 binaries and their CHERI counterparts—an essential step in verifying the correctness of the underlying transpilation process. The static analysis framework will be grounded in abstract interpretation, and the entire equivalence-checking pipeline will be formally verified to ensure soundness and reliability.

Research during Ph.D.

I worked with the Jasmin framework. Jasmin framework consists of the Jasmin language, a formally verified compiler, and support of tools to prove various properties like safety, constant-time, etc., at the source level. The Jasmin language is used to write high-assurance and efficient cryptography. It gives the programmer control over low-level details like the freedom of choosing the storage class (register or stack) of program variables and includes high-level constructs. The Jasmin compiler is formally verified for its correctness using Coq.

My work involves making Jasmin compiler more reliable and trustworthy. I formally proved (using the theorem prover Coq) that the Jasmin compiler preserves cryptographic constant-time property. The development is present here.

I also extended the previous work to prove (using the theorem prover Coq) the preservation of constant-time property targeting the fine-grained leakage models. The fine-grained leakage model extends the baseline leakage model (leaking only branching condition and accessed memory addresses) to include stronger (taking into account time-variable operations) and weaker leakage models (leaking the cache line of the address being accessed). The development is present here.

I also worked on providing mitigations against "Spectre" attacks (mainly Spectre v1) for a simple language using an information-flow based type-system. The soundness of the type system is proved using Coq. The development is present here. This idea is also extended for Jasmin framework. The soundness proof is done on paper. The development is present here.

Research during Masters

I worked on desigining a message passing-based language that incorporates an intensional design of the receive expression. This intensional receive helps in reasoning about the type of the message received by any process and its effect. Intensional design of receive expression integrates static and dynamic type checking and allows the effect of the message received to be intensionally inspected through a notion of dynamic typing. This enables reasoning about the effect of the message received from the head of the mailbox while retaining static type safety. The idea is formally verified for soundness using Coq. The development is present here.