[spec] Rectype_ok rules contain a loophole that allows oob `REC` typeuses in nested deftypes

[raoxiaojia]

There seems to be an issue in the Rectype_ok rules that allow oob REC typeuses to be valid. The relevant rules are the following:

rule Rectype_ok/empty:
  C |- REC eps : OK(x)

rule Rectype_ok/cons:
  C |- REC (subtype_1 subtype*) : OK(x)
  -- Subtype_ok: C |- subtype_1 : OK(x)
  -- Rectype_ok: C |- REC subtype* : OK($(x+1))

rule Rectype_ok/_rec2:
  C |- REC subtype* : OK(x)
  -- Rectype_ok2: C, RECS subtype* |- REC subtype* : OK x 0

rule Rectype_ok2/empty:
  C |- REC eps : OK x i

rule Rectype_ok2/cons:
  C |- REC (subtype_1 subtype*) : OK x i
  -- Subtype_ok2: C |- subtype_1 : OK x i
  -- Rectype_ok2: C |- REC subtype* : OK $(x+1) $(i+1)

Note that Rectype_ok/cons allows the subtype to be validated directly using whatever C.RECS was. Now consider the following example, with an outer 2-member rec group sts = REC [st_a, st_b] containing the following:

  st_a = SUB [] [] (STRUCT [ref (deftype inner_dt)])
  st_b = SUB [] [] (STRUCT [])

where the inner deftype is the 0th projection of a length-1 rec group which contains an oob reference:

  inner_dt = DEF (REC [inner_st]) 0
  inner_st = SUB [] [] (STRUCT [ref (REC 1)])

I claim that the outer rec group sts is valid under an empty context C via the following chain of sufficient conditions (I include the explicit *type_ok relations instead of using the C |- notations to avoid ambiguity):

