Model checking quantitative hyperproperties
From MaRDI portal
Abstract: Hyperproperties are properties of sets of computation traces. In this paper, we study quantitative hyperproperties, which we define as hyperproperties that express a bound on the number of traces that may appear in a certain relation. For example, quantitative non-interference limits the amount of information about certain secret inputs that is leaked through the observable outputs of a system. Quantitative non-interference thus bounds the number of traces that have the same observable input but different observable output. We study quantitative hyperproperties in the setting of HyperLTL, a temporal logic for hyperproperties. We show that, while quantitative hyperproperties can be expressed in HyperLTL, the running time of the HyperLTL model checking algorithm is, depending on the type of property, exponential or even doubly exponential in the quantitative bound. We improve this complexity with a new model checking algorithm based on model-counting. The new algorithm needs only logarithmic space in the bound and therefore improves, depending on the property, exponentially or even doubly exponentially over the model checking algorithm of HyperLTL. In the worst case, the new algorithm needs polynomial space in the size of the system. Our Max#Sat-based prototype implementation demonstrates, however, that the counting approach is viable on systems with nontrivial quantitative information flow requirements such as a passcode checker.
Recommendations
- Bounded model checking for hyperproperties
- Model checking algorithms for hyperproperties (invited paper)
- Compositional and quantitative model checking (extended abstract)
- Model checking hyperproperties for Markov decision processes
- Model Checking Quantified Computation Tree Logic
- Quantitative Model Checking Revisited: Neither Decidable Nor Approximable
- Quantitative model checking of linear-time properties based on generalized possibility measures
- Bounded model checking for asynchronous hyperproperties
- Theory and Applications of Satisfiability Testing
- Efficient loop conditions for bounded model checking hyperproperties
Cited in
(23)- Timed hyperproperties
- Model checking hyperproperties for Markov decision processes
- Program Repair for Hyperproperties
- Model checking algorithms for hyperproperties (invited paper)
- Verification of quantitative hyperproperties using trace enumeration relations
- Temporal hyperproperties
- Algorithms for model checking HyperLTL and HyperCTL^*
- Monitoring hyperproperties
- Compositional model checking for multi-properties
- Bounded model checking for hyperproperties
- Efficient loop conditions for bounded model checking hyperproperties
- Parameter synthesis for probabilistic hyperproperties
- Explaining Hyperproperty Violations
- Runtime enforcement of hyperproperties
- On satisficing in quantitative games
- Synthesis from hyperproperties
- Quantitative information flow as safety and liveness hyperproperties
- Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals
- Deciding hyperproperties combined with functional specifications
- Quantitative information flow as safety and liveness hyperproperties
- Concurrent hyperproperties
- Searching for ribbon-shaped paths in fair transition systems
- Quantitative model checking of linear-time properties based on generalized possibility measures
This page was built for publication: Model checking quantitative hyperproperties
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6045002)
