Tiered SMT delete soundness issue

[bobbinth]

In #1046 we implemented basic delete functionality (i.e., without support for the last tier deletions) for TSMT implementation in stdlib. While this implementation works, on case of the delete procedures has a soundness issue because it relies on the advice provider supplying correct data.

The specific case is when we need to remove a leaf node from TSMT. Currently, this is done non-deterministically. Specifically:

• The advice providers performs the deletion and provides the root of a new TSMT to the VM.
• The VM performs insertion into the TSMT defined by this root, and checks this against the original root.
• If the root post insertion is the same as the original root, then we can say that the root provided by the advice provider is the root resulting from deleting the specified key from the original TSMT.

The issue with the above approach is that our insert procedure assumes that the TSMT it works with is valid. However, in this case, the advice provider could provide an invalid TSMT. For example:

Let's say we have a TSMT with root R and two leaves: A and B. Keys for these leaves share the same 16-bit prefix, and thus, both of them are located at depth 32. Now, let's say we want to delete A. The proper deletion would remove A and move B up to depth 16. The root of the new tree would be R_new. Then the VM can insert A into R_new and if all was supplied correctly, it'll get R.

However, if a malicious user provides R_bad instead of R_new to the VM, and in this R_bad, A is removed, but B is not moved up to tier 16, inserting A into R_bad would also output R. So, the VM would accept R_bad as the new root of the TSMT.

I think it would be too difficult to ensure that insert procedure checks the validity of the entire tree. But it seems to me that implementing deletions without use of this kind of non-determinism should not be too compliated.

[Al-Kindi-0]

Yes, although I think it can be patched, it is an issue. A patch could be to provide data to justify the depth at which the insertion into R_new is done. This can be two non-empty nodes that are checked for inclusion as part of the deletion procedure.
Another solution, as you suggested, is to implement the deletion procedure in a direct manner. My worry is that this might be very complicated but there might be some opportunities to use non-determinism to speed-up some parts of it.

[frisitano]

Giving this some thought.

[bobbinth]

Closed by #1215 because we no longer will use TSMT.