Role based access control via monads or arrows or... something

porrifolius

2 Apr 2008 2 Apr '08

5:22 p.m.

Hello. I've been playing around trying to write a framework to support/enforce access control to resources. So far my efforts have yielded little but bruised forehead and compressed plaster-board. What I'd like is a solution that: (1) prevents access to resources except via a fine-grained permissions checking gateway (2) supports on-the-fly permissions eg Bob can see Fred's salary (3) supports dynamic role constraints eg Bob can't be both appointor and appointee of secret agent status (4) allows lack of permission to optionally act as a filter rather than cause an abort, eg Bob viewing all salaries returns Fred's but doesn't return Tom's rather than aborting altogether because Bob lacks the permission over Tom (5) well defined behaviour when checking permissions for actions that change permissions (6) it must be pure, no need for IO. (7) ideally required permissions would appear (and accumulate) in type signatures via inference so application code knows which are required and type checker can reject static/dynamic role constraint violations I've attempted a solution using arrows based loosely upon ideas in [1] and [2]. I can't figure out how to make it work, even if I did get it working I now suspect it can be done far more simply, and I don't think it could ever provide feature (7). For what it's worth it's attached. Ideally you kind folk could help me come up with a type-level solution to satisfy (7), so you could have something like: deptAveSal :: (HasPerms subject? Read Salary [person]?, HasPerm subject? Read Employees dept?, HasRole subject? Manager dept?) => Department -> Salary Failing that how to do it in a more simple fashion? I now think that a State-like monad exposing only functions taking values in a wrapper type that carries required permissions may be sufficient, but still probably couldn't satisfy (7). Failing that my existing attempt has me stumped for a few reasons: how do I get hold of the subject and resource so I can build the correct permission in Test? eg the Person whose Salary is needed in salary, and who's trying to get it where do I get the System from in Test? eg fakeSystem in personByName how to implement the filter functionality in RBAC? Parametric over container types? I think that perhaps the Validator would need to be a monad that holds the initial state of the System to provide a stable set of permissions/roles and that the subject and System should also be threaded through the arrows for use/modification. Any help you can offer for my aching cranium will be _much_ appreciated. Thanks. [1] Encoding Information Flow in Haskell - Peng Li, Steve Zdancewic. http://www.seas.upenn.edu/~lipeng/homepage/flowarrow.html [2] A Library for Secure Multi-threaded Information Flow in Haskell - Alejandro Russo, Tsa-chung Tsai, John Hughes. http://www.cs.chalmers.se/~russo/publications.html

Attachments:

RBAC.hs (text/haskell — 2.7 KB)
Test.hs (text/haskell — 1.6 KB)

Show replies by date

Luke Palmer

2 Apr 2 Apr

8:45 p.m.

New subject: Role based access control via monads or arrows or... something

2008/4/2 porrifolius :

...

(7) ideally required permissions would appear (and accumulate) in type signatures via inference so application code knows which are required and type checker can reject static/dynamic role constraint violations

If you mean what I think you mean by "dynamic", that these are runtime permissions, then you're not going to get the type checker to check them... of course. What did you mean by dynamic?

...

I've attempted a solution using arrows based loosely upon ideas in [1] and [2]. I can't figure out how to make it work, even if I did get it working I now suspect it can be done far more simply, and I don't think it could ever provide feature (7). For what it's worth it's attached.

Ideally you kind folk could help me come up with a type-level solution to satisfy (7), so you could have something like: deptAveSal :: (HasPerms subject? Read Salary [person]?, HasPerm subject? Read Employees dept?, HasRole subject? Manager dept?) => Department -> Salary

