cosmos / ibc

Interchain Standards (ICS) for the Cosmos network & interchain ecosystem.
Other
924 stars 382 forks source link

ICS 23: Standard accumulator #57

Closed cwgoes closed 5 years ago

cwgoes commented 5 years ago

Define required functions and their properties for the kind of cryptographic accumulator which IBC state inclusion proofs will require. Any accumulator which instantiates these properties (e.g. Merkle tree proofs) could be used with IBC and provide the usual safety guarantees. Different accumulators will have different performance characteristics, proof sizes, verification times, and possibly trusted setup assumptions (e.g. an RSA accumulator).

liamsi commented 5 years ago

I would be happy to help out with this / work on this. Feel free to assign me.

cwgoes commented 5 years ago

Thanks @Liamsi!

My thoughts so far:

  1. Datastructures
    1. AccumulatorRoot (opaque bytes)
    2. AccumulatorProof (opaque bytes)
    3. type Key = []byte
    4. type Value = []byte
  2. Functions
    1. verify :: AccumulatorRoot -> AccumulatorProof -> Key -> [Value] -> Bool

Arguably key and value shouldn't be separated here, but instead be a tuple, and the accumulator can just verify inclusion of an arbitrary []byte member - if that's more standard in the cryptographic literature, we should do that and then note the key, value tuple serialization requirements.

We do need some sort of lexicographic sorting, though, since we need range proofs / exclusion proofs.

cwgoes commented 5 years ago

The paper on RSA accumulators here might provide solid primitive definitions.

edit: Maybe better is this, page 6.

We should include optional BatchVerify for multiple values (or key-value pairs), which will make multiple-IBC-packet-proofs faster, but it can be optional (if the accumulator implements it, the packet handler can use it).

mossid commented 5 years ago
liamsi commented 5 years ago

Thanks for the input @cwgoes @mossid!

Especially

edit: Maybe better is this, page 6.

looks valuable!

Arguably key and value shouldn't be separated here, but instead be a tuple, and the accumulator can just verify inclusion of an arbitrary []byte member - if that's more standard in the cryptographic literature, we should do that and then note the key, value tuple serialization requirements.

Yes, I do not think it is common to separate those. I think that is because not every merkle tree is thought of as a key-value store (e.g. CT logs are more "list/array-like" than "map-like").

We do need some sort of lexicographic sorting, though, since we need range proofs / exclusion proofs.

Are range proofs an explicit requirement here? Or do we only need exclusion/non-membership proofs? In sparse merkle trees for instance, exclusion proofs are just an inclusion proof, which proves the included leaf or value is empty. In other words, does it make sense to have two functions instead?

cwgoes commented 5 years ago

Yes, I do not think it is common to separate those.

Let's avoid doing it here then.

Are range proofs an explicit requirement here?

No. They can enable certain batching downstream (e.g. in packet verification), so we should include them as an optional function, and the packet verification algorithm can use batch verification if the accumulator for that IBC connection supports it.

ValarDragon commented 5 years ago

Are you sure that accumulators suffice for light client proofs? I think light client proofs ought to be standardized on vector commitment schemes?

Namely, I think light clients desire a map, not a set. (In this sense, something list/array like is a map from integers to values)

cwgoes commented 5 years ago

Namely, I think light clients desire a map, not a set. (In this sense, something list/array like is a map from integers to values)

Often that may be useful, but I don't think it needs to be a requirement, since the IBC handler can insert values in a certain known order. Is there a particular verification case you're thinking of?

ValarDragon commented 5 years ago

There is no order guaranteed on accumulators. For example, accumulator(x_1, x_2) can equal accumulator(x_2, x_1). In fact, this is the case for an RSA accumulator.

cwgoes commented 5 years ago

There is no order guaranteed on accumulators. For example, accumulator(x_1, x_2) can equal accumulator(x_2, x_1). In fact, this is the case for an RSA accumulator.

That's right, but the IBC handler can decide to only ever insert in the order x_1, x_2, x_3, so if x_2 is included the verifier can assume x_1 has also been, and if x_2 is proved to be excluded then the verifier can assume x_3 has not been included either.

