Sealing

[ratmice]

Hi,

Norm said he was going to write up the following code, but I can't
find where he did.

I know there is a thorough breakdown of Stiegler's ocaml version here

That links to most sealer/unsealer pair related links on Norm's site (directly or indirectly).
The exceptions being WeakMap implementations, and a cooperating conspirators attack Attack 2.

(define (pgen)  (let ((thePayload '()) (hasPayload #f))
  (cons (lambda (payload) (lambda () (set! thePayload payload) (set! hasPayload #t)))
        (lambda (box) (set! hasPayload #f) (box) (if hasPayload thePayload #f)))))

Unfortunately this is a version of the buggy sealer which suffers from Attack1

Edit: Norm's updated code is indirectly linked above,
but I don't think there is any harm in just including it inline:
Seal

; my version of Stiegler's box.
; http://cap-lore.com/CapTheory/Synergy/E.html
(lambda () (let ((thePayload '()) (hasPayload #f))
  (cons (lambda (payload) (lambda () (set! thePayload payload) (set! hasPayload #t)))
        (lambda (box) (set! hasPayload #f) (box)
          (if hasPayload (begin (set! hasPayload #f) thePayload) #f)))))

; Interesting alternative -- returns nullOb upon bad box.
(lambda (nullOb) (let ((content nullOb))
  (cons (lambda (Ob) (lambda () (set! content Ob)))
        (lambda (box) (set! content nullOb) (box)
            (let ((r content)) (set! content nullOb) r)))))

; Demo:
(let* ((p ((fileVal "Seal"))) (seal (car p)) (unseal (cdr p))
    (b2 (seal 42))
    (b3 (seal 43)))
  (cons (unseal b2) (unseal b3))) ; => (42 . 43)

I'm not sure of where this attack originates from, Toby Murray's description here Analysing Object-Capability Security (Murray 2007) describes the solution:

Hence, once the invocation of the box returns, the slot should contain c if the box was sealed by the corresponding sealer. If the slot contains a capability, then the unsealer takes a copy of it and clears the slot before returning the capability.

Stiegler's ocaml code cleared the 'slot' as well. But I have never found a published reference for the attack, perhaps folklore.

Toby's slides have diagrams of the process.

I think it's worth considering WeakMap and other variants or primitives that produce their effect on seal rather than unseal. (e.g. insertion into the WeakMap) For reasons of having a thread safe unseal and less suprising implementation with regards to the unexpected effects discussed in the attack above, where failure to clear the slot essentially turns the unsealer itself into a one-way read-only communications channel when given a () -> () lambda for a box.

Edit/Caveat: not really familiar with WeakMap sealer/unsealers, I've mostly used typed opaque value mechanism where the unsealer is just the identity function to the unopaque type, the naive versions of which don't support revocation but are pure.