Proividing capability proofs unambiguously

[Gozala]

I am starting to dislike current structure of UCANs in which you have set of capabilities and set of proofs with no direct connections between them. Which requires a constraint solver on the verifier end which may need to explore several routes to before it can conclude if claimed capability is valid.

Above alone had been mild annoyance which resulted in more complicated code, however lately we're running into situations where certain capability e.g { can: 'store/add', with: 'did:key:user' } may require proofs e.g. that did has valid email account expressed with capability { can: 'access/identify', with: 'did:key:user' } which in turn depend on two other proofs:

1. That did:key:user claimed to have owned email user@email.to (issued by user DID)
2. That did:key:verifierverified above claim.

More simply relation between capabilities A, B, C, D is

  A
  |
  B
 / \
C   D

Unfortunately at the UCAN level relation between A, B, C and D is not captured and is unclear. Lack of that relation is also why we need a constraint solver.

What If ?

What if instead of hoisted proofs each capability linked to a proof directly something like ucan_cid/capability_id ? That would:

1. Remove need for constraint solver as path would be evident through links.
2. Capabilities can be more precisely be defined with JSON schema, types etc...

[expede]

@Gozala this is something that's come up a few times from implementers. I'm unclear if it's a good idea for the following reasons:

1. It adds complexity for the consumer
2. More things can go wrong in the token (e.g. point at the wrong proof)
3. If a proof is revoked, but they have another overlapping one, their UCAN is invalid, despite technically having that capability
4. It doesn't respect Postel's Law ("be liberal in what you accept, and conservative in what you send")

There is irreducible complexity in here, so we can push that into the user interaction, or into the library. My gut instinct is to always err on the side of making things as flexible for users as possible, and biting the bullet in the library.

That said, I'm not the final word on this spec, and am open to discussing this change further! Maybe it's the right tradeoff; it's possible!

we need a constraint solver

This is surprising to me! Tell me more about this. Are you using a full blown constraint solver like SMT, or a hand-rolled mini-matcher?

Unfortunately at the UCAN level relation between A, B, C and D is not captured and is unclear

Tell me more about this? To make sure that we're on the same page, assuming that the relation points upwards, A can only rely on B, and A will have no idea that C or D exist. Your validator for A would have no choice but to look at B, and B would look at C and/or D (depending on the exact situation). It's strictly recursive.

You mad mentioned a confusion a few weeks back about how capabilities are accessed in a chain, and this could potentially be the same thing? UCANs can only access their direct proofs, not proofs-of-proofs down the chain — for security reasons. i.e. they have access to multiples via breadth but not depth.

[expede]

Capabilities can be more precisely be defined with JSON schema, types etc...

I'm also not clear on how would this improve the JSON schema or types, but would love to hear your thoughts.

Do you mean with the assumption of the exact capabilities that you'll find in the proof. If you have a UCAN that has multiple capabilities in it, will you point to the exact cap inside that token, too? Something like Qm123#cap-4?

In terms of types, the current idea is that the library provides a parser: it's a function from less structured data to more structured data, and can stack those transformations.

[Gozala]

This sounds like a rights amplification use case, yes? https://github.com/ucan-wg/spec/#54-rights-amplification

It is

[Gozala]

I'm also not clear on how would this improve the JSON schema or types, but would love to hear your thoughts.

I find myself having to describe what proofs are required by specific capability, and inability to specify this really annoying e.g. I would love to have a way to describe it something like

type A<T> {
  with: T
  can: “do/A”
  proof: [Can<B<T>>]
}

type B<T> {
  with: T
  can: “do/B”,
  proof: [Can<C<T>>, Can<D<T>>]
}

Above makes it clear that capability A requires proof with capability B which in turn proofs with capabilities C and D. Right now these relations hard to impossible to capture.

[Gozala]

Do you mean with the assumption of the exact capabilities that you'll find in the proof. If you have a UCAN that has multiple capabilities in it, will you point to the exact cap inside that token, too? Something like Qm123#cap-4?

