Catch me if you can: Permissive yet secure error handling. Technical Report. Available at http://www.cs.cornell.edu/~aslan/ exceptions-tr.pdf

Program errors are a source of information leaks. Track-ing these leaks is hard because error propagation breaks out of program structure. Programming languages often fea-ture exception constructs to provide some structure to error handling: for example, the try...catch blocks in Java and Caml. Mainstream information-flow security compilers such as Jif and FlowCaml enforce rigid rules for exceptions in or-der to prevent leaks via public side effects of computation whose reachability depends on exceptions. This paper presents a general and permissive alternative to the rigid solution: the programmer is offered a choice for each type of error/exception whether to handle it or not. The security mechanism ensures that, in the former case, it is never handled and, in the latter case, it is always handled with the mainstream restrictions. This mechanism extends naturally to a language with procedures and output, where we show the soundness of the mechanism with respect to termination-insensitive noninterference