rectype_ok C sts x
<= (by (rectype_ok/rec2)) rectype_ok2 (C' := {C with RECS := sts}) (REC sts) x 0
<= (by (rectype_ok2/cons)) subtype_ok2 C' st_a x 0 && rectype_ok2 C' [st_b] (x+1) 1

The latter rectype_ok2 is trivial since st_b contains no interesting information. For the first part, all conditions except comptype_ok is trivial, since st_a declares no supertype (so nothing to prove for supertype validity and the $before predicate). This proceeds further by chasing down a long chain of constructors for the sufficient conditions (note that due to soundness's extension of typeuse to deftype and REC, all the various *_ok relations are actually in a large mutually recursive group):

comptype_ok C' (STRUCT [ref (deftype inner_dt)])
<= fieldtype_ok C' (ref (deftype inner_dt))
<= storagetype_ok C' (ref (deftype inner_dt))
<= valtype_ok C' (ref (deftype inner_dt))
<= reftype_ok C' (ref (deftype inner_dt))
<= heaptype_ok C' (deftype inner_dt)
<= typeuse_ok C' (deftype inner_dt)
<= deftype_ok C' inner_dt
<= rectype_ok C' [inner_st]

Now, we should expect the last line to be impossible, because rectype_ok/rec2 requires [inner_st] to be typed under a new context C'' := {C' with RECS := [inner_st]}, thereby revealing the oob REC 1 in inner_st. However, rectype_ok/cons gives a loophole that allows inner_st to be typed under C' := {C with RECS := [st_a, st_b]}, which was the original outer rec group. This would go through the above again until hitting typeuse, which then validates the REC 1 reference against the outer C'.RECS -- and is accepted because typeuse/rec_ only requires the REC index to be within bound. This completes a proof that the original rec group sts is well-typed under an empty context C despite it containing an inner subtype inner_st that contains an invalid REC index. The root cause is that rectype_ok/cons gives an incorrect context for a rec group to be checked.

IMO the mathematically correct fix is to directly remove rectype_ok/empty and rectype_ok/cons. This will force the typing of rec group to always go through rectype_ok/rec2, which will mandate a corresponding shadowing of the C.RECS field (as intended). As a result, rectype_ok will simply be a wrapper that updates the RECS field of the context, while the iterative check of each individual subtype in the rec group will be handled by the inductive rules of rectype_ok2.

Note that the current rectype_ok/empty+cons are redundant anyway, since rectype_ok2 already contains the iterative structure. However, this fix might not work directly for the spec document, as it may have complications regarding how the rectype_ok rule is currently rendered -- I believe the validation section only renders rectype_ok (which is actually wrong) instead of rectype_ok2 (which is a soundness-appendix-only artifact).

Lastly, I don't think this counterexample can currently appear during validation of an actual Wasm module, mainly because REC doesn't have a binary encoding; plus that REC only appears by rolling type indices, but rolling doesn't produce nested REC type variables in inner rectype groups due to the substitution functions correctly stopping REC substitution at rectype boundaries (by minus_recs), so there's no exploitable module-level counterexample.

[raoxiaojia]

Note that this also has some other consequences -- subtype_ok will become dead code if rectype_ok/cons is removed -- the validation of subtype and rectype will be taken over by subtype_ok2 and (wrapping over) rectype_ok2 respectively. I think the correct read here is that subtype_ok and rectype_ok are not merely just 'generalised' by adding subtype_ok2 and rectype_ok2 as stated in the current soundness section, but should instead be replaced by them.

[rossberg]

Interesting! I'm glad you're doing all the proofs!

So the idea of course was that Rectype_ok is what an actual Wasm validator implements, and Rectype_ok2 is the generalisation that's only necessary to define WF for internal types, needed only to prove soundness (and to restrict non-deterministic type guesses in some rules to be WF). So in the main body of the spec, we want to keep the former.

The idea was that only the cons rule from one of the judgements is used for a given REC, but it looks like my definition of the generalisation is such that both can mix and interfere in unintended ways, correct?

Would this be fixed by a side condition on Rectype_ok/rec2 that requires C.RECS to be empty? I think that would prevent going back from ok2 to ok as was intended, thereby ruling out the bad case.

[rossberg]

Answering my own question: no, that would fix the problem, but be too restrictive, since deftypes could no longer nest. Mh.

[raoxiaojia]

Yes, that fixes the above counterexample but allows actual valid nested types to be untypeable (considering just changing the inner REC's index from 1 to 0 and pad it accordingly).

[rossberg]

Maybe the correct place to put that side condition is on Rectype_ok/cons? Then this rule can only be used on the outermost recursion, not within a nested deftype.

[raoxiaojia]

@rossberg I think this closes the gap in my original counterexample (going back to rectype_ok/cons after applying rec2). However, there's a different type of counterexamples that exists, where a proof can suddenly jump ship from the middle of a rectype_ok/cons chain to rectype_ok/rec2, and then goes to rectype_ok2 with the wrong C.RECS context being assigned. This is observable when some elements of the rec group declares an incompatible supertypes, which will now be checked against an incorrect index that might incorrectly accepts the supertype. Consider the following length-4 rec group sts = [st_a, st_b, st_c, st_d]:

st_a = SUB [] (STRUCT [mut I32, I32])     -- 2-field struct, .REC-free
st_b = SUB [] (STRUCT [])              
st_c = SUB [] (STRUCT [mut I32])              -- incorrect index to be exploited as supertype
st_d = SUB [.REC 0] (STRUCT [mut I32])   -- declares .REC 0 as supertype

st_d declares st_a as the supertype which is impossible ([I32, I32] is not a supertype of [I32]). But there's a proof of validity if we apply rectype_ok/cons exactly 2 times, leaving the current suffix being [st_c, st_d], and then switches to apply rec2 which updates C.RECS with [st_c, st_d] only -- under which st_d's supertype is valid because they are equivalent.

I think the fundamental issue here is that we can't allow a proof tree to contain mixture of rectype_ok/cons and rectype_ok/rec2. The C.RECS=[] condition only forbids one direction of the mixture but not the other.

Upd: fixed the example -- my original example doesn't work because of the $before bound.

[raoxiaojia]

If the intention is to still keep a separate rectype_ok as the validator version, I felt that the correct call might be to add a flag to the type argument (so augmenting the OK(x) to something like OK(x, processing)), and then force rec2 to only type a rec group with the processing = false version of rectype_ok; in the mean time, rectype_ok/cons's inductive call will need to apply the processing = true signature. This seems to prevent the mixture by separating the two kinds of proof paths of rectype_ok; but at that point they might as well just be defined as separate predicates.

[rossberg]

There may be an even simpler fix: we remove the rule Rectype_ok/rec2, and just invoke Rectype_ok2 directly in Deftype_ok. There is no reason to actually take the detour through the extra rule. That would also clarify the judgements' respective roles.

[raoxiaojia]

Right -- that is much cleaner indeed. Actually, do we still need a separate rectype_ok2 if we take that approach given that it's now deftype_ok's responsibility to shadow the contexts? The only difference between that and the original version was the version of subtype_ok relation they depend on. Maybe we can combine them altogether (eg. defining subtype_ok2 as an extension of subtype_ok by adding a constructor to it. We only need to make sure that the validator version can't use the added constructor).

[rossberg]

Well, Rectype_ok2 needs to maintain the additional rec type index bound, which isn't needed for validation.

[raoxiaojia]

True, seems that skipping rectype in the deftype - subtype path is the right fix then.

[rossberg]

Mh, at this point I'm tempted to also change ok2/cons to:

rule Rectype_ok2/cons:
  C |- REC (subtype_1 subtype*) : OK x i
  -- Subtype_ok2: C |- subtype_1 : OK x i
  -- Rectype_ok2: C |- REC subtype* : OK x $(i+1)  ;; note no more +1 on x

since a deftype should never refer to one of its own types via a regular index. (And I'd correspondingly revert ec9067b in #2125.)

Does that look reasonable to you?

[raoxiaojia]

I agree -- I think that expresses the correct intention of the semantics, that at the stage of validating deftype, all intra-group references via idx should have already been rolled to rec. This also clarifies the intention of rectype_ok2 and rectype_ok a bit better.