New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Example logic queries #11
Comments
Example of a authentication server having a very broad token that is attenuated before being given to a user. Also showing the idea of having the authority defined by rules:
With the ambient facts Could such a token give more rights accidentally? |
Using constraints:
The verifier can present ambient facts like the current time or source IP address. Depending on the type of a value, we could have these kind of operations:
Revocation tokens:
The verifier would have revocation lists in which we can check the inclusion of a token |
a token that could be used by various microservices (using hosting as an example), trying to deploy an application:
Note: from this example I see that some facts could be marked as unique. If the In the billing service:
The billing service checks that the organisation has the right to deploy this application and that it has enough credits. On the hypervisor:
the verifier query would fail because the RAM limit for an app of this organisation is 2GB, lower than the requested 4GB. Constraints can express useful properties like those limits on available credits or memory usage, but maybe those should not be verified inside the token. It requires that the verifier loads facts from unrelated organisations, making the whole query a lot slower. |
Glad to see you exploring authorization languages! One small note: your examples use In my experience that's a classical source of audience confusion attacks. However, audience confusion generally arises in these scenarios due to logic bugs. So perhaps a sufficiently well-designed authorization language can avoid them. That said, an alternative I prefer is to cryptographically bind the credentials to audiences. With traditional Macaroons this usually involves obtaining a third party caveat from an online service. With a public-key construction, I think you can invert that relationship, and services can present their "SSO credential" which the target service can verify, mint a symmetric credential, and the "SSO credential" can optionally include a third party caveat which requires a discharge from the client for any client-imposed restrictions (this is the "Madeleines" idea I've referred to elsewhere). Probably a bit of a red herring for authorization languages. Otherwise this looks interesting. |
I like how it looks, because it allows both the token (through the authority part) and the service (through ambient facts) to provide scope. This is a net benefit over the implicit way it was done with macaroons, both in terms of clarity but also in terms of flexibility. With explicit scope provided during token validation (either in the token authority or by the service), I think it would sidestep all the confusion common with macaroons (since macaroons rely on implicit scoping thanks to the identifier). I'll work on typing judgments based on these examples, to see what the types ystem could look like. |
We seem to be using "confusion" two different ways. I'm using it in the context of a "confused deputy", or more generally an "audience confusion attack". See the following example: https://blog.intothesymmetry.com/2017/10/slack-saml-authentication-bypass.html The Macaroons approach provides a cryptographic audience binding through the use of symmetric cryptography. This avoids confused deputy attacks, because if something is wrong, the credential fails to verify. Debugging this may be... confusing... but it does fail closed, as opposed to systems where if audiences are deployed incorrectly, it provides lateral movement between services and escalation of privilege. |
I was wondering about providing scopes for facts to avoid these kinds of issues. So there could be these scopes:
|
I should have looked it up indeed. Thanks for the link, I'll check it out.
…On Thu, Feb 7, 2019 at 3:49 PM Tony Arcieri ***@***.***> wrote:
With explicit scope provided during token validation (either in the token
authority or by the service), I think it would sidestep all the confusion
common with macaroons (since macaroons rely on implicit scoping thanks to
the identifier).
We seem to be using "confusion" two different ways. I'm using it in the
context of a "confused deputy
<https://en.wikipedia.org/wiki/Confused_deputy_problem>", or more
generally an "audience confusion attack". See the following example:
https://blog.intothesymmetry.com/2017/10/slack-saml-authentication-bypass.html
The Macaroons approach provides a cryptographic "audience" binding through
the use of symmetric cryptography. This avoids confused deputy attacks,
because if something is wrong, the credential fails to verify. Debugging
this may be... confusing... but it does fail closed, as opposed to systems
where if audiences are deployed incorrectly, it provides lateral movement
between services and escalation of privilege.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#11 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAKk8_dTRrD18qhymebNDXXfASZBsdkZks5vLDzrgaJpZM4ajw22>
.
|
A more typical example of audience confusion is X.509 hostname verification. Certificates are issued within the scope of a particular SAN/set of SANs which describe the audience of that particular certificate. Unfortunately, these constraints (or other constraints) are often ignored, and certificates are treated as providing authority over all sites on the Internet. All that said: I think the big problem is e.g. X.509 libraries end up implementing that same sort of logic over and over again in slightly different ways. There is no One True Spec of how to do X.509 hostname verification (I have implemented RFC 6125 and it is littered with "MAYs"). One of the things I like the most about authorization languages is they provide a single place to focus efforts on getting the verification logic correct. @Geal your "scopes" are definitely in line with what I'm thinking, although I used different words. Nobody can agree on the words! I was generally using the word "context" for what you describe as "verifier scope" and "ambient scope". They are indeed two separate things, and I tried to recognize the separateness of ambient authority. "Context" has its own overloaded meaning in OCap though (e.g. "user context", which is more like "authority scope" in your definition). SegWit uses the term "witness data" for what you're describing as "authority scope", i.e. witnesses to an NP assertion (within the context of a proof of knowledge). tl;dr: naming things is hard, and I have no answers 😉 |
the one who writes the spec defines the words, however bad they MAY or MUST be 😆 |
I translated most of those examples to my small datalog implementation: https://github.com/Geal/dataexponential/blob/master/src/biscuit.rs#L96-L370 The types are a bit annoying to manipulate directly, but I'll test making a nice API on top (if I'm evil I might even make a text representation that compile to those types).
The symbol type is an implementation detail I tested: in my first implementation, everything was basically strings (fact name, values, etc), so I added an external symbol table that maps strings to numbers. |
the revocation id pattern requires a bit more:
See Geal/dataexponential@1ffc292 for the implementation |
the logic language has sufficiently evolved now, closing this |
with @clementd-fretlink, we've been looking at a datalog like language to express caveats.
Here are some ideas that emerged:
Current questions:
To make it easier to reason about this language, I propose that we write some example facts, rules and queries in that issue.
First example:
With
resource(file1), operation(read)
as ambient facts,caveat1
succeeds becauseresource(file1) & operation(read) & right(file1, read)
is true,caveat2
succeeds because the factresource(file1)
succeeds.With
resource(file1), operation(write)
,caveat1
fails butcaveat2
succeeds.With
resource(file2), operation(read)
,caveat1
suceeds butcaveat2
fails.The text was updated successfully, but these errors were encountered: