Few days ago I was working on some API handlers in our server written in Haskell with the framework Yesod. There was a mistake, some secret data was accessible to normal users because we forgot to check the user’s type, luckily it’s not on production yet. The fix is simple, just a line of if (userType user) /= Admin then ... but that doesn’t seems to solve the problem fundamentally, it’s simply so easy to forget to check for permission in various cases. Well, this is Haskell, wouldn’t it be possible to make it a compile time error if we forget to check it?
The handler looks like this.
getFooR = do
post <- get (PostKey aPostId) -- This line is ok
secret <- get (SecretKey aSecretId) -- This isn't. Secret is accessible for Admin only.
...
There is no different between getting a post and a secret, which means the compiler has no information to know whether is this allowed or not. In order to make things simpler, I’d like to simplified it into something like this first:
-- Lets say all the operations are IO String
operation :: IO String
operation = do
guestStr <- guestOperation
userStr <- userOperation
adminStr <- adminOperation
pure $ guestStr <> userStr <> adminStr
In the above example, I would like to have the compiler giving me an error for a certain operation. E.g. something like this:
operation :: IO String
operation = checkPermission @User $ do
guestStr <- guestOperation
userStr <- userOperation
adminStr <- adminOperation -- Some kind of error on this line
pure $ guestStr <> userStr <> adminStr
So here is the plan.
To create a type level list, we have to enable the some extensions.
{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, TypeOperators #-}
data UserType = Admin | User | Guest
-- The DataKinds extension turns "data and types" into "types and kinds"
data List a = Nil | a :> (List a)
infixr 5 :>
-- With the above definition, we can write a list like this:
type PermissionDef = Admin :> User :> Guest :> Nil
-- And we can also write some type level functions that would be helpful later
-- `After` is a type level function that returns the rest of the list after a certain element
type family After (a :: k) (i :: List k) where
-- If the first element matches, return the rest of the elements
After a (a :> rest) = rest
-- If the first element does not match, try to find from the rest of the elements
After a (b :> rest) = After a rest
-- If the list is empty, return an empty list.
After _ Nil = Nil
-- Example usage:
-- `After B (A :> B :> C :> Nil)` would have the same type as `C :> Nil`
With the above code, we can write a function that generates a list of available permission when given a user type.
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
type AvailablePermissions a = a :> (After a PermissionDef)
permissionsOf :: forall p. Proxy (AvailablePermissions p)
permissionsOf = Proxy
Example:
While we can calculate a list of permission, we need somewhere to put them. So lets create a monad transformer to add the list to the base monad.
-- Nothing really interesting
data PermissionT :: List UserType -> (* -> *) -> * -> * where
PermissionT :: m a -> PermissionT l m a
instance Functor m => Functor (PermissionT l m) where
fmap f (PermissionT io) = PermissionT (fmap f io)
instance Applicative m => Applicative (PermissionT l m) where
(PermissionT f) <*> (PermissionT v) = (PermissionT $ f <*> v)
pure = PermissionT . pure
instance Monad m => Monad (PermissionT l m) where
(PermissionT m) >>= f = PermissionT
(m >>= \x-> let (PermissionT p) = f x in p)
instance MonadTrans (PermissionT l) where
lift = PermissionT
instance MonadIO m => MonadIO (PermissionT l m) where
liftIO = PermissionT . liftIO
And we want a type level function that checks if an element is in the list.
type family InList (a :: k) (l :: List k) :: Bool where
InList _ Nil = False
InList a (a :> rest) = True
InList a (_ :> rest) = InList a rest
Such that, finally, we can describe the required permission! The function body doesn’t matter, just for demonstration.
-- This operation does not require any permission
safeOperation :: PermissionT l IO String
safeOperation = lift readLn
-- Assert that `Guest` is in the list `l`
guestOperation :: (InList Guest l ~ True) => PermissionT l IO String
guestOperation = lift readLn
-- Assert that `User` is in the list `l`
userOperation :: (InList User l ~ True) => PermissionT l IO String
userOperation = lift readLn
-- Assert that `Admin` is in the list `l`
adminOperation :: (InList Admin l ~ True) => PermissionT l IO String
adminOperation = lift readLn
Instead of just asserting the permissions, we also want to have a “checking function” that is responsible to check the permissions, and therefore remove the constraints on the list after the check. This is very similar to the previous permissionsOf function.
checkPermission :: forall p a l m. PermissionT (AvailablePermissions p) m a -> PermissionT l m a
checkPermission (PermissionT m) = PermissionT m
Available permissions are calculated by the provided user type. While the constraints on the calculated list is determined by the operations. Operations that failed to have it’s constraint fulfilled would have errors like this:
Finally, we need a way to “exit” the monad transformer.
runPermissionT :: PermissionT Nil m a -> m a
runPermissionT (PermissionT m) = m
Here is the key, by asserting the final list of permission to be Nil, we are forcing the user to create operations that does not ask for any permission. And if any permission is needed, they have to check it.
So, the simplified operations checking is working pretty nice. Let’s try to have it solving the original issue. The library used in Yesod is called yesod-persistent, here is a simplified version of its model types:
data Secret = Secret String
data Post = Post Int
class PersistEntity record where
data Key record :: * -> *
get :: Key record k -> IO record
-- Lets say the Secret model has a unique string as id
instance PersistEntity Secret where
data Key Secret k = SecretKey String
get (SecretKey str) = pure $ Secret str
-- And the Post model has a unique int as id
instance PersistEntity Post where
data Key Post k = PostKey Int
get (PostKey n) = pure $ Post n
Models can be accessed like this:
post :: IO Post
post = get (PostKey 1)
secret :: IO Secret
secret = get (SecretKey "hi")
Um… the function is used to get multiple types of model, how can we integrate the permission model we have? We need a way to transform the model into its required permission, and then assert with that permission. Lets describe the “model-permission-relationship”.
type family PermissionNeeded a :: UserType where
PermissionNeeded Secret = Admin
PermissionNeeded Post = User
PermissionNeeded _ = Guest
Instead of the normal get, we have to create a version of get that understand the permission, and therefore returns in the context of PermissionT.
safeGet
:: ( PersistEntity record
, InList l (PermissionNeeded record) ~ True
)
=> Key record k
-> PermissionT l IO record
safeGet = PermissionT . get
Which is integrated nicely with other operations!
In the above examples, I did nothing much except from checking for permissions, but it can be very powerful depends on how you implement the functions. This kind of checking is not difficult, but just easy to forget, especially when nested inside functions. By putting permission checking into type level, the type checker can help to make a more secure program.
The implementation idea is based on a paper about implementing type-safe, explicit exceptions.
I work at HERP and we are hiring. We mostly write Typescript but we do use some Haskell.