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.