Andrew Hirsch
November 5, 2021 at 12:00 PM on Zoom / Soda Hall
Semantic Techniques for Information-Flow Languages
Abstract: Information-flow languages enforce information-security policies for any program written in them. The most basic security policy of such languages is noninterference, which states that secret inputs do not affect the observations of an adversary. However, current practices for developing and proving correct information-flow languages rely exclusively on hand-rolled proofs, making exploration of the design space slow and labor intensive. Moreover, proofs are almost never given for implementations of information-flow languages. In this talk, I discuss how semantic techniques can alleviate some of this burden by providing general frameworks for noninterference proofs. In particular, I discuss how the semantics of effects eases the burden of proof for the source language, how denotational semantics can ease proofs of security preservation for compilers, and how modal logics can ensure that low-level security enforcement preserves noninterference.
Bio: Andrew K. Hirsch is a postdoctoral researcher at the Max Planck Institute for Software Systems in Saarbrücken, Germany. There, he works with the Foundations of Computer Security group on the foundations of decentralized programming. Previously, he earned his PhD from Cornell University in 2019.