Secure Multi-Execution in Haskell
with Alejandro Russo. PSI 2011.PDF
Abstract
Language-based information-flow security has emerged as a promising technology to guarantee confidentiality in on-line systems, where enforcement mechanisms are typically presented as run-time monitors, code transformations, 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, secure 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 library 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.
BibTeX
@inproceedings{JaskeRusso:PSI:2011,
title = {Secure Multi-Execution in Haskell},
address = {Akademgorodok, Novosibirsk, Russia},
author = {Mauro Jaskelioff and Alejandro Russo},
booktitle = {Proceedings of Andrei Ershov International Conference on Perspectives of System Informatics (PSI'11)},
editor = {Edmund M. Clarke and Irina Virbitskaite and Andrei Voronkov},
pages = {170--178},
url = {http://dx.doi.org/10.1007/978-3-642-29709-0_16},
doi = {10.1007/978-3-642-29709-0_16},
isbn = {978-3-642-29708-3},
series = {Lecture Notes in Computer Science},
volume = {7162},
publisher = {Springer},
year = {2011}
}