This note is mainly about a synergy algorithm in two different languages: OCaml and Scheme. Normally to reason about the correctness of code one must consider its behavior when called as expected. For code such as this, however, we must consider behavior of our code when interacting with arbitrary code, perhaps from an attacker.

In particular I try to wrap my head around the Sealer-Unsealer problem introduced by James H. Morris: “Protection in Programming Languages”, CACM, 16(1):15-21, 1973. I trust my intuitive understanding of what is to be achieved. I have recently learned to distrust my intuition about whether code such as this appropriately limits access to such sealed objects. It clearly works when invoked as planed. Does it ever unseal when it should not, however? I want to describe a frame of mind, or perhaps a formalism which tends to find bug such as mentioned here.

These fears extend to intuitions about call/cc as well.

I attempt to write some rules for users of the code. Here is the scenario which I presume you find yourself in.
Presumptions:

You invent a data format that can efficiently represent some useful abstract value.
You have code to process this internal data format.
Only this code, perhaps defined in some lexical scope, is to have direct access to the format that you have invented.
You will widely distribute a set of functions to be viewed in the netherworld as operators on these abstract types.
You export these values in this format only in sealed boxes while only you hold the sealer and unsealer.
Due to this arrangement any value in one of these boxes has been produced by your code and malformed values are your fault.

You may need to protect the interests of others as follows: (Other requirements may be placed on your code lest users refuse to use it:)

The abstract values, and of course their internal form, are inaccessible to you even while they are accessible to your code.
Clients of your code are assured that between operations of your code on their abstract instances, your code retains no access to their values, and thus it is impossible for your code to mix their secrets with the values of other clients of your code. (This clause is muddy. It needs to be replaced.)
While people trust your code with their secrets they need assurance that their secrets are kept from anyone except via the sealed boxes that they hold. They need further assurance that nothing besides your code can sabotage the internal data structures that carry their abstract values. You probably want that too but assurance to you may be suffice as assurance to them.

More plainly and less precisely: In the netherworld one must be unable to sense the abstract state of a value without a capability to the box holding the representation for that value. This must be said more clearly!

Here are some rules most of which are obvious but some of which are not. I hope to explain some of the obscure rules. They should impose no burden.

Call the function makeSealerPair or (fileVal "Seal") just once before any zots are created.
Keep the sealer as long as anyone may hold onto boxes in which you have sealed your representations.
Keep the unsealer as long as anyone may call one of your operator functions which returns an abstract value.
(Obscure) If x is a (sealed) box, then while (procedure? x) yields true, never invoke x. Especially never write code that invokes x and lives in functions that may be called from the netherworld. Denizens may hold x and invoke it and that, at least, is what we must worry about.

I think that small step semantics are needed here if only to accommodate call/cc.

Our unsealer routine calls the box which is a function supposedly produced by our sealer code. It is easy to see what happens if this is so but we must consider other cases as well. In particular we must consider what happens when the value of box is produced by a crafted function such as: (lambda () (x) (u b2)) where x is a call from the netherworld to a different protection domain in the netherworld which has legitimate access to another value sealed by the same sealer, and that other value is unsealed due to natural actions of the other domain. I see no fault yet.

The steps executed by the unsealer may be interleaved with steps of another invocation of the same unsealer when the first invocation passes a fake box which indirectly invokes that same unsealer but a different box.

I think (and need to show) that we must worry only about situations where the current (unnamed) continuation has frames whose program counter are either just before or just after … (cloud)

Here is an attack on a shortened version. I am working on an attack on the full version using continuations.