关于
I am a Principal Researcher at Microsoft Research India. My work spans the areas of language design, type systems, program verification, and software security. More specifically, I am interested in developing formal techniques for writing provably correct and secure software.
I am one of the core designers and developers of F* (opens in new tab), a language for program verification. In Project Everest (opens in new tab), we are using F* to build and deploy a verified HTTPS stack.
I received my PhD from the Computer Science Dept. (opens in new tab) at the University of Maryland, College Park, where I was advised by Michael Hicks (opens in new tab). Before that, I did M.S. from the Computer Science Dept. (opens in new tab) at the Stony Brook University working with Rob Johnson (opens in new tab).
I am serving or have served on the following committees:
- PC co-chair: ISEC 2024
- Diversity, Equity, and Inclusion co-chair: POPL 2024
- Program Committee: PLDI 2024, CSF 2024, OOPSLA 2022, CSF2022, CPP 2022, Indocrypt 2021, POPL 2021, CSF 2021, CCS 2020, FSTTCS 2020, Indocrypt 2020, FCS 2020, PLAS 2019, ISEC 2019, POPL 2018, CCS 2017, APLAS 2017, HOPE 2017, FTfJP 2017
- External Review Committee: PLDI 2020, PLDI 2019, PLDI 2016, POPL 2017, PLDI 2017
- Artifact Evaluation Committee: POPL 2017
- Reviewer, ACM Transactions on Programming Languages and Systems (TOPLAS)
- Tutorials and Tech. Briefings Co-chair ISEC 2019
- Sub-reviewer: CPP 2020, IEEE S&P 2017, IEEE S&P 2016, TACAS 2016, IEEE S&P 2015, ESOP 2015, ICFP 2015, POPL 2014, CSF 2014, OOPSLA 2014, TFP 2013, NDSS 2012.
I am co-organizing the VeriCrypt : An Introduction to Tools for Verified Cryptography (opens in new tab) event as part of Indocrypt 2020 (opens in new tab).
I am co-organizing the inaugural Workshop on Research Highlights in Programming Languages (opens in new tab) (virtually) co-located with FSTTCS 2020 (opens in new tab).
I was a guest lecturer for the Principles of Programming Languages Course (Monsoon 2018) at IIIT-Hyderabad.
I gave an F* tutorial at the Winter School in Software Engineering’2017 (opens in new tab) at Pune.
I co-taught F* at the Computer-aided security proofs summer school, Aarhus in Oct. 2017 (course web page (opens in new tab), course material (opens in new tab)).
精选内容
EverParse: Hardening critical attack surfaces with formally proven message parsers
EverParse is a framework for generating provably secure parsers and formatters used to improve the security of critical code bases at Microsoft. EverParse is developed as part of Project Everest, a collaboration between Microsoft Research labs in Redmond, Washington; India;…
Project Everest: Reaching greater heights in internet communication security
Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the verification tools and techniques the Everest team is using and…