FMitF: Track II: Enhancing the Bounded Model Checking Tool for Hyperproperties (HyperQB) for Industrial Applications

Many crucial requirements in computing systems such as security and privacy are properties of multiple behaviors of the system. While many tools have been developed to ensure the correctness of systems with respect to single executions in the past few decades, there is currently no tool support for ensuring the correctness of policies such as privacy. This project’s novelty is a state-of-the-art tool, called HyperQB, that will be able to mathematically prove the correctness of systems with respect to security and privacy policies. The tool will be robust, reliable, user-friendly, push-button, and open-source beyond an academic artifact while facilitating broader adoption and expanding its user base. The outcome of the project – the tool HyperQB – will take as input a family of models in popular modeling languages and a hyperproperty and produces as output a verdict on whether the models satisfy the hyperproperty. The project will deliver two sets of results. The first set will focus on significantly boosting the performance of HyperQB verification engine through a variety of methods. This includes incorporating (1) highly expressive semantics of hyperproperties; (2) enhancing its completeness; (3) compact representation of state space unrolling; (4) efficient implementation in Rust, and (5) interfacing with state-of-the-art solvers for quantified Boolean formulas. The second set will focus on substantially improving the front-end of the tool by providing (1) parsers for popular modeling languages; (2) an interface for third-party developers, and (3) user interfaces for standalone and web-based deployments. The project will rigorously evaluate the outcomes by a major expansion of benchmark suites by case studies from fields of information-flow security and concurrent data structures as well as detailed comparison and contrast with other existing tools. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.