On 09.02.2011 20:15, Cristiano Paris wrote:
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:
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.
Text below is literate haskell My solution is based on heterogenous lists and require number of language extensions. I'd recomend to read paper "Strongly typed heterogeneous collections"[1] which describe this technique in detail
{-# LANGUAGE TypeOperators #-} {-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE FlexibleInstances #-}
So lets start with definition of type classes for permissions and data types which represent such permissions.
class PRead a class PWrite a
data WRead = WRead data WWrite = WWrite
Now interestig part begins. We need to compose different permissons. I define heterogenous list for that purpose. It's nothing more than a nested tuple in disguise.
data a ::: b = a ::: b infixr :::
List has instance for some permission if it has corresponding type in it. Please note that I make use of overlapping here. You may need to read about it. Also list need some terminator. WRead is not instance of PRead whereas WRead ::: () is. I will use () for that purpose. It's OK since all type classes here are closed.
instance PRead (WRead ::: b) instance PRead b => PRead (a ::: b)
instance PWrite (WWrite ::: b) instance PWrite b => PWrite (a ::: b)
Here is function for checking that everything is working as expected
withR :: PRead a => a -> () withR _ = ()
withW :: PWrite a => a -> () withW _ = ()
withWR :: (PRead a, PWrite a) => a -> () withWR _ = ()
r = WRead ::: () w = WWrite ::: () rw = WRead ::: WWrite ::: ()
[1] http://homepages.cwi.nl/~ralf/HList/ P.S. You can use phantom types to propagate type information. I feel that carrying undefined is morally dubious practice.
data T a = T newtype Sealed p a = Sealed a
unseal :: T p -> Sealed p a -> a unseal _ (Sealed x) = x
admin :: T (WRead ::: WWrite ::: ()) admin = T