Seminars
View all Seminars | Download ICal for this eventVerified Programming Frameworks for Authenticated Data Structures
Series: Department Seminar
Speaker: Chaitanya Agarwal
Date/Time: Jan 09 11:30:00
Location: CSA Seminar Hall (Room No. 254, First Floor)
Abstract:
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 (Link that gives a formal proof of security and correctness of Authentikit.
Speaker 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.
Host Faculty: K. V. Raghavan