Achilles' Tent Notes #10 written by Nathan Lilienthal on October 28, 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
Typing Notes
- Oxide doesn’t have traits, or associated types
- Proper syntax for oblivious array types:
obliv [τ; N]
, cases enumerated below:Details:
obliv [obliv τ; N]⋮Index<obliv usize>
An oblivious array with oblivious data and oblivious access is an ORAMobliv [obliv τ; N]⋮Index<usize>
An oblivious array with oblivious data and plain accessobliv [τ; N]⋮Index<obliv usize>
An oblivious array with plain data and oblivious access is comparable to a PIR, as it could simply reveal the whole arrayobliv [τ; N]⋮Index<usize>
An oblivious array with plain data and plain access only adds a secure mapping of indices to logical memory addresses. Logical to physical mappings are still present in the face of compiled Rust[obliv τ; N]⋮Index<usize>
is just a normal ol’ array ofobliv τ
types[τ; N] ⋮Index<obliv usize>
is not implemented, and should be a type error
- Proper syntax for oblivious array types:
obliv ()
,obliv (T)
,obliv (T, U)
, and so on…obliv (T)
should not be equivalent toobliv T
obliv (T, U) = (obliv T, obliv U)
, simply structural- Rust’s
struct
(\(S::\langle\barρ,\barτ\rangle\)) are like tuples, so they should be consistent
obliv obliv τ
- Supports “MPC in the head” nested protocols
- Might require careful consideration when writing typing rules with promotions
conceal(τ)
andreveal(τ)
whereτ: σ → ρ
- Initial thought is that it doesn’t make sense to allow this, because function bodies must be public information in general, more on this below
- Oxide doesn’t currently have
enum
ormatch
match
should be able to be represented as if, with an understanding of some patterns- Enums are “tagged”, sum types
- We could start small and only allow matching for enums, avoiding the broader class of “patterns”
Redex Model
- Started a redex model
(define-language obliv)
- Thinking it should be
(define-union-language ...)
- Thinking it should be
- Example typing judgment:
[(types Γ e_1 (obliv bool)) (types Γ e_2 (obliv t)) (types Γ e_3 (obliv t)) -------------------------------------------- obliv-if (types Γ (obliv-if e_1 e_2 e_3) (obliv t))])
- Example reduction rule:
(--> (in-hole E (obliv-if v_1 (λ (x : t) e_2) (λ (x : t) e_3))) (in-hole E (λ (x : t) (obliv-if v_1 e_2 e_3))) "obliv-if-λ")
Public Promotion & Wire Types
- How can I write promotion rules like the following:
[(types Γ e t) (side-condition (public? t)) ---------------------------- promotion? (types Γ e (obliv t))]
- New typing forms for
public
andobliv
wire types[t ::= num bool (→ t t) ; ---------- (<public> t) (<obliv> t)]
(conceal (+ 1 2))
gets you(<obliv> 3)
1
used in place of a wire can be public promoted to(<public> 1)
Details:
- Public predicate and public values
(mux #t 2 3) ; -promotion> (mux (<public> #t) (<public> 2) (<public> 3)) ; -public-mux> (<public> 2) : (<public> num)
- Public predicate and
obliv
values(mux #f (conceal 2) (conceal 3)) ; -promotion> (mux (<public> #f) (conceal 2) (conceal 3)) ; -conceals> (mux (<public> #f) (<obliv> 2) (<obliv> 3)) ; -public-mux> (<obliv> 3) : (<obliv> num)
obliv
conditional predicate(mux (conceal x) 1 2) ; -promotion> (mux (<obliv> x) (<public> 1) (<public> 2)) : (<obliv> num)
- Public predicate and public values
(<public> (→ t t))
is the promotion of any function(<obliv> (→ t t))
could be the result type of something like(mux p (λ (x : num) x) (λ (x : num) 0))
since which function’s value is used will be unknown to an observer- We may want the ability to send/recv
(<public> v)
at run-time