Research

My research focuses on the design, implementation, and verification of secure programming languages. In the past, I have worked on abstract interpretation for quantitative information flow [2, 5] and mechanization (in Coq) of the metatheory for Checked C, an extension of C with spatial memory safety via typing [4]. Most recently, I worked on the design and implementation of a language, λ-Obliv, with a type system which enforces probabilistic memory trace obliviousness (PMTO) [3, 1]. PMTO is a property which guarantees that well-typed programs do not leak any secret data. It extends the classic noninterference property by (1) considering the timing and memory-trace side channels to be observable (MTO) and (2) including an expression for probabilistic choice (P).

I am currently working on integrating the type system of λ-Obliv into λ-Symphony, a state of the art programming language for Secure Multiparty Computation (MPC). This will allow λ-Symphony to support MPC computations in the RAM model using the fastest available Oblivious RAM (ORAM) constructions. For more details on ORAM and its usefulness, you can check out the classic paper by Goldreich and Ostrovsky or the case studies in our POPL paper.

Publications

[1] Short Paper: Probabilistically Almost-Oblivious Computation. Ian Sweet, David Darais, and Michael Hicks. In Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), November 2020.

[2] Probabilistic Abstract Interpretation: Sound Inference and Application to Privacy. Jose Manuel Calderón Trilla, Michael Hicks, Stephen Magill, Piotr Mardziel, and Ian Sweet. In Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva, editors, Foundations of Probabilistic Programming, chapter 15, pages 401-432. Cambridge University Press, 2020.

[3] A Language for Probabilistically Oblivious Computation. David Darais, Ian Sweet, Chang Liu, and Michael Hicks. In Proceedings of the ACM Conference on Principles of Programming Languages (POPL), January 2020.

[4] Achieving Safety Incrementally with Checked C. Andrew Ruef, Leonidas Lampropoulos, Ian Sweet, David Tarditi, and Michael Hicks. In Proceedings of the Symposium on Principles of Security and Trust (POST), April 2019.

[5] What’s the Over/Under? Probabilistic Bounds on Information Leakage. Ian Sweet, José Manuel Calderón Trilla, Chad Scherrer, Michael Hicks, and Stephen Magill. In Proceedings of the Symposium on Principles of Security and Trust (POST), April 2018.