Retrofitting Impure Languages with Static Information-Flow Control

Abstract

How can we write secure programs in a pervasively effectful language? In a “pure” language, such as Haskell, effects performed by a program are recorded explicitly in its type. Thus, a function of type Int -> Int is just that: a function that receives an integer and returns an integer. It does not perform side effects such as writing to or reading from a channel. In an impure language, such as ML, however, a function of type Int -> Int may read, write, or even order a burrito. It’s impossible to assert that a function is secure from its type alone, since it may be performing invisible side effects that may leak a secret. For this reason, standard approaches to enforcing static Information-Flow Control (IFC)—be it fine-grained or coarse-grained—are not readily applicable to impure languages since they require a complete reimplementation of the compiler and significant ingenuity from the programmer to restructure programs to conform to the new enforcement paradigm. So should we all just switch to Haskell? While I would never discourage anybody from doing that, this talk is about developing the foundations for retrofitting impure languages with static IFC at a much lower cost. In a recent result, Choudhury and Krishnaswami [1] show how purity can be recovered in an impure language by using capabilities and a special “modal” type operator. In this informal talk, I’ll show how their observations, in combination with recent advances in formulating modal types, pave the way towards the goal of this work.

Date
Dec 3, 2021 1:15 PM — 2:15 PM
Event