Achilles' Tent Notes #9 written by Nathan Lilienthal on October 15, 2019.

Surface Obliv-Rust

Below are the first highlights for obliv additions to the surface Rust language.

Formal Obliv-Oxide

Together with changes to the underlying Oxide formalism. Please note that this section is incomplete with respect to syntax, and possibly semantics. Please read as notes.

  1. Syntax
    ω ::= uniq | frzn | shrd

    We must be able to “freeze” references until we “thaw” them in an always block. We can interpret uniq as unique and mutable, frzn as unique but not mutable, and finally shrd as simply immutable.

    obliv τ ::= obliv bool | obliv int | ...
              | obliv [τ; n]
              | obliv [obliv τ; n]

    Oblivious base types are defined, I’m using int as a placeholder for more underlying numeric (and other sized) types. As well as a composite obliv [] type. Also note that both PIR and ORAM structures fit these types respectively.

    e ::= ...
        | conceal(e)
        | reveal(e)
        | obliv if e1 { e2 } else { e3 }
        | always { e }
  2. Typing Rules
    conceal & reveal primitives:
            e: τ              e: obliv τ
    -------------------      ------------
    conceal(e): obliv τ      reveal(e): τ
    obliv if:
         e1: obliv bool     e2, e3: τ
    obliv if e1 { e2 } else { e3 } : obliv τ

    And, returning functions (The case is the same for functions of no arguments):

        e1: obliv bool         e2, e3: fn(τ*) -> τ
    obliv if e1 { e2 } else { e3 }: fn(τ*) -> obliv τ

    However, I’m unsure still at this time if the next rule should result in type fn(&frz) or fn(&mut).

        e1: obliv bool         e2, e3: fn(mut τ*) -> τ
    obliv if e1 { e2 } else { e3 }: fn(frz τ*) -> obliv τ

    Do we need the notion of a function with explicit fn foo(mut x: u32, frz: u32)? Trait definition functions, for example, don’t allow patterns in the arguments.

    always: TODO
  3. Operational semantics
    obliv if e1 { |a1,...,an| e2 } else { |a1,...,an| e3 } =>
    |a1,...,an| { obliv if e1 { e2 } else { e3 } }

    This is a somewhat straightforward reduction, if you ignore the details of &frz and &mut for a moment:

    obliv if e1 { |&a1,...,&an| e2 } else { |&a1,...,&an| e3 } =>
    |&a1,...,&an| { obliv if e1 { e2 } else { e3 } }
  4. Safety


Open Questions