MAC, A Verified Static Information-Flow Control Library

摘要: 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 variety of advanced features like mutable data structures, exceptions, concurrency, whose subtle interaction makes verification guarantees challenging. In this work, we focus on MAC, statically-enforced library for Haskell. other libraries, computations have well-established algebraic structure (i.e., monads) responsible manipulate labeled values coming from an abstract type which associates sensitivity label piece information. enrich with functor provide applicative operator encourages more functional style simplifies code. Furthermore, present full-fledged, mechanically-verified model MAC. Specifically, show progress-insensitive noninterference our sequential calculus pinpoint sufficient requirements the scheduler prove progress-sensitive concurrent calculus. For that, study MAC using term erasure, proof technique that ensures same public output should be produced if secrets are erased before or after program execution. As another contribution, extend erasure two-steps flexible novel greatly helps many