prev Week 4 of 16 next
Jesus, what a week. The major work-related event was that I gave a talk at our research group's weekly seminar this past Thursday. The goal was to introduce the audience to the general topic that encompasses my summer research: applying formal logic to authorization. I went over some terminology, basic security concepts and challenges and then explained two logical approaches to authorization. [Slides]
The first, described in a 1993 paper by Abadi, Burrows, Lampson and Plotkin, is essentially a calculus for reasoning about relationships between principals. Recall, a principal is an entity that performs actions/operations/requests. A principal might represent a human user, a cryptographic key, or a bunny rabbit, say. The resulting logic has connectives that describe group membership, delegation, and much more. The paper also defines the very important and often-used "says" operator. You may have noticed it in some of the typing rules I posted on here in the past. I never really explained what it means, sorry. Suppose A is a principal and r is a request to read a file. A might represent me, logged into a workstation. If I want to read a file, the mechanism on the system that's in charge of the granting/refusing access makes a decision based on information available on the system (say in an access control list) as well as information "attached" to A (my user account/identity). So in an authorization logic, "A says r" basically means "r is true given information attached to A, and given general information available to the entity making the access control decision". The "says" operator expresses r relative to A. The idea of such an operator is pervasive in the work published on logic in access control so far, although the operator isn't necessarily called "says". Anyway, this logic from 1993 is able to express information contained in access control lists, such as "Maja may access file x", and so forth.
The other approach I described in the presentation is a constructive authorization logic (Garg,Pfenning 2006). The authors present a a logic, along with a sequent calculus, and use it to write security policies and make access control decisions based on policy rules. The logic is constructive, so access control decisions correspond to proof objects (or derivations): there is an explicit use of evidence. Incidentally, this approach also uses the "says" operator, but in contrast to the approach described above, does not define any connectives that express relationships between principals. The authors use a very high level of abstraction and thus, the principals in their calculus may be regarded simply as names for just about anything. The really cool thing about this particular authorization logic is that it was designed with a clean meta-theory in mind. The authors are thus able to prove some nice properties about the logic. This is quite important since understanding the properties of the authorization logic gives us a better understanding of the behaviour of security policies expressed in this logic. The most important property is that of being able to formally verify non-interference in any given access policy. This means that there is a way to prove that, for instance, a principal A cannot, under any circumstances, affect statements made by some other principal B. If such a result holds, then for example, if B has the authority to decide who can read file x, there's no way for A to manipulate B's statements so that A has access to file x. A will receive access to file x only if B explicitly states (in its policy) that A has access to x.
The project Brigitte and I are working on is a little different: we want to incorporate a suitable authorization logic into the type system of a functional programming language. In order to do so, we are drawing ideas from papers such as the ones described in my talk, in addition to contextual model type theory.