Security Seminar: Semantic Techniques for Information-Flow Languages with Andrew Hirsch, Friday Nov. 5th, 12 PM PDT

November 5, 2021

Title: Semantic Techniques for Information-Flow Languages
Speaker: Andrew Hirsch
Time: Friday Nov 5 at 12PM
Zoom link: https://berkeley.zoom.us/j/92366857619?pwd=b1E5UFJRS3JKTnZSK3VMNG9WZW1aQT09
In-person location: Soda 465H

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.