8 ms·

Is Datalog a good language for authorization?

68 points by triska 5y ago

flurie 5y ago
Sure it is, because the language of Open Policy Agent, called Rego, is a Datalog variant. I find a researcher’s failure to mention this concerning.
- 0x0000000 5y ago
  The second link in the article is https://www.openpolicyagent.org/docs/latest/policy-language/ https://www.openpolicyagent.org/docs/latest/policy-language/
- Nullabillity 5y ago
  The second sentence of the post links to OPA as an example of a system using Datalog for authz. Also, "X uses Y for Z" doesn't imply that Y is good at Z. It can be the start of an argument about how that choice is turning out for X, but it's in no way an argument by itself.
  - flurie 5y ago
    My assertion is glib, but your response is wholly insubstantive. Can you to point out how this piece treats Rego as an actual example of a real-world Datalog? I don't see any link when mentioning real-world Datalogs. The fact that this piece makes no mention of it but provides a drive-by link to it suggests that the author is not actually interested in evaluating the problem in a realistic scenario. The piece the literary equivalent of a reminder that one can harm oneself with a gun without ever actually discussing how one should implement gun safety.
NovemberWhiskey 5y ago
No mention of XACML?
samjs 5y ago
Well this was fun to see! I'm the CTO of Oso, where we're building Polar (the second of the links mentioned https://docs.osohq.com/ https://docs.osohq.com/). I have a few really minor nitpicks, so will try and make up for it by adding to the discussion :) First of all, it doesn't really make sense to talk about Datalog as a good language for authorization, because much like with Prolog there doesn't really exist a single implementation of it. OPA's language Rego is a datalog variant, and Polar started out as a Prolog variant (although it's not really recognisable as one any more). And that's an important point because otherwise it would be pretty reasonable to decide that: logic programming is good for authorization => you should go find the most battle-tested language out there and use that. For example, there's SWI Prolog [1] and Scryer Prolog [2] as two of my favourites. To me, the thing that is mind-blowing about logic programming, is (a) how powerful the paradigm is, and (b) how concisely you can implement a logic programming language. Take miniKanren [3] which is a full-blown logic language in a few hundred lines of code. In my mind, the original article makes a decent case that logic programming is a good fit for authorization. And just generally I love anyone bringing attention to that :) But in my opinion the reason logic programming is such a solid foundation for authorization logic is the pieces you can build on top of it. For Polar, we've added: - Types! So you can write authorization logic over your data types and help structure your logic. We've implemented this by simply adding an additional operator into the language that can check types - Authorization primitives like roles and relationships (RBAC and ReBAC). These are all backed by the logical rules, so can be easily extended with custom logic - And last but not least... the ability to convert authorization logic into SQL [4]. Which is done by having the language return constraints over any unbound (free) variables. To me this is what makes logic programming exciting for authorization. It gives you this small kernel of declarative programming, and gives you a ton of freedom to build on top. [1] https://www.swi-prolog.org/ https://www.swi-prolog.org/ [2] https://github.com/mthom/scryer-prolog https://github.com/mthom/scryer-prolog [3] http://minikanren.org/ http://minikanren.org/ [4] https://www.osohq.com/post/authorization-logic-into-sql https://www.osohq.com/post/authorization-logic-into-sql
- aafldkjfaljkdpr 5y ago
  Puzzled: why is the conversion to SQL either interesting (SQL being a logic language so if disregarding recursion[1] they should map straightforwardly[2]) or of business value? [1] yeah, CTEs, I know [2] yeah, words are cheap from my end, I know Edit: additionally, and for curiosity: the article covers use of datalog but no underlying security model (eg. consistency of access to resources so you don't have one way blocked to you but can go around via another route, as I know of one homebrew system where you could do that). How do you deal with that? I understand lattices can be used for this (TBH I have only done a little reading on these).
naasking 5y ago
Use good old CSP and model checkers: https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.172.9128 https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.172...
YeGoblynQueenne 5y ago
>> The other factor we need to consider is that the polynomial data complexity of Datalog is based on the most basic form, which doesn’t have function symbols (ie datatypes like lists) or arithmetic. Once you start adding such features (which almost all real-world Datalogs do), the data complexity inevitably goes up. The informal definition of Datalog is that it is a decidable subset of Prolog, or a pure set of Prolog, etc, but I think it's more accurate to say that datalog clauses are a subset of the definite clauses such that a definite clause, C, is datalog if and only if a) C has no functions other than constants and b) every variable in the head literal of C is shared with a literal in the body of C. For example, below, C is datalog, D and E are not: C = P(x,y) ← Q(x,z), R(z,y) % datalog D = P(x,y) ← Q(x,z) % z is not shared with head(D) E = P(x,y) ← Q(f(x),z), R(z,y) % f(x) is not a constant function. Note that Prolog programs are sets of definite clauses, but without the restrictions (a) and (b) of datalog. As the article points out, lists need functions, so for example p([H|T], H) is not datalog because [H|T] is a function, and for arithmetic n(s(0)) is not datalog because s(0) is a function. So what's up with functions? In logic programming a function is a function symbol followed by n terms, where n is the arity of the function symbol, so if f(x,y) is a function then f is a function symbol with arity 2. Unlike in imperative programming, functions in logic programming _are not replaced by their values_, instead the truth of a formula containing functions is calculated by substituting the variables in the function. So f(x) can become f(a), f(b) etc. where a and b are constants. Problem is, variables in logic programming can be substituted for arbitrary terms and functions themselves are terms, so given the function symbol f of arity 1 we can make an infinite number of functions: f(x), f(f(x)), f(f(f(x))), f(f(f(f(x)))), etc. That's one important reason for the undecidability of First Order Logic (FOL). Definite logic, the logic of definite clauses, which is a restriction of FOL, is _semi_ decidable, meaning that if a theorem doesn't have a proof, there is no way to know in finite time. Datalog doesn't have functions so it removes this particular source of undecidability. If, in addition to not having functions, the Herbrand Universe (the set of all constants) is finite, then datalog is decidable, informally because every proof can only replace the variables in a program with a finite set of constants, which means there's a finite set of proofs for every program. What about the requirement that the head literal shares variables with the body literals? That's to ensure that the entire datalog program can be ground. Datalog is evaluated "bottom up" meaning that literals in the body are ground before literals in the head, so in a clause like D above, even if Q(x,z) is grounded during evaluation, the variable y in the head of the clause cannot be grounded because it's not shared with the body. Which means that we can't prove that P(x,y) is a consequence of Q(x,z). In a clause like C, on the other hand, we can ground every variable by grounding the literals in the body and so bottom-up evaluation is possible. Bottom-up evaluation is desired because it avoids left-recursions and it makes the ordering of clauses irrelevant for the proof of a program, unlike in Prolog. This is an attractive property of datalog. Now, about functions, the Inductive Logic Programming community knows a few tricks to retain the decidability of datalog programs even with functions. The sneakiest such trick is "flattening" where functions are "hidden" away from the datalog clauses. For instance, instead of writing: member(X, [X|Xs]) ← ... With flattening we can write: member(X, Xs) ← head(Xs,X), ... Where "head" is defined as head([X|Xs],X). With flattening we can keep some parts of the program datalog and the rest definite, and so have our cake and eat it.
geal 5y ago
(biscuit author here) I like how that post points a crucial issue in authorization systems: how powerful and flexible should we make them? If you go towards flexibility, you get more complexity and possibly unexpected results. And they become hard to audit and explain. You can choose simple, single purpose systems, like a RBAC only authz backed by a SQL database. You write tight, easy to understand policies. But systems always grow beyond the bounds of those rules, and you end up with a lot of ad hoc rules, or role explosion. Datalog was a good tradeoff for Biscuit (https://www.biscuitsec.org https://www.biscuitsec.org): powerful enough to cover a lot of use cases, simple enough to be implemented the same way in multiple languages

68 points by triska 5y ago

Sure it is, because the language of Open Policy Agent, called Rego, is a Datalog variant. I find a researcher’s failure to mention this concerning.

0x0000000 5y ago
The second link in the article is https://www.openpolicyagent.org/docs/latest/policy-language/ https://www.openpolicyagent.org/docs/latest/policy-language/
Nullabillity 5y ago
The second sentence of the post links to OPA as an example of a system using Datalog for authz. Also, "X uses Y for Z" doesn't imply that Y is good at Z. It can be the start of an argument about how that choice is turning out for X, but it's in no way an argument by itself.
- flurie 5y ago
  My assertion is glib, but your response is wholly insubstantive. Can you to point out how this piece treats Rego as an actual example of a real-world Datalog? I don't see any link when mentioning real-world Datalogs. The fact that this piece makes no mention of it but provides a drive-by link to it suggests that the author is not actually interested in evaluating the problem in a realistic scenario. The piece the literary equivalent of a reminder that one can harm oneself with a gun without ever actually discussing how one should implement gun safety.

NovemberWhiskey 5y ago

No mention of XACML?

samjs 5y ago

Well this was fun to see! I'm the CTO of Oso, where we're building Polar (the second of the links mentioned https://docs.osohq.com/ https://docs.osohq.com/). I have a few really minor nitpicks, so will try and make up for it by adding to the discussion :) First of all, it doesn't really make sense to talk about Datalog as a good language for authorization, because much like with Prolog there doesn't really exist a single implementation of it. OPA's language Rego is a datalog variant, and Polar started out as a Prolog variant (although it's not really recognisable as one any more). And that's an important point because otherwise it would be pretty reasonable to decide that: logic programming is good for authorization => you should go find the most battle-tested language out there and use that. For example, there's SWI Prolog [1] and Scryer Prolog [2] as two of my favourites. To me, the thing that is mind-blowing about logic programming, is (a) how powerful the paradigm is, and (b) how concisely you can implement a logic programming language. Take miniKanren [3] which is a full-blown logic language in a few hundred lines of code. In my mind, the original article makes a decent case that logic programming is a good fit for authorization. And just generally I love anyone bringing attention to that :) But in my opinion the reason logic programming is such a solid foundation for authorization logic is the pieces you can build on top of it. For Polar, we've added: - Types! So you can write authorization logic over your data types and help structure your logic. We've implemented this by simply adding an additional operator into the language that can check types - Authorization primitives like roles and relationships (RBAC and ReBAC). These are all backed by the logical rules, so can be easily extended with custom logic - And last but not least... the ability to convert authorization logic into SQL [4]. Which is done by having the language return constraints over any unbound (free) variables. To me this is what makes logic programming exciting for authorization. It gives you this small kernel of declarative programming, and gives you a ton of freedom to build on top. [1] https://www.swi-prolog.org/ https://www.swi-prolog.org/ [2] https://github.com/mthom/scryer-prolog https://github.com/mthom/scryer-prolog [3] http://minikanren.org/ http://minikanren.org/ [4] https://www.osohq.com/post/authorization-logic-into-sql https://www.osohq.com/post/authorization-logic-into-sql

aafldkjfaljkdpr 5y ago
Puzzled: why is the conversion to SQL either interesting (SQL being a logic language so if disregarding recursion[1] they should map straightforwardly[2]) or of business value? [1] yeah, CTEs, I know [2] yeah, words are cheap from my end, I know Edit: additionally, and for curiosity: the article covers use of datalog but no underlying security model (eg. consistency of access to resources so you don't have one way blocked to you but can go around via another route, as I know of one homebrew system where you could do that). How do you deal with that? I understand lattices can be used for this (TBH I have only done a little reading on these).

naasking 5y ago

Use good old CSP and model checkers: https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.172.9128 https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.172...

YeGoblynQueenne 5y ago

>> The other factor we need to consider is that the polynomial data complexity of Datalog is based on the most basic form, which doesn’t have function symbols (ie datatypes like lists) or arithmetic. Once you start adding such features (which almost all real-world Datalogs do), the data complexity inevitably goes up. The informal definition of Datalog is that it is a decidable subset of Prolog, or a pure set of Prolog, etc, but I think it's more accurate to say that datalog clauses are a subset of the definite clauses such that a definite clause, C, is datalog if and only if a) C has no functions other than constants and b) every variable in the head literal of C is shared with a literal in the body of C. For example, below, C is datalog, D and E are not: C = P(x,y) ← Q(x,z), R(z,y) % datalog D = P(x,y) ← Q(x,z) % z is not shared with head(D) E = P(x,y) ← Q(f(x),z), R(z,y) % f(x) is not a constant function. Note that Prolog programs are sets of definite clauses, but without the restrictions (a) and (b) of datalog. As the article points out, lists need functions, so for example p([H|T], H) is not datalog because [H|T] is a function, and for arithmetic n(s(0)) is not datalog because s(0) is a function. So what's up with functions? In logic programming a function is a function symbol followed by n terms, where n is the arity of the function symbol, so if f(x,y) is a function then f is a function symbol with arity 2. Unlike in imperative programming, functions in logic programming _are not replaced by their values_, instead the truth of a formula containing functions is calculated by substituting the variables in the function. So f(x) can become f(a), f(b) etc. where a and b are constants. Problem is, variables in logic programming can be substituted for arbitrary terms and functions themselves are terms, so given the function symbol f of arity 1 we can make an infinite number of functions: f(x), f(f(x)), f(f(f(x))), f(f(f(f(x)))), etc. That's one important reason for the undecidability of First Order Logic (FOL). Definite logic, the logic of definite clauses, which is a restriction of FOL, is _semi_ decidable, meaning that if a theorem doesn't have a proof, there is no way to know in finite time. Datalog doesn't have functions so it removes this particular source of undecidability. If, in addition to not having functions, the Herbrand Universe (the set of all constants) is finite, then datalog is decidable, informally because every proof can only replace the variables in a program with a finite set of constants, which means there's a finite set of proofs for every program. What about the requirement that the head literal shares variables with the body literals? That's to ensure that the entire datalog program can be ground. Datalog is evaluated "bottom up" meaning that literals in the body are ground before literals in the head, so in a clause like D above, even if Q(x,z) is grounded during evaluation, the variable y in the head of the clause cannot be grounded because it's not shared with the body. Which means that we can't prove that P(x,y) is a consequence of Q(x,z). In a clause like C, on the other hand, we can ground every variable by grounding the literals in the body and so bottom-up evaluation is possible. Bottom-up evaluation is desired because it avoids left-recursions and it makes the ordering of clauses irrelevant for the proof of a program, unlike in Prolog. This is an attractive property of datalog. Now, about functions, the Inductive Logic Programming community knows a few tricks to retain the decidability of datalog programs even with functions. The sneakiest such trick is "flattening" where functions are "hidden" away from the datalog clauses. For instance, instead of writing: member(X, [X|Xs]) ← ... With flattening we can write: member(X, Xs) ← head(Xs,X), ... Where "head" is defined as head([X|Xs],X). With flattening we can keep some parts of the program datalog and the rest definite, and so have our cake and eat it.

geal 5y ago

(biscuit author here) I like how that post points a crucial issue in authorization systems: how powerful and flexible should we make them? If you go towards flexibility, you get more complexity and possibly unexpected results. And they become hard to audit and explain. You can choose simple, single purpose systems, like a RBAC only authz backed by a SQL database. You write tight, easy to understand policies. But systems always grow beyond the bounds of those rules, and you end up with a lot of ad hoc rules, or role explosion. Datalog was a good tradeoff for Biscuit (https://www.biscuitsec.org https://www.biscuitsec.org): powerful enough to cover a lot of use cases, simple enough to be implemented the same way in multiple languages