Quantification And Formalization Of Security
Computer security policies often are stated informally in terms of conﬁdentiality, integrity, and availability of information and resources; these policies can be qualitative or quantitative. To formally quantify conﬁdentiality and integrity, a new model of quantitative information ﬂow is proposed in which information ﬂow is quantiﬁed as the change in the accuracy of an observer’s beliefs. This new model resolves anomalies present in previous quantitative informationﬂow models, which are based on change in uncertainty. And the new model is sufﬁciently 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 veriﬁcation) is proposed. Security policies are modeled as hyperproperties, which are sets of trace properties. Although important security policies, such as secure information ﬂow, 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. Veriﬁcation, reﬁnement, and topology of hyperproperties are also addressed. Hyperproperties for system representations beyond trace sets are investigated.
Dissertation or Thesis