Swarn Priya

My Image



Google Scholar


About me

I am a doctoral researcher at Inria, Sophia Antipolis, France, in the STAMP team working with Yves Bertot and Benjamin Grégoire. I am also a third-year Ph.D. student in the department of Computer Science at Université Côte d'Azur, France. I am working on applying formal methods in the security domain. More generally, I am working on providing 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.


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 am currently working 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.