I am an assistant professor in the Department of Computer Science at the Rochester Institute of Technology. I work on making software more secure and reliable using techniques based on formal verification, programming languages and type systems.
Short bio: I pursued my Ph.D. studies at the University of Pennsylvania, under the supervision of Benjamin Pierce and co-advised by Cătălin Hrițcu. After my Ph.D., I held postdoctoral appointments at Boston University and at Carnegie Mellon. As an undergraduate student, I majored in computer science and engineering at Unicamp and Polytechnique. I am one of the authors of Software Foundations, an introductory textbook to the Coq proof assistant, and write about Coq in my blog.
Email: arthur.aa@gmail.com
Office: GOL-3547
Current research
Cryptographic protocols
Cryptographic protocols such as TLS are crucial for securing communication over the Internet. Unfortunately, their design is tricky to get right, which often results in devastating attacks. We are currently developing a formalism that leverages recent advances in program verification (in particular, separation logic) to verify cryptographic protocols. These verified protocols can be combined with standard proofs of correctness to derive application-level specifications. For more information, check out our draft and accompanying Coq formalization.
Compartmentalization
Low-level languages such as C and C++ are often seen as the gold standard for fast systems code, but their unsafe semantics often leads to simple bugs turning into critical vulnerabilities. Compartmentalization refers to a series of techniques for limiting the scope of such vulnerabilities, often leveraging process-based isolation, code instrumentation, or specialized hardware. We have been analyzing the formal guarantees of such compartmentalization techniques, and have applied them to develop SECOMP, the first formally verified realistic compartmentalizing compiler. If you want to learn more, check out our paper, available here.
News
March 2025 Our draft Cryptis: Cryptographic Reasoning in Separation Logic is out. The accompanying Coq formalization is available here.
January 2024 Our draft SECOMP: Formally Secure Compilation of Compartmentalized C Programs is out.
Our paper Pipelines and Beyond: Graph Types for ADTs with Futures appeared at POPL 2024 (available here).
January 2023 I have started as assistant professor at RIT.
Teaching
Spring 2024: CSCI 344 01 (RIT): Programming Language Concepts
Fall 2023: CSCI 740 (RIT): Programming Language Theory
Spring 2023: CSCI 344 01 (RIT): Programming Language Concepts
Spring 2022: CS 599 G1 (BU): Formal Proofs about Programs
Recent Publications
Full list here. Check also my DBLP and Google Scholar pages.
Kleene Algebra with Commutativity Conditions Is Undecidable. With Cheng Zhang and Marco Gaboardi. CSL 2025. [ DOI | arxiv | http ]
SECOMP: Formally Secure Compilation of Compartmentalized C Programs. With Jérémy Thibault, Roberto Blanco, et al. CCS 2024. [ DOI | GitHub | arxiv | http ]
Domain Reasoning in TopKAT. With Cheng Zhang and Marco Gaboardi. ICALP 2024. [ DOI | arxiv | http ]
Pipelines and Beyond: Graph Types for ADTs with Futures. With Francis Rinaldi, june wunder, et al. POPL 2024. [ DOI | arxiv | http ]
Bunched Fuzz: Sensitivity for Vector Metrics. With june wunder, Patrick Baillot, et al. ESOP 2023. [ DOI | arxiv | http ]
On incorrectness logic and Kleene algebra with top and tests. With Cheng Zhang and Marco Gaboardi. POPL 2022. [ DOI | arxiv | http ]
Students
I am fortunate to be currently advising the following amazing students at RIT:
- Dongyu Wu (PhD)
- Chandradeep Dey (PhD)
- Melwyn Saldanha (MS)
- Eloise Christian (MS)
- Tejas Gadwalkar (BS)
Besides official advising duties, I have also mentored and worked with many other students in various capacities. Here are some of them:
- Cheng Zheng (BU, PhD; currently a postdoc at UCL)
- june wunder (BU, PhD)
- Vivien Rindisbacher (BU, BS; currently a PhD student at UCSD)
Software
Cryptis: An extension of the Iris separation logic for verifying cryptographic protocols.
Deriving: A Coq library for automating the definition of class instances for inductive types.
Extensional Structures: A Coq library of finite data structures that support extensional equality.
Micro-policies: A programming model for tag-based security policies formalized in Coq.
Coq utils: A small library of Coq utilities, including a formalization of nominal sets.
Netter: A language for modeling and verifying probabilistic, stateful networks.
Taglierino: A bounded model checker for cryptographic protocols.