Secure multi-execution in Haskell

Abstract. Language-based information-flow security has emerged as a promis-ing technology to guarantee confidentiality in on-line systems, where enforce-ment mechanisms are typically presented as run-time monitors, code transfor-mations, or type-systems. Recently, an alternative technique, called secure multi-execution, has been proposed. The main idea behind this novel approach consists on running a program multiple times, once for each security level, using special rules for I/O operations. Compared to run-time monitors and type-systems, se-cure multi-execution does not require to inspect the full code of the application (only its I/O actions). In this paper, we propose the core of a library to provide non-interference through secure-multi execution. We present the code of the li-brary as well as a running example for Haskell. To the best of our knowledge, this paper is the first work to consider secure-multi execution in a functional setting and provide this technology as a library.