CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Flexible manipulation of labeled values for information-flow control libraries

Marco Vassena (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Pablo Buiras (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; L. Waye ; Alejandro Russo (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science. 21st European Symposium on Research in Computer Security, ESORICS 2016, Heraklion, Greece, 26-30 September 2016 (0302-9743). Vol. 9878 LNCS, 2016 (2016), p. 538-557.
[Konferensbidrag, refereegranskat]

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.

Denna post skapades 2016-11-02. Senast ändrad 2016-12-14.
CPL Pubid: 244666


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)


Data- och informationsvetenskap

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:

MAC, A Verified Information-Flow Control Library