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.



Coming soon.