I’m not sure I fully understand this question. I do imply however that yes each capability will refer to specific capabilities in the specific proofs. In which case dicts of caps and proofs might work better than arrays, but that is whole another subject.

I would think that it would be something like ./prf[2]/att[3] which would be my third proofs fourth capability is a proof for this specific capability. That said IPLD paths would indeed be more preferable so something like Qm123#cap-4 would work even better.

Anyway I don’t have strong opinions of how it could be represented. Mostly I’ve been annoyed but how much validator needs to know and feeling like issuer already has to know it so why not keep validator simple and domain agnostic.

[andrewzhurov]

These types resemble UCANs, one per type!
I feel you on amplification introducing ambiguity. As well as it accidentally attenuates #171
Perhaps a solution is to have just one Capability per UCAN.
Amplification then becomes a collection of UCANS.
E.g., [C1, D1]. Here C1 and D1 are individual delegations of C and D.
I.e., just passing around multiple UCANs.

On the running example, detailed:
C is the capability to compute
D is the capability to store
B is compute&store, with compute limit of 10 seconds
A is compute&store, with compute limit of 10 seconds, store limit of 1 megabyte

Then, in order to express A with explicit capability->proof, we may issue the following UCANs:

{
   "bafy...compute":
   {"with": "compute resource URI",
    "can": "compute/any"
    "proof": "bafy...someProof1"},

   "bafy...store":
   {"with": "store resource URI",
    "can": "store/any",
    "proof": "bafy...someProof2"},

   "bafy...computeLimited":
   {"with": "compute resource URI",
    "can": "compute/any",
    "caveats": [{"computeTimeout": [10 "seconds"]}]}

   "bafy...storeLimited":
   {"with": "store resource URI",
    "can": "store/any",
    "caveats": [{"storageLimit": [1 "mega" "byte"]}]
    "proof": "bafy...store"},
 }

And A as

["bafy...computeLimited",
 "bafy...storeLimited"]

[expede]

Also going to CC @matheus23 to bring his voice in to the conversation.

IIRC he has also described a similar idea in the past where we point at specific CIDs (and to which I made the same argument as above about who has to handle the irreducible complexity). Tell me why I'm wrong! 🙏

[Gozala]

I would like to address some of the notes

1. It adds complexity for the consumer

I am not sure I agree although maybe we’re thinking about different actors behind “consumer”. I’m thinking of actor that handles invocation, in which case it’s actually less complex because it is told exactly what the proofs are as opposed to having to find that out.

2. More things can go wrong in the token (e.g. point at the wrong proof)

Maybe. Although I do not find to be a compelling argument. Sure code creating derived token has more opportunity to mess up, but then again just the same it could forget to include necessary proofs, in which case UCAN would be invalid and error would be less clear as there could be many paths that failed and the right path would not even be present.

3. If a proof is revoked, but they have another overlapping one, their UCAN is invalid, despite technically having that capability

This is the case when user may have two or more capability sets that would have satisfied same claim. It is true, however one could also claim same capability multiple times pointing to different proofs. It would be a lot more verbose, but I’d still argue a lot more clear still.

4. It doesn't respect Postel's Law ("be liberal in what you accept, and conservative in what you send")

Fair enough. It would be a lot easier to update validation code than it is to reissue all the malformed tokens produced by invalid issuer code.

[matheus23]

3. If a proof is revoked, but they have another overlapping one, their UCAN is invalid, despite technically having that capability

This is the case when user may have two or more capability sets that would have satisfied same claim. It is true, however one could also claim same capability multiple times pointing to different proofs. It would be a lot more verbose, but I’d still argue a lot more clear still.

If you allow claiming the same capability multiple times by pointing to different proofs, and a single "invalid" proof is considered OK, then you need to have what you call the constraint solver again.

[matheus23]

Oh right. I just remembered #21.

I disambiguating parenthood vs. delegation as an intent already goes a big step towards a simpler capability delegation checker.

If that lands, maybe capability delegation checking becomes "easy enough"? @Gozala

[Gozala]

To be clear it's not the complexity that bothers me, but ambiguity rather. I keep finding myself having to say something like { can: 'store/upload' } requires either proof with { can: 'access/identify' } or { can: 'access/authorize' }

