Nickel
Covert channels allow malicious applications to circumvent information flow control systems by encoding and transferring information indirectly, and they are often subtle and difficult to spot.
Nickel is a framework that helps developers systematically eliminate covert channels inherent in their system designs, through automated verification of noninterference. It allows developers to express a high-level information flow policy in Python. It extends the Hyperkernel infrastructure to verify that both an interface specification and an implementation satisfy noninterference with respect to the policy, ruling out covert channels. If verification fails, Nickel generates informative counterexamples for debugging and revising the design.
Download
Publications
-
Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Noninterference specifications for secure systems. ACM SIGOPS Operating Systems Review, 54(1), Aug 2020. [pdf]
-
Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. A note on verifying information flow control systems with Nickel. Technical Report UW-CSE-2019-10-01, University of Washington, Oct 2019. [pdf]
-
Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. Nickel: A Framework for Design and Verification of Information Flow Control Systems. In Proc. of the 13th OSDI, Oct 2018. [pdf] [slides]