In ghci I get

...

...

let evil = appendLog "Foo" "Bar" <interactive>:1:11: Ambiguous type variable `p' in the constraints: `PRead p' arising from a use of `appendLog' at <interactive>:1:11-31 `PWrite p' arising from a use of `appendLog' at <interactive>:1:11-31 Probable fix: add a type signature that fixes these type variable(s)

And then, specializing evil's type:

...

...

let good = appendLog "Foo" "Bar" :: Sealed Admin String unseal (undefined :: Admin) good "FooBar"

-- Steffen On 02/09/2011 06:15 PM, Cristiano Paris wrote:

Hi all,

I've a type problem that I cannot solve and, before I keep banging my head against an unbreakable wall, I'd like to discuss it with the list.

Consider the following code:

------------ module Main where

class PRead p where {} class PWrite p where {}

newtype Sealed p a = Sealed a

instance Monad (Sealed p) where return = Sealed (Sealed x)>>= f = f x

mustRead :: PRead p => a -> Sealed p a mustRead = Sealed

mustWrite :: PWrite p => a -> Sealed p a mustWrite = Sealed

readLog :: PRead p => String -> Sealed p String readLog = mustRead . id

writeLog :: PWrite p => String -> Sealed p String writeLog = mustWrite . id

appendLog l e = do l<- readLog l writeLog $ l ++ e ------------

The central type of this code is Sealed, which boxes a value inside a newtype with a phantom type which represents a "set of permissions".

This set of permissions is implemented through a series of type classes (PRead and PWrite in this case) which are attached to the permission value p of the Sealed newtype.

This way I can define which set of permissions I expect to be enforced when trying to peel off the Sealed value. The use of the Monad class and type classes as permissions behaves nicely when combining functions with different permission constraints, as it's the case of appendLog, whose type signature is:

appendLog :: (PRead p, PWrite p) => String -> [Char] -> Sealed p String

Very nice, the permissions accumulates as constraints over the p type. Now for the "peel-off" part:

------------ unseal :: p -> Sealed p a -> a unseal _ (Sealed x) = x ------------

Basically this function requires a witness value of the type p to peel-off the Sealed value. Notice that:

------------ unseal undefined $ appendLog "Foo" "Bar" ------------

won't work as the undefined value is unconstrained. That's good, because otherwise it'd very easy to circumvent the enforcing mechanism. So, I defined some "roles":

------------ data User = User data Admin = Admin

instance PRead User where {}

instance PRead Admin where {} instance PWrite Admin where {} ------------

If I try to unseal the Sealed value passing User, it won't succeed, as the type checker is expecting the value of a type which is also an instance of the PWrite class:

------------ *Main> unseal User $ appendLog "Foo" "Bar"

<interactive>:1:14: No instance for (PWrite User) arising from a use of `appendLog' at<interactive>:1:14-34 ------------

while works perfectly if I pass Admin as a value:

------------ *Main> unseal Admin $ appendLog "Foo" "Bar" "FooBar" ------------

The idea is to hide the Admin and User constructor from the programmer and having two factory functions, checkAdmin and checkUser, which checks whether the current user has the named role, something like:

------------ checkAdmin :: IO Admin checkUser :: IO User ------------

where role checking happens in the IO Monad (or something similar), a-là trusted kernel. So far so good and I'm very happy with that.

Now the problem.

I would like to enforce permissions not at the role level, but at the permissions level. Let's say that I want to leave "unseal" unchanged, I'd like to "construct" a p-value for unseal "combining" functions checking for single permissions, that is, in pseudo-code:

unseal (checkPRead .*. checkPWrite) $ appendLog "Foo" "Bar"

where .*. is some kind of "type aggregation" operator.

Or maybe something like:

(checkPRead .*. checkPWrite) $ appendLog "Foo" "Bar"

So far I got only frustration. In principle it seems possible to achieve this result because everything is known at compile time and the type-checked should have all the information available to enforce the security constraints.

Anyhow, I couldn't write any usable code.

Any help would be appreciated, even pointers to papers discussing this approach.

Thank you,

On Wed, 2011-02-09 at 18:15 +0100, Cristiano Paris wrote:

I've a type problem that I cannot solve and, before I keep banging my head against an unbreakable wall, I'd like to discuss it with the list.

If I'm understanding your high-level goals correctly, then you're going about things the wrong way. It looks like in your "Sealed" type, you're accumulating a list of type class constraints that are needed by a phantom type, in order to access the value. But type classes are open; anyone can make any new type an instance of the type class whenever they want. In particular, you say:

------------ unseal :: p -> Sealed p a -> a unseal _ (Sealed x) = x ------------

Basically this function requires a witness value of the type p to peel-off the Sealed value. Notice that:

------------ unseal undefined $ appendLog "Foo" "Bar" ------------

won't work as the undefined value is unconstrained. That's good, because otherwise it'd very easy to circumvent the enforcing mechanism.

This is not true, though. One could just as easily write: data Dummy instance PRead Dummy instance PWrite Dummy unseal (undefined :: Dummy) $ appendLog "Foo" "Bar" and they've circumvented your security checks. I think you'll need to back up and rethink your base strategy. Without really understanding fully what you want, I'll still point out that there are tricks with existentials that work when you need someone to have an authentic token to do something; e.g., see the ST monad. -- Chris Smith