TL;DR
This paper demonstrates how modern random testing techniques, especially QuickCheck, can efficiently identify counterexamples and guide the design of complex information-flow control mechanisms, improving correctness verification.
Contribution
It introduces a novel application of QuickCheck for testing complex information-flow abstract machines, including a flow-sensitive enforcement mechanism, and presents effective methods for bug detection and counterexample shrinking.
Findings
Successfully identified over 45 bugs using random testing.
Effective counterexample shrinking simplifies bug analysis.
Testing guided the discovery of invariants for noninterference proof.
Abstract
Information-flow control mechanisms are difficult both to design and to prove correct. To reduce the time wasted on doomed proof attempts due to broken definitions, we advocate modern random testing techniques for finding counterexamples during the design process. We show how to use QuickCheck, a property-based random-testing tool, to guide the design of increasingly complex information-flow abstract machines, leading up to a sophisticated register machine with a novel and highly permissive flow-sensitive dynamic enforcement mechanism that is sound in the presence of first-class public labels. We find that both sophisticated strategies for generating well-distributed random programs and readily falsifiable formulations of noninterference properties are critically important for efficient testing. We propose several approaches and evaluate their effectiveness on a collection of injected…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