Which leads me to wishing I could express that unambiguously e.g.

type Upload {
   can: 'store/upload'
   // with: ...
   evidence: Link<Identify | Authorize>
}

type Identify {
  can: 'access/identify'
  // ...
}

type Athorize {
  can: 'access/authorize'
  // ...
}

But then again I do realize it has downsides a per

It doesn't respect Postel's Law ("be liberal in what you accept, and conservative in what you send")

Fair enough. It would be a lot easier to update validation code than it is to reissue all the malformed tokens produced by invalid issuer code.

[expede]

To be clear it's not the complexity that bothers me, but ambiguity rather. I keep finding myself having to say something like { can: 'store/upload' } requires either proof with { can: 'access/identify' } or { can: 'access/authorize' }

also

type A {
with: T
can: “do/A”
proof: [Can<B>]
}

type B {
with: T
can: “do/B”,
proof: [Can<C>, Can<D>]
}

Just picking up this thread again @Gozala. I'm still confused about what you're trying to achieve specifically. Validators are unambiguous. By "unambiguous" do you perhaps mean statically?

Let me paraphrase, to see if I can get closer to what you're looking for:

There is an action store/upload, which can be proven by either access/identify or access/authorize. You want to express this generically and statically so that you could do things like abstract over the type of a capability with generics. Is that about right?

If so, it's true that you're constrained by the fact that TypeScript lacks open type families. That said, you also won't be able to express this for the resources, because they have URIs that often depend on runtime values. The example that you gave above seems reasonable. You should be able to get pretty close when constructing. These aren't generic, but a concrete representation seems doable:

type Parenthood = null | undefined;

interface Upload {
  can: 'store/upload',
  proof: Parenthood | Upload | Identify | Authorize
}

interface Identify {
  can: 'access/identify',
  proof: Parenthood | Identify
}

interface Authorize {
  can: 'access/authorize',
  proof: Parenthood | Authorize
}

const exampleTerm : Upload = {
  can: 'store/upload',
  proof: {
    can: 'access/identify',
    proof: null
  }
}

type Cap<T> = {with: URI} & T

Of course at validation time, the parser would need to go down to an Either/Result type, as parsers tend to do. The above seems too simple, so I'm definitely missing something big from your example/use case.

Also possibly worth noting that passing the with: T all the way through the chain likely would need to be rephrased to handle changing that T to include extension/amplification cases (classic example: has access to two resources: can opener and can)

[UPDATE: I was actually able to get very close to type families using field accessors at the type level in the TypeScript playground]

[andrewzhurov]

If a proof is revoked, but they have another overlapping one, their UCAN is invalid, despite technically having that capability

This is the case when user may have two or more capability sets that would have satisfied same claim. It is true, however one could also claim same capability multiple times pointing to different proofs. It would be a lot more verbose, but I’d still argue a lot more clear still.

If you allow claiming the same capability multiple times by pointing to different proofs, and a single "invalid" proof is considered OK, then you need to have what you call the constraint solver again.

While it's fairly pointed that amplification UCANs with some, but not all, proof UCANs that grant overlapping capabilities revoked would still be considered valid, as there are proofs left, it makes me wonder whether bundling is a good ability to have in the first place.

Consider an example of Compute+Store provider issuing to Alice "compute+store" UCAN, C+S, and Store2 provider issuing "store" UCAN, S2.
Then, if Compute+Store provider would to revoke S, "store" capability of "compute+store", Alice could issue an equal in capabilities UCAN C+S+S2 from her C+S + S2 UCANs.

