Still not sound: Gradual typing vs. opportunistic decoding

[nomeata]

Looks like we still haven’t found the grail yet…

TL;DR: Our relaxed coercion rules for opt (#110 and following) may lead to “hard” deserialization errors later on.

I seems that the following can’t all hold:

• We are sound in the higher-order case (as per IDL-Soundness)
• We have no subtyping checks while deserialization (one of our Design goals).
• Type Erasure (another of the design goal)
• Record Extensibility, at least in the form implemented right now.

Counter-example

Here is the counter example:

service A1 : { bar : () -> () }
service B1 : { baz : () -> () } 

service C : { 
  init : (service A1, service B1) -> (); // stores (a1, b1)
  run : () -> () ;  // runs a1.bar(b1.baz())
}

If we pass A1 and B1 to C.init, all is well. C.run works fine.

Now we upgrade A1 to A2 and B1 to B2, as follows:

type WantsBool = service : { foo : (bool) -> () }
type WantsInt = service : { foo : (int) -> () }
service wantsInt : WantsInt
service A2 : {  bar : (opt WantsBool) -> () } // calls `arg.foo(true)` if `arg` is not `null`
service B2 : { baz : () -> (opt WantsInt) }  // returns (opt wantsInt)

These upgrades are permitted by our :<, and actually desirable (i.e. restricting <: to avoid “obviously bogus” upgrades doesn’t help)

But now C.run will cause B2 to pass opt wantsInt to A2. This will succeed at deserialization (because “Function and services references coerce unconditionally”). Now A2 invokes wantsInt.foo(true), and the deserialization of (true) at expected type (bool) will fail in wantsInt.

Generic Soundness proof

In https://github.com/dfinity/candid/blob/master/spec/IDL-Soundness.md#proof-for-canonical-subtyping we have a generic soundness proof for “Canonical subtyping”, that says “A solution with canonical subtyping (transitive, contravariant) is sound.”. And our <: is that!

But it’s not “decompositional” any more. In particular,

If t1 <: t2 and s1 in t1 <: s2 in t2 then s1 <: s2.

(as required in the generic proof) doesn’t hold .

Concretely in our example above, we have opt WantsInt <: opt WantsBool (because all opt types related). But because the reference value is passed through, this also means WantsInt in opt WantsInt <: WantsInt <: opt WantsBool, but we don’t have WantsInt <: WantsBool.

So…

Dunno. No concrete suggestions. It’s sunday morning, and I just wanted to get this insight out of my head.

[rossberg]

Hm, let me see.

Before C itself gets changed to the extended signature types and upgraded, it will keep ignoring the new optional args & results and not pass anything on to bar.

However, if you do try to change C to use the new types, you will probably get something like a warning that the call bar(baz()) uses unsafe subtyping. In Motoko, you wouldn't even be able to compile it anymore, and would be forced to change the program to pass null explicitly for the new parameter. (The example is a bit odd in that it composes two calls over a unit value, which is a bit pointless; but you can of course enrich the example such that there is at least one preexisting result/arg involved).

So unless I am missing something, this kind of case can only break if the general opt subtyping was allowed in the source language itself -- which would alway be unsound regardless of Candid, unless subtyping was coercive and coerced to null in that case. Which would also fix the problem.

Am I missing something? Is there a way to construct this example with a sound source language? Maybe by going one order higher? (Edit: Don't think that's possible, due to the property that we do not have "covert channels", so never pass on unknown values.)

[nomeata]

Before C itself gets changed to the extended signature types and upgraded, it will keep ignoring the new optional args & results and not pass anything on to bar.

Oh, right, I was simplifying this too much. (I think I made the same mistake when building counter examples many times so far…)

I need to make it more higher order:

Counter example (2nd try)

Let me try to decompose this into two steps:

1. A “unsafe coercion” setup
2. Exploiting that

For 1., let me try to construct a situation where a service s : service_typ1 turns into any s : service service_typ2.

Preparation:

service A1 : { return_s : () -> () }
service B1 : { accept_s : (func () -> ()) -> () } 
service C : { 
  init : (service A1, service B1) -> (); // stores (a1, b1)
  run : () -> () ;  // runs b1.accept_s(a1.return_s)
}

If we pass A1 and B1 to C.init, all is well. C.run and thus B.baz works fine.

Now we upgrade A1 to A2 and B1 to B2, as follows:

service A2 : { return_s : () -> (opt service_typ1)} // return (opt s)
service B2 : { accept_s : (func () -> (opt service_typ2)) -> ()}  // calls arg.(), if result is not null, stores it as (s : service_typ2)

These upgrades are permitted by our <: relation.

But now C.run will cause A2 to pass s: service_typ1 to B2 This will succeed at deserialization (because “Function and services references coerce unconditionally”).

Now B2 has (s : service_typ2), which is clearly unsound.

Actually exhibiting the crash is now easy, just set

service_typ1 = service { foo : (bool) -> () }
service_typ2 = service { foo : (int) -> () }

and let B2.accept_s call s.foo(3), which breaks s.foo (as that expects a bool).

[nomeata]

(Edit: Don't think that's possible, due to the property that we do not have "covert channels", so never pass on unknown values.)

We never pass on unknown values, but we can pass on values at “accidential types”. We said that at opt we are fine returning a non-null value if the values happen to work out, and don’t mind if the sender had a different type there (e.g. extra variants, the type of an empty list, or – crucially – different types on references).

[rossberg]

Right. Our opt rule relies on detecting any eventual inconsistencies and falling back to null. But if functions are involved, we do not detect any inconsistency. And when an actual call is performed, we have already forgot the assumed type, so a deferred check a la gradual typing isn't possible either.

It seems like the only fix here would be to go the proper gradual typing route and wrap deserialised function values -- or equivalently, remember their deserialisation type and use that for calls as well as for consecutive serialisations. And yes, do a subtype check upon deserialisation if we want eager detection.

[nomeata]

It seems like the only fix here would be to go the proper gradual typing route and wrap deserialised function values

I don’t think wrapping (i.e. eta-expanding and inserting code) works, as we can’t transfer closures, only the raw function or service reference, but

– or equivalently, remember their deserialisation type and use that for calls as well as for consecutive serialisations.

might help. But:

And yes, do a subtype check upon deserialisation if we want eager detection.

Is that really optional? If we don't do that check in the decoding of opt service_typ2 in B2.accept_s (where thing go wrong), then even if B2 remembers the type, what do we do with that information?

It seems that the eager subtype check is a reqiurement to fix this problem, and if we have the subtype check, we don't actually need any wrapping/type passing. Because the subtyping check is enough to ensure that

If t1 <: t2 and s1 in t1 <: s2 in t2 then s1 <: s2.

and then the generic soundness proof applies again.

[rossberg]

Well, if we were to go the gradual route then there wouldn't be any check at deserialisation time, but it would decompose into checks at use. Of course, it is too late to fall back to null at that point, so instead you'd get deferred type errors with some notion of blame (which arguably is of limited use in a distributed setting). That would be a possible semantics, but one can argue that it doesn't fit our approach.

So yeah, the choice seems to be between

1. Eager error detection involving subtype checks.
2. Lazy error detection involving gradual typing and blame.
3. No soundness.

All else being equal, (1) would seem like the obvious choice. But the price would be implementing subtyping in deseralisers.

[nomeata]

But the price would be implementing subtyping in deseralisers.

I am warming up that idea… it’s not like it’s impossible.

The main complexity I see here is to implement recursion breaker correctly, likely by memoization as we do in type.ml all over the place. The data structure, in general, seems to be quadratic in size (a subset of (types in message × types in expected type), or maybe just carefully chosen loop breakers). In the Motoko RTS we are least better equipped now to implement that (we have the “type hash”, and we can implement that part in C or Rust) than half a year ago. Still not an exciting prospect, though.

[rossberg]

You cannot avoid the quadratic worst-case with structural subtyping. That's not necessarily a problem for normal programs, which won't ever exercise this, but might be a concern with malicious parties sending "type checking bombs" (though I believe even that is only possible if the receiver uses a non-minimal type definition itself).

My other worry is that the extra complexity of implementing such a subtyping check might be seen as a con against using Candid.

[crusso]

So what if we had a separate opt type, say maybe <typ>, that restricted contents to first-order data so reference types cannot be encountered while deserialzing maybe <typ> values? Would that be enough of a restriction to recover soundness?

I'd much rather we ship something less expressive and sound than more expressive and unsound but I'm guess you are all with me on that, right?

[rossberg]

@crusso, interesting idea to restrict the offensive subtyping to first-order! I don't even think you'd need a separate type for that (which would be harder to target). Simply restrict all "inverse" and "unsafe" rules to only apply with first-order constituent types, which should cover the vast majority of use cases. @nomeata, what do you think?

[crusso]

Another suggestion might be to make the maybe <typ>, not first-order, but invariant, so as a long as subtyping holds, there's nothing to verify. It means you woudn't be able to reserve or deprecate with maybe reserved and maybe empty (or whatever way around it is).

[nomeata]

Simply restrict all "inverse" and "unsafe" rules to only apply with first-order constituent types, which should cover the vast majority of use cases. @nomeata, what do you think?

This might be too restrictive. Recall that we want both of these:

{ foo : opt (service s1) } <: {} -- normal subtyping
{} <: { foo : opt (service s2) } -- reverse subtyping, for extensible argument records

And hence, by transitivity, we get the problematic { foo : opt (service s1) } <: {} <: { foo : opt (service s2) }.

So you are saying we don’t get {} <: { foo : opt (service s2) }?

In other words, you can add new optional arguments to your services, but not if they would take function or service references?

but invariant

I don’t think that works; see the example above. You need variance (in fact the “anything goes rule”) to keep the relation transitive.

[rossberg]

Yes, such a restriction would prevent you from (contravariantly) adding higher-order fields, even when optional. I was thinking that that may be okay? Such a case might be rare enough that it is fine to require a more heavyweight solution for it. But obviously, I'm hand-waving with that reasoning.

[nomeata]

Such a case might be rare enough that it is fine to require a more heavyweight solution for it.

Such as using the untyped principal and do unsafe casting (which I expect is how people will work around this ;-))

Still not easy, because of transitivity. It sounds we want

{} <: { foo : opt (variant { first_order : int ) }

but unless we restrict the totally harmless rule t <: t' ⟹ opt t <: opt t' we also have

{ foo : opt (variant { first_order : int ) } <: { foo : opt (variant { first_order : int; higher_order : service s ) }

but now by transitivity we have

{} <: { foo : opt (variant { first_order : int; higher_order : service s ) }

and it's broken again.

[rossberg]

Yes, good point. In a certain twisted way I find it reassuring that hacks like that won't work. :)