Thursday, April 19, 2007

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.

15 comments:

Thomas Schilling said...

You wrote: "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."

Well, it is. See, e.g., this paper on HaskellDB, section 4.3.2: http://haskelldb.sourceforge.net/haskelldb.pdf

I was just pointed to this paper: http://www.cs.virginia.edu/~jba5b/singleton/
Maybe that might be interesting for you, too.

Creighton Hogg said...

I wasn't aware of that HaskellDB paper, and while what they do is clever I think it almost reinforces my point. We can abuse typeclasses until you get some notion of less than, but what about implementing the binary operators on the lattice?

I haven't seen that other paper though, so thanks for linking it!

Josef said...

I totally agree with you that the paper is awesome. I was very impressed by it when I read it. However, as soon as you start trying to actually use it for something you're immediately going to bump its limitations. For instance dealing with any kinds of side effects is far from trivial.
If you're interested in how to deal with these shortcomings I recommend the forthcoming paper by Russo, Tsai and Hughes called "A Library for Secure Multi-threaded Information Flow in Haskell". I guess it will appear in due course.

Antoine said...

If you want to form a lattice on types, would inheritance (in the OO sense) work? The difference between a poset and a lattice is outside my comfort zone, so maybe this doesn't work for you.

That only gets you one of your (three?) lattices for your project at hand. But if your type system already has one notion of inheritance, how hard could it be to add other, orthogonal inheritances?

I guess my point is that people work with partial-orders on sets of types all the time, and there might be some existing systems out there you can leverage if dependent types aren't available.

Antoine said...

Just so I'm clear on your model:

The Haskell type system forces the developer to use the proper arrows to compose computations.

The arrow system, then, would performs run-time checks on capabilities (as well as control flow - but you could likely do that without arrows ^_^).

Will you ultimately need three different constraint-sets as an argument to the FlowArraw constructor, or is it a matter of protocol that the set of constraints form distinct lattices?

I don't remember if this was in the write-up you sent me, but do you have any estimates on the total number of capabilities in a system?

Creighton Hogg said...

Yo Mr. Antoine.
so I hadn't thought too hard about inheritance as a description of lattices. The main problem I see with it is defining the binary operators over the lattice. So, if "inherits from" is the <= operator on our lattice of types, then implementing the join operator would require making the class of the result be the "smallest" class that both of them inherit from while the meet operator would require making the result class the "largest" class that inherits from both.

I guess that doesn't seem too bad if your object system had proper reflection and multiple inheritance. Come to think of it though, I'm not sure of too many object systems that can do that. CLOS can, and I imagine Smalltalk or Ruby could as well.

Now, the question becomes is it worth it? A good bit of our motivation for wanting to put lattice information at the type level is for speed & I have *NO* intuition for how performance is impacted by reflection.

You've gotten me interested though. I should write up some stupid examples in CLOS and see how they work. Thanks.

Also, there would be a capability for any nameable resource. In order to implement safe shared memory, which is one of the goals, even pages would have to be nameable resources. So there'd be a *lot* of capabilities and they should be pretty light weight.

One clarification though. I wouldn't say that the arrows themselves enforce the capabilities. I mean, that's all in the phantom types and doesn't need arrows at all. The arrows are just a nice interface for keeping track of the lattice policy of the calculation. Not necessary, but kind of slick to keep a lot of the plumbing simple.

Anonymous said...

I found this site using [url=http://google.com]google.com[/url] And i want to thank you for your work. You have done really very good site. Great work, great site! Thank you!

Sorry for offtopic

Anonymous said...

Free pills tofranil ED augmentin Order luvox Without prescription maxalt World delivery mevacor No prescription vicodin es

Anonymous said...

Locality pertain formidable they are as a replacement payment uncommon dope [url=http://onlineviagrapill.com]viagra[/url]. Accost divvy up dated the well-balanced efficacy, unusually the arm make oneself scarce reach anyway a lest [url=http://ambiendrug.com]ambien[/url]. This paddling trusteeship normally possibility in be afflicted with prospering and a assuredly physicality in in the sector [url=http://cialislove.com]cialis[/url].

Anonymous said...

Eff you ever been to buynikenow.com? a real unemotional shell outlet with a astronomic [url=http://www.buynikenow.com]Air Max 1[/url] listing and over than chiliad Air Max shoes. The accumulation supplies varied scale sales and discounts and delivers your shoes in 7-10 business days. By far the most advisable station to [url=http://www.buynikenow.com]Buy Nike[/url] items in fantabulous prices.

Dean said...

greetings to all.
I would first like to thank the writers of this blog by sharing information, a few years ago I read a book called Real Estate Investment costa rica in this book deal with questions like this one.

niz said...

Hello .. firstly I would like to send greetings to all readers. After this, I recognize the content so interesting about this article. For me personally I liked all the information. I would like to know of cases like this more often. In my personal experience I might mention a book called Generic Viagra in this book that I mentioned have very interesting topics, and also you have much to do with the main theme of this article.

Cheap viagra said...

First I would like to greet all the people who like to read this blog, on my part can be congratulated for this great contribution, a few months ago I had the opportunity to attend a conference called "really the human" in this conference spoke on an issue identical to this!

Super Bowl Commercials 2012 said...

Thanks for the post. I liked it. Keep going I follow you.
Bot and me| Images|

viagra pills said...

I liked this blog, i think is very interesting, most of all for the new ideas that this blog talk.