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

Authors: 

Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang, University of Washington

Abstract: 

Nickel is a framework that helps developers design and verify information flow control systems by systematically eliminating covert channels inherent in the interface, which can be exploited to circumvent the enforcement of information flow policies. Nickel provides a formulation of noninterference amenable to automated verification, allowing developers to specify an intended policy of permitted information flows. It invokes the Z3 SMT solver to verify that both an interface specification and an implementation satisfy noninterference with respect to the policy; if verification fails, it generates counterexamples to illustrate covert channels that cause the violation.

Using Nickel, we have designed, implemented, and verified NiStar, the first OS kernel for decentralized information flow control that provides (1) a precise specification for its interface, (2) a formal proof that the interface specification is free of covert channels, and (3) a formal proof that the implementation preserves noninterference. We have also applied Nickel to verify isolation in a small OS kernel, NiKOS, and reproduce known covert channels in the ARINC 653 avionics standard. Our experience shows that Nickel is effective in identifying and ruling out covert channels, and that it can verify noninterference for systems with a low proof burden.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {222549,
author = {Helgi Sigurbjarnarson and Luke Nelson and Bruno Castro-Karney and James Bornholt and Emina Torlak and Xi Wang},
title = {Nickel: A Framework for Design and Verification of Information Flow Control Systems},
booktitle = {13th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 18)},
year = {2018},
isbn = {978-1-931971-47-8},
address = {Carlsbad, CA},
pages = {287--305},
url = {https://www.usenix.org/conference/osdi18/presentation/sigurbjarnarson},
publisher = {{USENIX} Association},
}