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 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 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 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.
