As discovered in #3571, it is currently possible to violate capability guarantees in the current viewpoint adaptation table, but this could be prevented by updating ponyc to use George Steed's viewpoint adaptation rules which distinguish between extracting and non-extracting viewpoint adaptation. However, we wish to patch up the immediate soundness hole without waiting for someone to complete that larger chunk of work.
@sylvanc pointed out that we could easily close the latter hole without implementing the extensive changes required by George Steed's model by simply updating our single viewpoint adaptation table.
This could potentially break existing code, in that it might remove some valid/sound uses of non-extracting capabilities to fix the soundness hole for extracting capabilities. But it would fix the hole and prevent the exploit.
To be totally clear, fixing this issue would mean updating the trn row of our viewpoint adaptation table to the following:
| ▷ | iso field | trn field | ref field | val field | box field | tag field |
|-----------------|-----------|-----------|-----------|-----------|-----------|-----------|
| __trn origin__ | iso | box | box | val | box | tag |
In other words, the only change required to fix this hole is to make it so that the viewpoint adaptation trn->trn would now be a box rather than a trn.
Note that in George Steed's model, the non-extracting form is trn and the extracting form is val, so you would expect that we can choose val for the "weaker" one but we actually can't guarantee val until we know we're extracting, which we don't know because we haven't made that distinction. So the best we can do is have it be box.
Note that we will also need to update the Pony tutorial viewpoint adaptation table using the table row I gave above.
@sylvanc pointed out that we could easily close the latter hole without implementing the extensive changes required by George Steed's model by simply updating our single viewpoint adaptation table.
It turns out that this approach to resolving the problem is incompatible with the standard library collections/persistent package, as discovered by @jasoncarr0 in #3591.
It seems like to fix the soundness bug in this ticket, we would either need to go ahead with the full, extensive change in #2815 or drop support for the collections/persistent package until that time.
It may also be possible to refactor the collections/persistent package to not rely on trn->trn, but @jasoncarr0 has suggested that it would be nontrival, and we're not sure at this time that it is even possible.
@Theodus will investigate how the persistent collections package can be refactored to step around this issue. He will either file a PR to fix the usage, or if it can't be done, he will update the issue ticket with his findings on why it couldn't be fixed.
PR open: #3592
@jemc fyi the tutorial was already updated this change at some point.
Most helpful comment
PR open: #3592