Security Policy: Logic and Engineering

Yuri Gurevich, Microsoft Research

Abstract:

In software industry many engineers do formal logic even though they
may not realize that. Security policy is one of those fields where
engineers do logic. The security policy of a large organization may
consist of great many rules. You want to throw in a few more
rules. Are you sure that they do not contradict the current policy? Do
you know whether the current policy is consistent? Is the meaning of
the rules well defined? Are there unintended ambiguities? Is your
policy in compliance with government regulations? Are those
regulations consistent? A typical current solution for the compliance
problem is to hire consultants which is expensive and does not scale.

A few logic-based languages arose to deal with these problems. As a
rule they presume a central logic engine. Our policy language, called
DKAL, goes beyond that. It formalizes not only logic but also
communication which facilitates reasoning about interacting
policies. A year ago we presented DKAL at TAU. In the meantime we
developed a new incarnation of the language, called Evidential DKAL,
where information x is communicated together with a proof of x. The
present lecture does not presume that the audience remembers the
last-year lecture; we will start from scratch. But the emphasis will
be on the Evidential DKAL.

Bio:

Yuri Gurevich is Principal Researcher at Microsoft. He is also
Prof. Emeritus at the University of Michigan, ACM Fellow, Guggenheim
Fellow, a member of Academia Europaea, and Dr. Honoris Causa of a
Belgian and Russian universities.