A. Gollamudi and S. Chong, “Expressive Authorization Policies using Computation Principals,” in Workshop on Foundations of Computer Security, 2021, 2021.Abstract

In authorization logics, it is natural to treat computations as principals, since systems need to decide how much authority to give computations when they execute. But unlike other kinds of principals, the authority that we want to give to computations might be based on properties of the computation itself, such as whether the computation is differentially private, or whether the computation is memory safe.

Existing authorization logics do not treat computation principals specially. Instead, they identify computation principals using a brittle hash-based naming scheme: minor changes to the code produce a distinct principal, even if the new computation is equivalent to the original one. Moreover, existing authorization logics typically treat computation principals as “black boxes,” leaving any reasoning about the structure, semantics, or other properties of the computation out of the logic.

We introduce Coal, a novel programming-language calculus that embeds an authorization logic in its type system via the Curry-Howard isomorphism. A key innovation of Coal is computation principals: computations that can be treated like other principals but also allow reasoning about the computation itself. Critically, Coal allows equivalent computations to be treated as equivalent principals, avoiding the brittleness of identity-based approaches to computation principals. Coal enables us to cleanly express fine-grained access control policies that are dependent on the structure and semantics of computations, such as expressing trust in all computations that are analyzed to be differentially private by any program analyzer that has been verified correct.

ibmplday2019.pdf coal-fcs.pdf
O. Arden, A. Gollamudi, E. Cecchetti, S. Chong, and A. C. Myers, “A Calculus for Flow-Limited Authorization,” arXiv:2104.10379, 2021. Publisher's VersionAbstract
This work supersedes the earlier publication "A Calculus for Flow-limited Authorization", Computer Security Foundations 2016. It not only fixes significant technical errors but also generalizes the theoretical results from the previous publication.
A. Gollamudi, S. Chong, and O. Arden, Information Flow Control for Distributed Trusted Execution Environments. Harvard University, 2019. Technical Report
A. Gollamudi, S. Chong, and O. Arden, “Information Flow Control for Distributed Trusted Execution Environments,” 32nd IEEE Computer Security Foundations Symposium. 2019. Publisher's Version
P. Kraft, A. Waterland, D. Y. Fu, A. Gollamudi, S. Szulanski, and M. Seltzer, “Automatic Parallelization of Sequential Programs,” arXiv:1809.07684, 2018. arXiv:1809.07684
A. Gollamudi and C. Fournet, “(Extended Abstract) Building Secure SGX Enclaves using F*, C++ and X64,” in Principles of Secure Compilation, PRISC, LA, 2018. Publisher's Version pdf
A. Gollamudi and S. Chong, “Automatic Enforcement of Expressive Security Policies using Enclaves,” Proceedings of the 29th Annual ACM SIGPLAN Conference on Object-Oriented Programming Languages, Systems, Languages, and Applications (OOPSLA). 2016. Publisher's Version
K. Bhargavan, et al., “Formal Verification of Smart Contracts,” in Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, 2016. Publisher's Version pdf