What comes to mind is that you could pass proofs around which represent required permissions. The hard part is coming up with a data type algebra for expressing your "theorems" (permission requirements). If you want a rich system of permissions, it's pretty unlikely that you'll get inference. data HasRole role dept = HasRole -- do not expose this constructor data HasPerm perm obj dept = HasPerm -- nor this one class Department d where deptAveSal :: (Department dept) => HasPerm ReadPerm Employees dept -> HasRole ManagerRole dept -> dept -> Salary And then dole out HasRoles and HasPerms through your module interface. However, I'm pretty sure any solution to (7) will be unsatisfactory to you, considering your long list of requirements. Haskell's type system is not SQL, it will have a hard time supporting these things. If you're interested in programming with type-safe permissions you might want to look into dependent types (Epigram, Agda 2), but those languages are not what you would consider "mature" or "fast" (it takes 1 second to verify that 113 is prime in Agda 2... now you see what I mean?). It would be an academic exercise. Here's my ill-informed advice (since I don't know what problem you're trying to solve, only what solution you want to have): Forget (7), stay away from arrows for this, and avoid overengineering (this kind of problem especially likes to attract overengineers). My hunch is that you only need two things: a data type witnessing a permission. That is, don't worry about the subject? stuff; if the program can get its hands on a witness of a permission, then it has that permission. I would start with KISS, just a plain unparameterized data type: -- keep this type abstract and do not expose the constructors data Perm = ReadSalaryPermission Employee | ... And then maybe introduce separation and type parameters as you start to use them and see where the logical boundaries are. Of the possible ways you can put this into a monad, I would say "Access t" is a computation which results in a value of type t after receiving witnesses of required permissions. I considered: data Access a = Access { value :: a, required :: Set Perm } But I like to avoid ad-hoc checks like this and actually put the checks right in the code. newtype Access' a = Access' (Set Perm -> Maybe a) Or: data Access'' a = Result a | NeedPermissions (Set PermSpec) (Set Perm -> Access'' a) Or something like that. Let the computation figure out how to verify the permissions. Notice how Perm and PermSpec are different in the last example, because of the witness model. You don't want to give someone the permissions to do something when you're just trying to tell them what permissions they need. In particular, though, there is nothing arrow-like about this problem. Arrows abstract the notion of function, and this problem is all about values. Luke

David Roundy

3 Apr 3 Apr

9:18 a.m.

New subject: Role based access control via monads or arrows or... something

On Thu, Apr 03, 2008 at 12:45:49AM +0000, Luke Palmer wrote:

...

2008/4/2 porrifolius :

...
(7) ideally required permissions would appear (and accumulate) in type signatures via inference so application code knows which are required and type checker can reject static/dynamic role constraint violations

If you mean what I think you mean by "dynamic", that these are runtime permissions, then you're not going to get the type checker to check them... of course. What did you mean by dynamic?

With GADTs you can certainly get pretty easy compile-time type checking of dynamic constraints. The catch is that GADTs aren't properly integrated with type classes, and this sort of permissions problem may not be expressible without class constraints, in which case the system may require olegish code complexity. At the simplest (and stupidest) level, one could define data CanReadA data CanReadB -- etc data HavePermission perms where HaveAPerm :: HavePermission CanReadA HaveBPerm :: HavePermission CanReadB and if you then restricted access to the constructors of HavePermission, you could write code like data RestrictedData permrequired a = Data a -- constructor obviously not exported, or you'd lose any safety readRestrictedData :: HavePermission perm -> RestrictedData perm a -> a and now if you export readRestrictedData only, then only folks with the proper permissions could access the data (and this could be done at runtime). But this is far from an elegant or satisfactory (or complete) solution. -- David Roundy Department of Physics Oregon State University

apfelmus

11:31 a.m.

New subject: Role based access control via monads or arrows or... something

David Roundy wrote:

...

Luke Palmer wrote:

...
porrifolius wrote:

...
(7) ideally required permissions would appear (and accumulate) in type signatures via inference so application code knows which are required and type checker can reject static/dynamic role constraint violations

If you mean what I think you mean by "dynamic", that these are runtime permissions, then you're not going to get the type checker to check them... of course. What did you mean by dynamic?

At the simplest (and stupidest) level, one could define

data CanReadA data CanReadB -- etc

data HavePermission perms where HaveAPerm :: HavePermission CanReadA HaveBPerm :: HavePermission CanReadB

and if you then restricted access to the constructors of HavePermission, you could write code like

