An Attack on Simplified Version

On 2016 May 25 Matt Rice said of this: “don't you need a 2nd temporary/(set! hasPayload #f) after (box) for the case where someone has the correct unsealer, doesn't have the box, but can call a function which causes a box they don't have to be unsealed?”
Matt was right. Scenario: X and Y both legitimately hold unsealer U. X wants access to b which is sealed in a box B that Y, but not X holds. While X and Y are distinct protection domains, they each call functions defined by the other. X passes Q to U where Q is a routine crafted by X to call R (from Y) which passes B to U. As U returns to R the variable HasPayload is still true and thePayload still holds p. R returns to its caller which is an invocation of U by X and returns p to X which is what X wanted and should not have gotten.
This exploit is prevented by (set! hasPayload #f) after confirming HasPayload but before returning as we do here. This bug, and fix is portable to several languages.

This can be classified as a concurrency bug as there were two processes at once in the unsealer routine; there were two stack frames within the same lexical scope coordinating the state of the same instance of HasPayload. This code is not needed in Keykos because Keykos has the primitive domain tool which provides efficient synergy. Also domains are not accidentally ‘reentrant’ as they are in most modern languages. Keykos also prevents domains from being called while they ‘are already on the stack’.

One red flag is a call to a suspicious function, such as box. But what is a ‘suspicious function’? The plan was that box was an object whose behavior we had defined, but there was no way to enforce that plan. Reasoning about the behavior failed when a call to a suspicious function resulted in running code, that we had written, which used its authority to modify the variable which we were reasoning about. For any sort of correctness we must assume that the function car is in fact the real primitive described in the manual. Here box is a parameter passed from the netherworld. We think:

The sarcasm above may be strategic in establishing the sought “frame of mind”. I hope we can do better.

Another bad mental pattern is while thinking about sealer logic, we try to guard only the uniqueness of our access to innards of sealed objects. We did not fail in that regard but we may neglect our obligation to keep separate the abstract values of our clients. Now the question is just whose obligation is that? This is a serious question. The Keykos factory was invented to absolve the definer of the behavior of objects from a factory from issues of keeping secrets defined by the abstracted state of those objects.

If a purveyor of an abstraction wants to guarantee that abstractions from one client are never mixed from those of another, it will suffice to instantiate a whole new purveyor with its own sealer-unsealer pair. Factory like logic can assure clients that this has been done. This would preclude clients from even sharing those abstract value should they decide to.

With factory logic in Keykos two users of the same factory will not have their secrets mixed even if the behavior of the objects from the factory are incompetent. They can share such objects should they decide to. This is because the object from the factory retains the domain creator that all of the siblings from that factory use. The creator and recognize and open domains that it created, much as the unsealer unseals.