[Pl-seminar] PL seminar schedule (note: nonstandard time)

[Aaron Turon]

NEU Programming Languages Seminar presents

Michael Clarkson
Cornell University

NOTE: **nonstandard time**
**Thursday 10/14, 3-4pm** (during PhD seminar)

Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Tea and cookies will be served.

Hyperproperties

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.  Joint work with Fred B.
Schneider.

BIO:
Michael Clarkson is a Postdoctoral Associate in the Department of
Computer Science at Cornell University in Ithaca, New York.  He
received a Ph.D. in Computer Science from Cornell in 2010. Clarkson's
research interests include computer security and programming
languages. His work focuses on using principled techniques to define
security and to construct secure systems. He is the lead creator of
the Civitas voting system.