prev Week 2 of 16 next
Last week, Brigitte gave me a type system to look at. I was supposed to think about whether this proposed type system is a good base for a programming language designed to enforce access control policies. The best way to do this is to try to express some simple access control scenarios using the proof terms of the type system. If we can't even express the simplest examples easily, we need to go back and change the system.
Before starting to work on finding such examples, I spent a good amount of time reading about about general principals in computer security and previous logic-based projects related to access control. I didn't find any shocking ideas, but this extra background reading got a me little more comfortable with the material I learned for this project last semester.
However, every hour spent reading was an hour spent not thinking about the type system I was really supposed to be thinking about. Predictably, I delayed my most important task for quite some time. When I finally got to it, I realized I didn't understand how the type system could possibly work. As it turns out, there was a miscommunication between Brigitte and I: the proposed type system was intended for a static access policy, whereas I was trying to make it work for dynamic policies. Looking at it again, everything makes much more sense. So I will work out some examples this week.
The plan is to start with a simple version of the type system, with only static permissions in mind, and build it up according to what we learn from the examples we study. My first examples will all refer to a central security policy, and the authorization logic will not be used to derive any permissions. Programs will simply reference statements in the central policy. If that works reasonably well in some basic scenarios, such as a program trying to access a protected file of some sort, then I will define basic inference rules for the embedded authorization logic and work out some examples that involve short derivations. For instance, when type checking gets to the stage where it must be decided whether a program has the right to open some file, a little proof of access must be generated based on rules in the central security policy. Informally, a proof might sound something like: "The central policy states that 'profs are allowed to access file x', and that 'Elmer is a prof'. We infer that Elmer may access file x."
The next step is to allow programs to modify the central security policy. For example, a program may declare itself protected from students. This addition essentially comes down to adding a controled method of accessing the authorization layer of the type system from the computational layer (via a new inference rule in the computational portion of the system).
Eventually, it would be cool to be able to access the computational layer from the authorizational layer. Having a way for the authorization logic to refer to programs by name or by role is an interesting idea that we will explore in the future.
In other news, I'm supposed to give an hour-long talk in a week and a half to introduce the rest of our group to logic and access control since I'm the only one working on this stuff. I better get started...