Flexible Manipulation of Labeled Values for Information-Flow Control Libraries
| Autor: | Alejandro Russo, Lucas Waye, Pablo Buiras, Marco Vassena |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Soundness
Theoretical computer science Algebraic structure Computer science Covert channel 020207 software engineering 0102 computer and information sciences 02 engineering and technology Information security Abstract data type Mathematical proof 01 natural sciences 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Programming paradigm Haskell computer computer.programming_language |
| Zdroj: | Computer Security – ESORICS 2016 ISBN: 9783319457437 ESORICS (1) |
| DOI: | 10.1007/978-3-319-45744-4_27 |
| Popis: | The programming language Haskell plays a unique, privileged role in Information-Flow Control (IFC) research: it is able to enforce information security via libraries. Many state-of-the-art libraries (e.g., LIO, HLIO, and MAC) allow computations to manipulate data with different security labels by introducing the notion of labeled values, which protect values with explicit labels by means of an abstract data type. While computations have an underlying algebraic structure in such libraries (i.e. monads), there is no research on structures for labeled values and their impact on the programming model. In this paper, we add the functor structure to labeled values, which allows programmers to conveniently and securely perform computations without side-effects on such values, and an applicative operator, which extends this feature to work on multiple labeled values combined by a multi-parameter function. This functionality simplifies code, as it does not force programmers to spawn threads to manipulate sensitive data with side-effect free operations. Additionally, we present a relabel primitive which securely modifies the label of labeled values. This operation also helps to simplify code when aggregating data with heterogeneous labels, as it does not require spawning threads to do so. We provide mechanized proofs of the soundness our contributions for the security library MAC, although we remark that our ideas apply to LIO and HLIO as well. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|