Detecting noninterference violations with property-based testing

Abstract

In today’s interconnected digital world, protecting sensitive data is critical. However, the design and verification of information-flow control (IFC) mechanisms, crucial for data security, present significant challenges. In this work, we propose the integration of property-based testing into the verification process of IFC mechanisms, utilizing the existing metatheory as a foundation.

Property-based testing can streamline the formal verification of information-flow control mechanisms by generating random test cases. This approach can expose errors early in the proving process, guiding users toward accurate design and implementation. By generating counterexamples, property-based testing can effectively uncover potential noninterference violations.

We illustrate the effectiveness of this approach by applying it to the DypLIO library, a Haskell-based IFC mechanism designed to enforce security policies. This application successfully identified issues in both the implementation and the ongoing proof mechanization. Our results highlight the potential of propertybased testing as a complementary strategy for enhancing the security of IFC mechanisms.