Hyperproperties

dc.contributor.author	Clarkson, Michael R.
dc.contributor.author	Schneider, Fred B.
dc.date.accessioned	2008-12-22T17:13:54Z
dc.date.available	2008-12-22T17:13:54Z
dc.date.issued	2008-12-22T17:13:54Z
dc.description.abstract	Properties, which have long been used for reasoning about systems, are sets of traces. Hyperproperties, introduced here, are sets of properties. Hyperproperties can express security policies, such as secure information flow and service level agreements, that properties cannot. Safety and liveness are generalized to hyperproperties, and every hyperproperty is shown to be the intersection of a safety hyperproperty and a liveness hyperproperty. A verification technique for safety hyperproperties is given and is shown to generalize prior techniques for verifying secure information flow. Refinement is shown to be applicable with safety hyperproperties. A topological characterization of hyperproperties is given.	en_US
dc.identifier.uri	https://hdl.handle.net/1813/11660
dc.subject	security policies	en_US
dc.subject	safety and liveness	en_US
dc.title	Hyperproperties	en_US

Files

Now showing 1 - 1 of 1