Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874859 | Journal of Logical and Algebraic Methods in Programming | 2018 | 60 Pages |
Abstract
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 IFC libraries (e.g., LIO and HLIO) support a variety of advanced features like mutable data structures, exceptions, and concurrency, whose subtle interaction makes verification of security guarantees challenging. In this work, we focus on MAC, a statically-enforced IFC library for Haskell. In MAC, like other IFC libraries, computations have a well-established algebraic structure for computations (i.e., monads) responsible to manipulate labeled values-values coming from an abstract data type which associates a sensitivity label to a piece of information. In this work, we enrich labeled values with a functor structure and provide an applicative functor operator which encourages a more functional programming style and simplifies code. Furthermore, we present a full-fledged, mechanically-verified model of MAC. Specifically, we show progress-insensitive noninterference for our sequential calculus and pinpoint sufficient requirements on the scheduler to prove progress-sensitive noninterference for our concurrent calculus. For that, we study the security guarantees of MAC using term erasure, a proof technique that ensures that the same public output should be produced if secrets are erased before or after program execution. As another contribution, we extend term erasure with two-steps erasure, a flexible novel technique that greatly simplifies the noninterference proof and helps to prove many advanced features of MAC.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Marco Vassena, Alejandro Russo, Pablo Buiras, Lucas Waye,