data RestrictedData permrequired a = Data a -- constructor obviously not exported, or you'd lose any safety

readRestrictedData :: HavePermission perm -> RestrictedData perm a -> a

and now if you export readRestrictedData only, then only folks with the proper permissions could access the data (and this could be done at runtime).

At runtime, are you sure? I mean, if I want to use it like in foo = ... readRestrictedData permission secret ... I must know that the type of my permission matches the the type of secret , either by knowing them in advance or by propagating this as type variable into the type of foo. In any case, I may only write foo if I know statically that permission is going to match the secret . No runtime involved? In other words, I fail to see how this GADT example is different from a normal phantom type (modulo different naming) data Permission p = Permitted -- not exported low :: Permission Low -- same role as HaveAPerm high :: Permission High -- a module which knows these constants has -- corresponding permissions data Restricted p a = Restricted a readRestricted :: Permission p -> Restricted p a -> a Regards, apfelmus

David Roundy

11:51 a.m.

New subject: Role based access control via monads or arrows or... something

On Thu, Apr 03, 2008 at 05:31:16PM +0200, apfelmus wrote:

...

David Roundy wrote:

...
Luke Palmer wrote:

...
porrifolius wrote:

...
(7) ideally required permissions would appear (and accumulate) in type signatures via inference so application code knows which are required and type checker can reject static/dynamic role constraint violations

If you mean what I think you mean by "dynamic", that these are runtime permissions, then you're not going to get the type checker to check them... of course. What did you mean by dynamic?

At the simplest (and stupidest) level, one could define

data CanReadA data CanReadB -- etc

data HavePermission perms where HaveAPerm :: HavePermission CanReadA HaveBPerm :: HavePermission CanReadB

and if you then restricted access to the constructors of HavePermission, you could write code like

data RestrictedData permrequired a = Data a -- constructor obviously not exported, or you'd lose any safety

readRestrictedData :: HavePermission perm -> RestrictedData perm a -> a

and now if you export readRestrictedData only, then only folks with the proper permissions could access the data (and this could be done at runtime).

At runtime, are you sure? I mean, if I want to use it like in

foo = ... readRestrictedData permission secret ...

I must know that the type of my permission matches the the type of secret , either by knowing them in advance or by propagating this as type variable into the type of foo. In any case, I may only write foo if I know statically that permission is going to match the secret . No runtime involved?

In other words, I fail to see how this GADT example is different from a normal phantom type (modulo different naming)

The difference is that I can inspect at runtime what permissions I have. I see that I didn't demonstrate this. You can introduce a function checkPerms :: HavePermission p -> HavePermission p' -> EqCheck checkPerms HaveAPerm HaveAPerm = IsEq checkPerms HaveBPerm HaveBPerm = IsEq checkPerms _ _ = NotEq data EqCheck a b where IsEq :: EqCheck a a NotEq :: EqCheck a b which allows you to compare permissions at runtime and make use of them. -- David Roundy Department of Physics Oregon State University

Dan Weston

2:41 p.m.

New subject: Role based access control via monads or arrows or... something

