Arrows & Security

I've been rereading an interesting paper from last year: Encoding Information Flow in Haskell.

In a nutshell, the paper is about encoding security lattices in Haskell via arrows.
To start with, I should say a few words about lattices. A lattice is, fundamentally, a set with a partial order, a least upper bound binary operator, and a greatest lower bound binary operator. I'm just going to be simple here and consider only bounded lattices where there is an actual least and greatest element for the entire lattice.

Now how does a lattice tie in with security? Well, I found that the original paper on the subject is a very good introduction, but the basic idea is that any sane arrangement of security labels that can be assigned should form a lattice. For example, if you have two security labels then you have privileges greater than or equal to either of them.

Matrioshka, our planned OS kernel, uses three lattices along with type-level capabilities to completely describe any information policy. In case it's not immediately clear why one cannot include lattice information in the capabilities, the reason is that Haskell doesn't have true dependent types so comparisons on the type level are boolean in nature. The types match or they do not. You can't examine the types and decide whether one is "greater" than the other in some sense.

Now this paper advocates using arrows as an interface to describe protected computations. Essentially, you wrap up functions with the extra data describing the lattice information and then use the standard arrows typeclasses to handle control flow and composition. I actually think it's a rather neat approach.

So the basic data structure involved is the FlowArrow

data FlowArrow l a b c = FA {
  computation :: a b c,
  flow :: Flow l,
  constraints :: [Constraint l]}

A FlowArrow is a wrapper around any other arrow type that also includes the change in lattice point for the computation and a list of constraints on the lattice generated by the composition of FlowArrows. This list of constraints is then matched against the lattice and if everything checks out the computation is unwrapped and can be executed. Pretty slick.

Of course, we can add phantom types to the FlowArrow pretty easily and thus get some representation of actual capabilities.

data CapArrow caps l a b c = CA (FlowArrow l a b c) 

So now we require that for arrows to be composed together, the capabilities must be of the same type. This is where Haskell's polymorphism pays off as we can then compose arrows that have capability requirements such as

readArrow :: CapArrow (Read,d) l a b c

and

writeArrow :: CapArrow (d,Write) l a b c

if the user had possession of a resource with the proper permissions attached to it

initArrow :: Resource caps b -> CapArrow caps l a b b

Now, a lot of this is still speculation because I have no hard prototype. In terms of a system built on top of House, the underlying arrow instance would probably be Kleisli arrows for the H monad.