(we're assuming correct IBC handler behaviour anyways)

ValarDragon commented 5 years ago

I'm confused. Is the scenario your proposing that a verifier is given a commitment, and then a proof that x_2 is not included, and that they can then infer that x_3 is not included as well? I don't see how this is a guarantee.

cwgoes commented 5 years ago

Yes, because the verifier can assume (does already assume) correctness of the IBC handler on the sending chain, so the accumulator itself doesn't need to provide the ordering guarantee.

(although vector commitments could still be more efficient etc.)

ValarDragon commented 5 years ago

How is x_3 different from any byte string occurring lexicographically after x_2? You can't state that since x_2 isn't included, that no string lexicographically greater than x_2 is included.

cwgoes commented 5 years ago

How is x_3 different from any byte string occurring lexicographically after x_2? You can't state that since x_2 isn't included, that no string lexicographically greater than x_2 is included.

You could state that, if the IBC handler only ever inserted bytestrings in lexicographically increasing order. We're concerned about specific bytestrings, of course, with e.g. a packet sequence number included in the first part of the value.

ValarDragon commented 5 years ago

This isn't true, unless you assert that IBC inserts every bytestring in lexicographic order. (There is no bytestring less than a certain bound omitted)

This is the reason why: Consider an accumulator of {1, 5, 7}. 2 is not in this set, however you cannot then conclude that 5 and 7 are not parts of this set, no matter what guarantees you have on insertion order.

cwgoes commented 5 years ago

This isn't true, unless you assert that IBC inserts every bytestring in lexicographic order. (There is no bytestring less than a certain bound omitted)

This is the reason why: Consider an accumulator of {1, 5, 7}. 2 is not in this set, however you cannot then conclude that 5 and 7 are not parts of this set, no matter what guarantees you have on insertion order.

Ah sure, bad example. In the case of IBC we can expect every sequence number to be inserted in lexicographical order.

ValarDragon commented 5 years ago

Cool, glad we sorted that out. I still don't think accumulators suffice. There are two distinct cases that remain:

cwgoes commented 5 years ago

IBC for proving elements existence in the state tree: In this case, this property does not apply.

The ordering property does not apply, but we don't need vector commitments to prove inclusion of a particular (key, value) pair, a regular inclusion proof will do that. What case do you mean?

IBC on packets w/ sequence numbers: I agree that accumulators suffice if you assume that all the leaves are constructed honestly, however not all lite clients assume this (e.g. Coda), and this doesn't work for reasoning about the other chain.

Agreed.

(to be clear - I think vector commitments are great and will write a version of the verification algorithm that uses them - I just don't think they should be required)

ValarDragon commented 5 years ago

There aren't key value pairs in an accumulator. An inclusion proof on an accumulator only checks if a value is in a set, there is no key.

cwgoes commented 5 years ago

There aren't key value pairs in an accumulator. An inclusion proof on an accumulator only checks if a value is in a set, there is no key.

You can insert a (key, value) tuple as the accumulator value, and check membership of that (key, value) tuple - or check a Merkle path at a particular key, as in a sparse Merkle tree for example.

ValarDragon commented 5 years ago

check a Merkle path at a particular key, as in a sparse Merkle tree for example.

A merkle tree is a vector commitment, its not in the set of accumulators that aren't vector commitments!

Consider the following accumulator: Let tuples be (key, value) pairs. {(0, 1), (0, 2), (1, 1)}. You could try to lookup the key 0, but someone could return either (0,1) or (0, 2) validly. You could also try to prove that there is no key 1, by saying (1, 3) isn't included.

Accumulators don't have key value pairs, they only have distinct values. I think you want these vector commitment properties onto them (key-binding), hence why I think it ought to actually be vector commitments.

cwgoes commented 5 years ago

Consider the following accumulator: Let tuples be (key, value) pairs. {(0, 1), (0, 2), (1, 1)}. You could try to lookup the key 0, but someone could return either (0,1) or (0, 2) validly. You could also try to prove that there is no key 1, by saying (1, 3) isn't included.

Yes, but the trusted process (IBC handler) can remove old key-value pairs, so only either (0, 1) or (0, 2) could be included at any given time.

You're right that the key exclusion proof doesn't work though.

It might be possible to formulate timeout logic without exclusion proofs by proving the existence of a different value at that key (and the handler process guaranteeing that the key will only be written to once) but that seems disadvantageous.

Accumulators don't have key value pairs, they only have distinct values. I think you want these vector commitment properties onto them (key-binding), hence why I think it ought to actually be vector commitments.

Ok I see now, thanks for the patience. For the exclusion proofs we do indeed need key-binding.