Authenticated data structures (ADSs) allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are challenging to develop and implement correctly. In this talk, I will talk about programming frameworks that exploit some structural properties of ADSs to make the task of correctly implementing ADSs easier: (1) lambda-auth - a domain-specific extension of the OCaml programming language, that generates correct and secure ADS binaries automatically; (2) Authentikit - a library version of lambda-auth currently implemented in OCaml. I will also talk about recent work by us (https://dl.acm.org/doi/abs/10.1145/3719027.3744801) that gives a formal proof of security and correctness of Authentikit.
Short Bio:
Chaitanya Agarwal (https://culechetoo.github.io) is a 3rd year computer science PhD student at the New York University, advised by Joseph Tassarotti. He is broadly interested in programming languages and formal verification with a particular focus on verification of security applications. In the past, he has also worked with Thomas Wies on abstract-interpretation analysis for recursive, higher-order programs, and with Shibashis Guha, on developing statistical-model-checking techniques for Markov Decision Processes (MDPs). Chaitanya obtained his B.Tech. from IIIT Delhi.
