Discussion: pinned data

[pchiusano]

Sometimes you want to tell Unison that data shouldn't leave a node, perhaps because it is secret. Here's a simple API for this:

builtin type Pinned a
builtin ability Pinned.Read
pin : a -> Pinned a
read : Pinned a ->{Pinned.Read} a

ability Remote where -- oversimplified
  -- Nodes are tagged with their allowed abilities
  at : Node {e} -> '{e} a -> Future a
  spawn : Abilities e -> Node {e}
  force : Future a -> a

So you can read a Pinned, but it requires the Pinned.Read ability. We can allow that ability for local programs (think like watch expressions and the like), but when creating nodes, you won't be given access to it, and since it is opaque you cannot write your own handler for it.

Furthermore, we change how Pinned values are serialized: they are just serialized as a dummy value. Since a valid, typed program can't ever call read on the recipient node, this is fine.

And an example usage:

ex1 node = 
  topSecret = pin "shouldn't leave this node"
  at bob '(read topSecret ++ "... exfiltrating")

Won't typecheck, unless bob node has a handler for the Pinned.Read ability which by the above reasoning won't be possible.

Improving this

The above is okay, but it's pretty limited in that you can't allocate "existential" pinned data in the middle of a larger remote computation. An example: I move a computation to the bob node which allocates some pinned data, reads it, and then returns 42. This should be fine, since the pinned data isn't escaping, but the above API would prevent it.

It seems possible to fix this using the runST trick, so something like:

builtin type Pinned t a
builtin ability Pinned.Read t

pin : a -> Pinned t a
read : Pinned t a ->{Pinned.Read t} a

ability Remote where
  at : Node e -> '{e, forall t . Pinned.Read t} a -> Future a
  ...

... which I believe gives you the ability to read pinned values you create locally, but not pinned values declared in outer scopes.

[aryairani]

you cannot write your own handler for it.

Is this necessary? Like a MITM thing?

[atacratic]

The following compiled for me - is that bad? Looks like it would successfully steal a secret. Maybe I am cheating because a real attacker wouldn't get to write code with the t in scope.

ex1 : Future t -> Future Text
ex1 foo = 
  topSecret : Pinned t Text
  topSecret = pin "shouldn't leave this node"
  bob : Node {Pinned.Read t}
  bob = Node
  Remote.at bob '(read topSecret ++ "... exfiltrating")

(Full gist here.)

[pchiusano]

@atacratic yeah, I think in practice you won’t have a node with the same token type as the pinned data.

Also aside is I think we are moving away from dealing with nodes in the API, instead there’s just logical tasks with locations / regions corresponding to some compute pool.

[pchiusano]

Playing with this some more, you need to have pin require the ability. Also, I realized this has nothing to do with Remote specifically, it's just a general scoping mechanism that prevents you from using tagged values outside of some lexical scope.

Here's a working example. Switching the nomenclature a bit. You'd want Local and Scope to be opaque for maximum safety.

unique type Local t a = Local a 
unique ability Scope t where void : Void 

local : a ->{Scope t} Local t a
local a = Local a

read : Local t a ->{Scope t} a
read = cases Local.Local a -> a

run : (forall t . '{Scope t, g} a) ->{g} a
run a = 
  handle !a with
  cases 
    { a } -> a
    { Scope.void -> k } -> bug "blarg"

ex = run 'let
  a = local 10
  b = local 12
  read a + read b

foo s = 
  use Nat +
  go s a = local (read s + a)
  List.foldl go s [0,1,2,3,4,5,6]

> run '(foo (local 0) |> read)

> ex

Yields:

      unique ability Scope t
      unique type Local t a
      ex    : Nat
      foo   : Local t Nat ->{Scope t} Local t Nat
      local : a ->{Scope t} Local t a
      read  : Local t a ->{Scope t} a
      run   : (∀ t. '{g, Scope t} a) ->{g} a

  Now evaluating any watch expressions (lines starting with `>`)... Ctrl+C cancels.

    30 | > run '(foo (local 0) |> read)
           ⧩
           21

    32 | > ex
           ⧩
           22