Arthur

Azevedo de Amorim

I work on making software more secure and reliable using techniques based on formal verification, programming languages and type systems. Currently, I am a postdoc at Boston University working under the supervision of Marco Gaboardi. Before joining BU, I held a postdoc appointment at Carnegie Mellon, where I worked with Limin Jia, Matt Fredrikson and Anupam Datta.

In January 2023, I will be starting as an assistant professor at RIT. I am looking for students to join our Ph.D. program in the 2023/2024 academic year. If you are interested, drop me a line!

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. 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.

E-mail: arthur.aa@gmail.com

News

February 2022 I am serving on the program committee of MFPS 2022.

November 2021 I am serving on the program committee of ICFP 2022. I am also serving as one of the ICFP Workshop co-chairs, along with Zoe Paraskevopoulou.

I am serving on the program committee of WoLLIC 2022.

September 2021 Our paper On Incorrectness Logic and Kleene Algebra with Top and Tests was selected to appear at POPL 2022 (arxiv).

July 2021 Our draft Cryptis: Composition and Separation in Cryptographic Protocols is out.

I am serving on the program committee of PriSC 2022.

November 2020 Our paper Netter: Probabilistic, Stateful Network Models was accepted at VMCAI 2021.

I am serving on the CoqPL 2021 program committee.

July 2020 Our short paper Automating Compositional Analysis of Authentication Protocols was accepted at FMCAD 2020.

April 2020 Our paper Reconciling Noninterference and Gradual Typing was accepted at LICS 2020.

I am serving on the program committees of the Haskell Symposium 2020 and of CPP 2021.

March 2020 I am serving on the artifact evaluation committee for PLDI 2020.

Teaching

CS 599 G1 (BU): Formal Proofs about Programs

Publications

Check also my DBLP and Google Scholar pages.

On incorrectness logic and Kleene algebra with top and tests. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Proc. ACM Program. Lang., 6(POPL):1--30, 2022. [ DOI | arxiv | http ]

Learning Assumptions for Verifying Cryptographic Protocols Compositionally. Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, and Corina S. Pasareanu. In Gwen Salaün and Anton Wijs, editors, Formal Aspects of Component Software - 17th International Conference, FACS 2021, Virtual Event, October 28-29, 2021, Proceedings, volume 13077 of Lecture Notes in Computer Science, pages 3--23. Springer, 2021. [ DOI | http ]

Netter: Probabilistic, Stateful Network Models. Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, and Limin Jia. In Fritz Henglein, Sharon Shoham, and Yakir Vizel, editors, Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, volume 12597 of Lecture Notes in Computer Science, pages 486--508. Springer, 2021. [ DOI | .pdf ]

Automating Compositional Analysis of Authentication Protocols. Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, and Corina S. Pasareanu. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 113--118. IEEE, 2020. [ DOI | .pdf ]

Reconciling noninterference and gradual typing. Arthur Azevedo de Amorim, Matt Fredrikson, and Limin Jia. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 116--129. ACM, 2020. [ DOI | .pdf ]

Probabilistic Relational Reasoning via Metrics. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1--19, 2019. [ DOI | arxiv | http ]

When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hrițcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, and Andrew Tolmach. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 1351--1368, 2018. [ DOI | arxiv | http ]

The Meaning of Memory Safety. Arthur Azevedo de Amorim, Cătălin Hrițcu, and Benjamin C. Pierce. In Proceedings of POST 2018, part of ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, pages 79--105, 2018. [ http ]

A methodology for micro-policies. Arthur Azevedo de Amorim. PhD thesis, University of Pennsylvania, 2017. [ .pdf ]

A semantic account of metric preservation. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 545--556, 2017. [ arxiv ]

Binding Operators for Nominal Sets. Arthur Azevedo de Amorim. Electr. Notes Theor. Comput. Sci., 325:3--27, 2016. [ http ]

A verified information-flow architecture. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hrițcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. Journal of Computer Security, 24(6):689--734, 2016. [ DOI | arxiv ]

Testing noninterference, quickly. Cătălin Hrițcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, and Dimitrios Vytiniotis. J. Funct. Program., 26:e4, 2016. [ DOI | arxiv ]

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. Yannis Juglaret, Cătălin Hrițcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. In IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016, pages 45--60, 2016. [ DOI | arxiv ]

Micro-Policies: Formally Verified, Tag-Based Security Monitors. Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hrițcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015, pages 813--830, 2015. [ DOI | slides | full version ]

Really Natural Linear Indexed Type Checking. Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. In Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages, IFL '14, Boston, MA, USA, October 1-3, 2014, pages 5:1--5:12, 2014. [ DOI | arxiv ]

A verified information-flow architecture. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hrițcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 165--178, 2014. [ DOI | slides ]

Testing noninterference, quickly. Cătălin Hrițcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 455--468, 2013. [ DOI ]

Software

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.