Is this type-level design flexible enough for future requirement changes? The best answer to "Why is this door locked?" may not be "You don't have permission to open it", but rather "What door?". Suppose a client comes along later with a requirement that the permissions themselves are secret (e.g. I don't want you to know that I have permission to read your email). Now the permissions themselves have to be reflected somehow. And this reflection has permissions of its own. And permissions might have to nest not like locked doors but like trap doors. The most effective permission denial is the illusion that there is nothing there. Also, doesn't the type-level correspond to an intuitionistic logic, so it is difficult to express the concept of not-having-permission (a Vice President has permission to nuke some defenseless country only if the President's permission has been revoked through impeachment). Moreover, I see no way to have side effects (if someone peeks into your secret documents, let them look rather than tip them that you are on to them, but monitor their movements to see who they sell them to). Finally, type checking always halts, but it may desirable (in a Kafkaesque way) simply not to answer, such as when a dissident applies for an exit visa she is entitled by law to receive. Some many ways for a rigid design to fail. Dan David Roundy wrote:

...

On Thu, Apr 03, 2008 at 05:31:16PM +0200, apfelmus wrote:

...
David Roundy wrote:

...
Luke Palmer wrote:

...
...
(7) ideally required permissions would appear (and accumulate) in type signatures via inference so application code knows which are required and type checker can reject static/dynamic role constraint violations If you mean what I think you mean by "dynamic", that these are runtime

porrifolius wrote: permissions, then you're not going to get the type checker to check them... of course. What did you mean by dynamic?

At the simplest (and stupidest) level, one could define

data CanReadA data CanReadB -- etc

data HavePermission perms where HaveAPerm :: HavePermission CanReadA HaveBPerm :: HavePermission CanReadB

and if you then restricted access to the constructors of HavePermission, you could write code like

data RestrictedData permrequired a = Data a -- constructor obviously not exported, or you'd lose any safety

readRestrictedData :: HavePermission perm -> RestrictedData perm a -> a

and now if you export readRestrictedData only, then only folks with the proper permissions could access the data (and this could be done at runtime). At runtime, are you sure? I mean, if I want to use it like in

foo = ... readRestrictedData permission secret ...

I must know that the type of my permission matches the the type of secret , either by knowing them in advance or by propagating this as type variable into the type of foo. In any case, I may only write foo if I know statically that permission is going to match the secret . No runtime involved?

In other words, I fail to see how this GADT example is different from a normal phantom type (modulo different naming)

The difference is that I can inspect at runtime what permissions I have. I see that I didn't demonstrate this. You can introduce a function

checkPerms :: HavePermission p -> HavePermission p' -> EqCheck checkPerms HaveAPerm HaveAPerm = IsEq checkPerms HaveBPerm HaveBPerm = IsEq checkPerms _ _ = NotEq

data EqCheck a b where IsEq :: EqCheck a a NotEq :: EqCheck a b

which allows you to compare permissions at runtime and make use of them.

apfelmus

6 Apr 6 Apr

5:27 a.m.

New subject: Role based access control via monads or arrows or... something

David Roundy wrote:

...

apfelmus wrote:

...
David Roundy wrote:

...
porrifolius wrote:

...
(7) ideally required permissions would appear (and accumulate) in type signatures via inference so application code knows which are required and type checker can reject static/dynamic role constraint violations

In other words, I fail to see how this GADT example is different from a normal phantom type (modulo different naming)

The difference is that I can inspect at runtime what permissions I have. I see that I didn't demonstrate this. You can introduce a function

checkPerms :: HavePermission p -> HavePermission p' -> EqCheck checkPerms HaveAPerm HaveAPerm = IsEq checkPerms HaveBPerm HaveBPerm = IsEq checkPerms _ _ = NotEq

data EqCheck a b where IsEq :: EqCheck a a NotEq :: EqCheck a b

which allows you to compare permissions at runtime and make use of them.

Ah, so you are able to use case expressions casePerm :: (Permission Low -> a) -> (Permission High -> a) -> Permission any -> a which is not possible with a plain phantom type approach. One example use would be foo :: Permission p -> Either String Bar foo = casePerm (const $ Left "foo: permission too low") (\p -> readRestricted p ... ) Of course, you may not export HaveAPerm and HaveBPerm (at least not for construction, only for pattern matching), so you probably need such a special function casePerm anyway. Regards, apfelmus

Wouter Swierstra

5:41 a.m.

New subject: Role based access control via monads or arrows or... something

...

Any help you can offer for my aching cranium will be _much_ appreciated.

You might also be interested in the paper Edwin Brady and Kevin Hammond just submitted to ICFP: http://www.cs.st-andrews.ac.uk/~eb/drafts/icfp08.pdf It describes how to manage resources, in particular locks, in a dependently-typed language. You didn't explicitly mention that it needed to be in Haskell, so it might be worth having a look. Best of luck, Wouter

6256

Age (days ago)

6260

Last active (days ago)

List overview

Download

7 comments

6 participants

participants (6)

apfelmus
Dan Weston
David Roundy
Luke Palmer
porrifolius
Wouter Swierstra