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.
- Syntax
ω ::= uniq | frzn | shrd
We must be able to “freeze” references until we “thaw” them in an
always
block. We can interpretuniq
as unique and mutable,frzn
as unique but not mutable, and finallyshrd
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 compositeobliv []
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 }
- 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)
orfn(&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 - 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 } }
- 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 behavedn/d
for short syntax, and manually check forif d == 0
- Otherwise,
checked_div
will be available which returns anobliv Option
, forcing the user to handle then/0
case
- The
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