Quantification and Formalization of Security
Abstract
Computer security policies often are stated informally in terms of confidentiality, integrity, and availability of information and resources; these policies can be qualitative or quantitative. To formally quantify confidentiality and integrity, anew model of quantitative information flow is proposed in which information flow is quantified as the change in the accuracy of an observers beliefs. This new model resolves anomalies present in previous quantitative information flow models, which are based on change in uncertainty. And the new model is sufficiently general that it can be instantiated to measure either accuracy or uncertainty. To formalize security policies in general, a generalization of the theory of trace properties (originally developed for program verification) is proposed. Security policies are modeled as hyperproperties, which are sets of trace properties. Although important security policies, such as secure information flow, cannot be expressed as trace properties, they can be expressed as hyperproperties. Safety and liveness are generalized from trace properties to hyperproperties, and every hyperproperty is shown to be the intersection of a safety hyperproperty and a liveness hyperproperty. Verification, refinement, and topology of hyperproperties are also addressed. Hyperproperties for system representations beyond trace sets are investigated.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 2010
- Accession Number
- AD1000328
Entities
People
- Michael R. Clarkson
Organizations
- Cornell University