Assistant Professor, Computer Science
George Washington University
(Video runs from 00:03:38 to 01:13:26)
Security policies on computer systems are usually expressed in terms of confidentiality, integrity, and availability. Unfortunately, no complete technique is known for formalizing and verifying such security policies. This talk proposes expressing security policies in terms of hyperproperties, a new mathematical framework based on sets of sets of traces. Hyperproperties are expressive enough for handling information flow, service guarantees, and a host of other security policies that have been problematic for the frameworks currently in use. Hyperproperties yield insight into the structure of security policies: every hyperproperty is the intersection of a safety hyperproperty and a liveness hyperproperty, where a safety hyperproperty proscribes bad system behaviors, and a liveness hyperproperty prescribes good system behaviors; and safety and liveness correspond to fundamental definitions of structures in mathematical topology. A class of hyperproperties (namely, safety hyperproperties whose bad behaviors can be finitely bounded) enjoys a relatively complete verification technique. A temporal logic, HyperLTL, can express many hyperproperties, and it also has a decidable model-checking algorithm.
Michael Clarkson is an assistant professor in the Department of Computer Science at George Washington University in Washington, DC. His work focuses on using principled techniques to define security and to construct secure systems. He received a Ph.D. in computer science from Cornell University in 2010.