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

• Achilles’ Tent Notes #8
• Achilles’ Tent Notes #9
• Achilles’ Tent Notes #10
• Achilles’ Tent Notes #11
• Achilles’ Tent Notes #12
• Achilles’ Tent Notes #13

---

Surface Obliv-Rust

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

• New type:

  type Obliv<T>;
  // or simply
  type obliv τ
  

• New obliv if expression:

  obliv if e1 { e2 } else { e3 }
  

  fn add(x: obliv u32, y: obliv u32) -> obliv u32 {
    obliv if x == y {
        x * 2
    } else {
        x + y
    }
  }
  

• New obliv match expression:

  obliv match e { ... }
  

  fn oadd1(i: obliv Option<u32>) -> obliv Option<u32> {
    obliv match i {
        Some(n) => Some(n + 1),
        None => None,
    }
  }
  

• Either a new function declaration:

  obliv fn foo(a: &u32, b: &mut u32) -> &mut u32
  

  Or, a new reference qualifier in signature:

  fn bar(a: &u32, b: &frz u32) -> &frz u32
  // `baz` is forbidden in obliv context, has &mut.
  fn baz(a: &u32, b: &mut u32)
  // `bat` also has an &mut making it forbidden in obliv context,
  // however takes an &frz, what does this mean?
  fn bat(a: &mut u32, b: &frz u32)
  

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

Math

• obliv num / obliv num should never panic
  • The impl Div for oblivious types should have a well defined division by 0 value. Users can choose a well behaved n/d for short syntax, and manually check for if d == 0
  • Otherwise, checked_div will be available which returns an obliv Option, forcing the user to handle the n/0 case

Open Questions

• What is an obliv &, if anything
• fiat-crypto Rust extraction
  • Still need to play with running the extraction more
  • Questions about what types to expose for the underlying algebraic structures
• Possibly use λ-rust for some parts of Rust that Oxide doesn’t reason about, e.g. unsafe