prev Week 1 of 16 next
My final exams ended last week, and I made it out alive. Time to start working whole-heartedly on research.
While preparing for a meeting with Brigitte, I happened to skim a paper I read last semester: Access Control in a Core Calculus of Dependency. It made a lot more sense this time around. I have thus decided to carefully reread the 5 or 6 papers I have been exposed to while learning about logic and access control during the semester. I think this will give me some much needed perspective and help some of my ideas settle. For instance, there exist logical formalizations of access control that define a principal as just a set of permissions. Others, on the other hand, distinguish principals from permissions. So, which, if either, is the right way to think about it? How should we think about principals when designing the type system for a programming language? I probably shouldn't get too obsessed with this question, but it's certainly been distracting me. Hopefully, I will become more comfortable with this after the proposed re-reading.
During my most recent meeting with Brigitte, we considered a tentative description of our target type system. Brigitte proposes to divide the terms into two distinct levels: one for "regular" computations, and the second for reasoning about access control. This second level is the one that would be based on an authorization logic. It would contain all the usual logical connectives, such as "and", "or", and some specialized terms such as "K says s" or "K controls s". The choice of terms depends on how we design our authorization logic.
The authorization logic component is based on a contextual modal logic. Modal logic has several levels of truth: a proposition can be true in every world, or it can be true in some worlds. In contextual modal logic, a proposition may be judged to be true relative to a specific context of assumptions. To be clear, you can write something like "A is true in a world in which B and C are valid". This doesn't make the logic any more expressive than a modal logic without contextual annotations or operands, but it does offer a new flexibility. It is particularly promising for our access control project since we would like to produce a programming language suitable for distributed systems. For example, we might be able to reason about where, within a distributed system, a piece of code is allowed to run by using contextual information such as the presence of a printer, say. Generally speaking, solutions aimed at a distributed computing setting need to incorporate this sort of flexibility in order to handle decentralization.
For the moment, Brigitte thinks we should use a bidirectional type system, which incorporates the use of type annotations in the type-checking process. Since access control policy information is to reside directly in our type system, it makes sense to use type annotations in the programming language as a means for policy documentation. More on this later.
The most immediate goal is to determine whether our proposed type system is actually useful for its intended purpose. If that works out, I might implement a testing framework in SML. This will give me the ability to compare different approaches to the access control problem. So by next week, I am supposed to be done with my re-reading, and I am to come up with some simple application examples that will help us get a sense of whether our type system is well formulated or not (i.e. whether it's actually useful). In next week's journal entry, I might explain access control and authorization logics more precisely, and share the outcome of my examples.