While C+S+S2 would grant the desired "compute" and "store" capabilities, amplification does make it harder to track where capabilities come from (validator would check: does "store" come from C+S? C? no. S? yes, but it's been revoked. does it come from elsewhere? S2? yes, valid) - the subject of this discussion.

I'd further argue that allowing to have multiple capabilities in a UCAN poses a similar difficulty.
In order to validate that UCAN attenuates some capabilities from its one and only proof UCAN, validator would first need to match them with their corresponding capabilities from the proof.
This is an argument in favor to allow only one capability per UCAN.
It's not compelling on its own, but perhaps we could further consider tradeoffs of this approach.

Another thing to note from the example above is how S UCAN would hang in proof chain if Alice would to wish to still use the left C capability, which's been unfortunately to her bundled and provider as part of C+S.
Perhaps we better off authorizing capabilities individually, that would more fine-grained management.
Amplification then could be expressed as a collection of UCANS, as wondered about in the comment above.

The example above would look like:

Where all capabilities are shared as separate UCANs, and when S got revoked, Alice switched from using [C, S] collection over to [C, S2].

[Gozala]

This is surprising to me! Tell me more about this. Are you using a full blown constraint solver like SMT, or a hand-rolled mini-matcher?

Hand written one. Maybe calling it a constraint solver is overstatement, but it was non trivial code already and introducing relations between specific capabilities is making it even more complicated.

It just seems that issuer of the token should be in much better position to link proof chains than validator which otherwise does not really need to hold domain specific logic.

[expede]

it was non trivial code already and introducing relations between specific capabilities is making it even more complicated

Is this in ts-ucan? Or are you writing your own validation functions in your application? I guess these validators (ucan-wg/ts-ucan#21) haven't been written yet, but the ability to hand the library validation code for a single validation step function would be pretty straightforward, no? (Kind of like using a recursion scheme)

Maybe for clarity: we're discussing if this check should happen at creation-time or a validation-time. FWIW, I agree that it's always easier for the library author to have hardcoded data (but there's tradeoffs to doing that).

[Gozala]

Mostly it's me wishing I could encode dependencies unambiguously as opposed to have several paragraphs of text explaining what capability depends on what other capability.

And yes there are tradeoff I have not considered until you've pointed them out.

[Gozala]

Tell me why I'm wrong! 🙏

I do not know if you are wrong, but my primary sentiment is issuer knows what proofs it needs to provide when granting some capability, but it is does not encode that knowledge so validator needs to go and figure on it’s own. To do so it also needs to have more domain knowledge than it otherwise needs.

That said, your arguments helped me recognize the fact that improving validator would be a lot easier & cheaper than to cause mass token rotation, so maybe more ambiguity is better.

For what it’s worth spec does not stops us from adding extra fields in our capabilities to link to a relevant proofs.

[expede]

@Gozala actually now that I'm thinking through this more, how is this different from a unique resource? You can do things like this:

{
  with: "foo:bar/baz",
  can: "quux/write",
  prf: "QmbFMke1KXqnYyBBWxB74N4c5SBnJMVAiMNRcGu6x1AwQH" // Proof CID
}

or

{
  with: "foo:bar/baz",
  can: "quux/write",
  unq: "mynonce123" // Made unique by nonce, so can find by matching on nonces alone
}

But also can manage this directly in the resource to make it unique (maybe overloading that is a bad idea?)

  //            Nonce in the URI hash
{ //                vvvvvvvvvvv
  with: "foo:bar/baz#mynonce123",
  can: "quux/write"
}

[Gozala]

I'm not sure I fully understand matching by nonce idea, first one is more more or less what I had in mind, except with more exact selector

{
  with: "foo:bar/baz",
  can: "quux/write",
  proof: ["QmbFMke1KXqnYyBBWxB74N4c5SBnJMVAiMNRcGu6x1AwQH/1"] // Second capability in Proof with that CID
}

[Gozala]

Actually maybe something even simpler like

{
  with: "foo:bar/baz",
  can: "quux/write",
  per: [[0, 1]] // Second capability in of the first Proof
}

[matheus23]

how is this different from a unique resource?

I think the difference in practice would be support for this in UCAN libraries. You can have anything additional in capabilities, but having UCAN libraries support that kind of thing is dependent on what the spec says, IMO.

[expede]

I'm not sure I fully understand matching by nonce idea

This was just meant to show that the matching nonce simply notes that the index is arbitrary, so you don't need the lengthy path from the CID (though a CID is a perfectly fine index).