tarcieri
commented
5 years ago I haven't had time to read through the spec yet, but I can attempt to describe an approach which I believe drove part of it.
From a practical perspective, I think it's important to clearly separate authority conferred upon a particular principal in an access control decision from "caveats". There is a hugely important reason to do this: user experience.
There are many ways to represent an "all caveats" construction: a set intersection, a logical disjunction (which when modus ponens is added gives you a logic for expressing third party caveats), or an authorization program, but when an access control decision fails, you need to answer "why" in a way that humans can actually understand, i.e. in a prose description.
For programmers deploying these credentials, one thing is incredibly clear to me at least from the failure of Macaroons: the access control calculation needs to be abstracted away from the programmer. In "OSS Macaroons" this was largely left as an exercise to the end-user to solve in application level code. That's awful.
Ideally I think verifying the credential involves the programmer instantiating a verification keyset and then calling a verification function which takes the credential, a set of "facts" about what is the credential bearer is proposing to do, such as a resource to be accessed and an action to be performed upon it, and potentially a big old bag of ugly ambient authority (what is their IP address, what country are they coming from, what is the authentication system's confidence score that they are on a secure terminal and have not recently been exhibiting indications of compromise).
As I've been discussing with @Geal, my personal preference for this now is authorization programs, although ones which are perhaps more in the style of Martín Abadi than Nick Szabo.
I'm talking about languages that are roughly Prolog-ish (Abadi's Binder and Open Policy Agent are two examples). To the extent the Macaroons paper was prescriptive about a specific verification logic (most of which was not ever implemented by the OSS community), a system based on authorization programs is more flexible, and can better express intent from the practical/human side.
They are certainly capable of expressing boolean algebras, but also Prolog-like queries, and with those it's possible to write programs that can be compiled into prose or diagrams and attempt to give a reasonable explanation of the policy it's trying to express.
Concretely to do this we need to separate positive authority from restrictions/caveats, and by simply doing that, authority amplification can be avoided, and also we'll end up with an authorization decision a developer or even an end user might have a snowflake's chance in hell of comprehending (which is a diss on the incomprehensibility of past systems, not users).
To do that, instead of saying "everything is a caveat", we can look at the initial authority conferred at the time the token was minted as a set of facts (although in my descriptions, I have generally preferred to use the word "authority" for this set), and then describe the caveats/restrictions as a set of rules which are the logical inverse of how Macaroons restrictions would normally work (which, IMO, are incredibly redundant).
As an example, if Macaroons would have you express something like this:
id: [1, 2, 3]id: [1, 3]id: [3]
For an authorization program example, I will use a sort of Prolog-like pseudocode, and to really screw with your brain I'm going to invert the capitalization because it drove me insane in Erlang:
Authority ("fact" encoded in the credential)
ID: [1,2,3]
Rules (caveats/restrictions)
authorized0(id) <- ?ID(id)authorized1(id) <- id != 2 && authorized0(id)authorized2(id) <- id != 1 && authorized1(id)
Why write things this way instead of the Macaroons way? In addition to being more expressive (a language like this is expressive enough for all of the hidden logic decisions going on in Macaroons proofs, but in a way that's written in the same language a programmer might use), as I mentioned earlier it's potentially conducive to prose or diagrammatic translations.
Here's a strawman stab at a couple examples:
authorized2(0)"This credential is only authorized to access id: 1, 2, 3, but you are attempting to access id: 0"
authorized2(2)"This credential cannot access id: 2. It was originally granted access to id: 1, 2, 3, but a caveat denies access to id: 2"
Each of these rules could potentially have some metadata / a "comment" about why it's there, and the credential could also come with a set of "claims" (i.e. identity information) about its provenance which could be incorporated into a prose description. It wouldn't figure into the access control decision, but it could be immensely helpful for debugging.
For example, let's say we have this user database:
Users
- 100: Alice
- 101: Bob
- 102: Carol
We initially issue the credential to Alice:
[claims]
uid = 100
[authority]
ID = [1, 2, 3]Alice wants to delegate her credential to Bob, but doesn't want Bob to be able to access id: 2. So she encodes:
caveat: authorized1(id) <- id != 2 && authorized0(id)
claims: uid = 101Bob then delegates to Carol, without the authority to call 1:
caveat: authorized2(id) <- id != 1 && authorized1(id)
claims: uid = 102Now we have:
authorized2(0)"This credential is only authorized to access id: 1, 2, 3, but you are attempting to access id: 0"
authorized2(2)"This credential cannot access id: 2. It was originally granted to Alice with access to id: 1, 2, 3, however a caveat restricting access to id: 2 was added before she delegated to Bob."
divarvel
KellerFuchs
Compared to macaroons, the attenuation syntax seems to allow capabilities extension, whereas macaroons structurally guarantee that no extension can happen (by relying on boolean algebra).
The example features diff-ilke attenuation (instead of general properties the query must satisfy, attenuations are modifications to the token's rule set. In isolation, each attenuation rule cannot be checked. This implies that a reduction has to happen before the receiving service can check if the token is okay for a given request. On the contrary, macaroons verifiers check each caveat in isolation.
This leads to an important question: "who's responsible for the reduction?".
Compare this to macaroons, where we have the best of both worlds: syntax is not constrained and attenuation is proved by basic boolean algebra rules.
Unless biscuit ships with a rock-solid attenuation language, with structural proofs that expansion is impossible (in the current spec, this implies amongst other things computing regexes intersections), it means that the burden of proving attenuation is transferred to the owner, which would make it a dangerous token to use.