Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of k-safety properties, i.e., propert...
详细信息
ISBN:
(纸本)9783031572487;9783031572494
Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of k-safety properties, i.e., properties that state that all k-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider for all(k)there exists(l) properties, which state that for all k executions, there exist l executions that, together, satisfy a property. This captures important non-k-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of for all(k)there exists(l) properties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called ForEx and report on encouraging experimental results.
暂无评论