# A Neighborhood of Infinity

## Sunday, April 29, 2007

### Homeland Security Threat Level Monad

I've previously introduced the idea of a monad being a kind of one way wrapper. The Monad interface allows you to wrap things, but not unwrap them again. And it allows you to apply any function you like to a wrapped object, as long as it stays wrapped. I also indicated how this could be used to model a notion of taint. If you have some data from a tainted source - for example it's unreliable, then the trivial monad can do a nice job of keeping track of all other data that has been tainted by contact with this data. What I also want to show is that a wide variety of other monads can be interpreted in terms of taint. What this means is that despite its simplicity, the trivial monad is always worth keeping in the back of your mind because it is a protoype for many other monads.

You could imagine using this taint idea as a security model. Any data of type W a is considered secret and a threat to public safety if it is revealed. By sticking to the Monad interface we force the compiler to make sure that any data depending on secret data is itself marked secret. This makes it easy to keep secret data sequestered - at least as long as people only use the Monad interface to W.

But suppose this isn't good enough and we need to track not only which data is secret, but also the threat level to public safety should a secret be revealed. With this in mind, define the Homeland Security Threat Level Monoid:

> data Threat = LOW | GUARDED | ELEVATED | HIGH | SEVERE>          deriving (Eq,Ord,Enum,Show)

It's a monoid because it has an associative binary operator max and has an identity LOW. For example max LOW ELEVATED = ELEVATED.

We want to tag some of our data with a threat level. In addition, we want to ensure that if we combine two tagged pieces of data, x and y, the combination must be tagged with the worse of the two threat levels. That's why we have the monoid structure that allows us to combine two threats.

So define
> data T a = T Threat a deriving Show

But to use this it appears we have to thread use of the max function all the way through our code. It'll be a nightmare to implement. But there's a solution. What we want is a monad!

Consider LOW to be the default threat level of all data and that tells us how to define return.

Now suppose we have a function f :: a -> T b and some data x :: T a. We want to be able to apply f to x using the monad interface: x >>= f. The threat level of the result should be the max of the two possible sources of threat: x itself or the result of computing f. With that in mind:

> instance Monad T where>     return x = T LOW x>     (T t x) >>= f = let T t' x' = f x in T (max t t') x'

Notice how we've now shown how to implement threat combination in a way that can be used by any code that uses the monad interface. So now we can take last week's definition of h and use it:

> g x y = y >>= (return . (+x))> h x y = x >>= (\x -> g x y)

Try evaluating h (T ELEVATED 3) (T GUARDED 6). It just works, even though g and h were originally written for the trivial monad! So it's trivial to make code that's written monadically work with our new threat level system. This should give some idea of the power of monads. We've completely changed the sematics of our monadic addition operator, h, without lifting a finger to edit it.

But notice that I didn't need to talk about threats at all. I've shown how to tag data with other data that's implicitly carried along with it. All we needed was a rule for combining pairs of tags. Our tags were of type Threat. Instead we could have used strings and instead of max we could have used ++. If we had, then we'd have a way of implicitly carrying around logs with our computations. In fact, all I have done here is implement a special case of the Writer monad. But I still think that thinking in terms of data that is quarantined in some way helps with the intuition.

I hope that by starting with the trivial monad last week, and upgrading in a natural way to the Homeland Security Threat Level monad, I've given an easy way to think about monads. Our ordinary intuitions about taint, for example that if a clean object touches a tainted one it becomes tainted itself, carry over to monads. And the Writer monad isn't the only one that can be thought of in these terms. I hope at some point soon to look at the Maybe and list monads in this way too.

Creighton Hogg said...

Hi Mr. Sigfpe,
I don't know how much this'll interest you but there's a paper on using monad transformers to separate security levels for a separation kernel. I don't know if these ideas were ever actually incorporated in the Osker project or not. I've found hard to find out anything related to Programmatica.
http://www.cse.ogi.edu/PacSoft/projects/programatica/domainseparation.pdf

Thomas Schilling said...

A straightforward extensions of this scheme is to not only tag the result with the right level, but to also control who may actually use sensitive data. I haven't thought this through, but I'm quite confident that this can be modeled nicely with arrows. The questions is how much type-level programming magic this would involve ...

sigfpe said...

Thomas,

Having said that, I've a feeling comonads can be used to handle privileges. I also think Arrows may be useful when you want something to be both monadic and comonadic. So I suspect you're right.

Creighton Hogg said...

Your comment about comonads and security has intrigued me. I'm going to try and have something written up tonight that may clear things up for at least myself and hopefully be interesting to others.

Also, I'm sorry but the link I first posted looks really messed up on my laptop.

The paper is called Domain Separation by Construction, and is easily found on google scholar.

Josef said...

There is a paper which explains how to do security using arrows. It's called Encoding Information Flow in Haskell and it's a pretty cool paper. There's also a follow-up paper by some other guys which shows how to extend the results with side effect and concurrency: A Library for Secure Multi-threaded Information Flow in Haskell.