Skip to main content


eCommons@Cornell >
Cornell University Graduate School >
Cornell Theses and Dissertations >

Please use this identifier to cite or link to this item:
Title: Quantification And Formalization Of Security
Authors: Clarkson, Michael
Issue Date: 9-Apr-2010
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, a new model of quantitative information flow is proposed in which information flow is quantified as the change in the accuracy of an observer’s beliefs. This new model resolves anomalies present in previous quantitative informationflow 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.
Appears in Collections:Cornell Theses and Dissertations

Files in This Item:

File Description SizeFormat
Clarkson, Michael.pdf833.59 kBAdobe PDFView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us