Linked Presentation: Nickel: A Framework for Design and Verification of Information Flow Control Systems