Research Interests
My current research falls under the intersection of formal verification, mathematics, machine learning and cryptography.
Broad Research Areas
- Number Theory
- Formal Methods
- Cryptography.
Work Experience
Advisor: Joseph Tassarotti
- Formally verifying the robustness of cryptography and machine learning models.
Advisor: Alley Stoughton
- During the internship, I developed a testsuite for maintaining ucDSL. This involves developing a test description language (using Menhir) that automatically executes the corresponding test and generates an elaborate report. Part of the challenge is in supporting extensive exception/error handling. Future work includes translating ucDSL programs into EasyCrypt’s procedural programming language and proving that the translation is semantically preserving. The project also involved writing formal proofs in EasyCrypt proof assistant.
Advisor: Joel Bellaiche
- My primary area of research is Eigen varieties and p-adic L-functions.
- My dissertation focuses on investigating the behaviour of L_b ideal without knowing the modules of overconvergent modular symbols M+ and M- at p irregular cuspidal CM modular forms of weight 1 and level N.
- Courses Taught (as an independent instructor)
- Applied Linear algebra (Fall 2020)
- 2nd-semester calculus (Fall 2016, Fall 2017, Spring 2020)
- 1st-semester calculus (Spring 2017, Fall 2015)
- Courses Designed
- Applied Linear Algebra Practicum at Brandeis University (with Prof. John Wilmes and others)
- Mathematics of Cryptography. This course introducesthe mathematics of public key cryptosystems with an emphasis on Elliptic Curve Cryptography
Current Projects
Mechanized Certified Adversarial Robustness (Working Paper)
- We present a complete mechanized proof of the robustness guarantee of classifiers by Cohen et al. The proof has been developed in Coq. Since the original proof relies on inverse CDF of the standard Gaussian distribution and any implementation of the Gaussian distributions involves some way of rounding a real number to the nearest floating point which may introduce rounding errors. These rounding errors can be significant enough that implementation of the classifier may not carry the theoretical robustness. The challenge here is to extend robustness guarantees to the implementation. Our approach relies on two key insights: first, relying on a formally verified external sampler and second, modeling the robustness result using discrete Gaussian distribution. We are exploring both directions. Joint work with Joseph Tassarotti.
Certified Gaussian Samplers
- Formally verifying the correctness of Gaussian samplers that approximate samples to that rounded Gaussians.
Verified MCMC
- Formally verifying the convergence of Markov chain Monte Carlo (MCMC) theorem in discrete and n-dimensional reals.
Publications
PhD Thesis (2021)