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…