: Static Enforcement of Privacy Policies for
Policy-Agnostic Oblivious Computation

Qianchuan Ye

Purdue University

Benjamin Delaware

Purdue University

Secure multiparty computation (MPC) techniques enable multiple
parties to compute joint functions over their private data without
sharing that data to other parties, typically by employing powerful
cryptographic protocols to protect individual's data. One challenge
when writing such functions is that most MPC languages force users
to intermix programmatic and privacy concerns in a single
application, making it difficult to change or audit a program's
underlying privacy policy. Existing policy-agnostic MPC languages
rely on run-time / dynamic enforcement to decouple privacy
requirements from program logic.  Unfortunately, the resulting
overhead makes it difficult to scale MPC applications that manipulate
structured data. This work proposes to eliminate this overhead by
instead transforming programs to semantically equivalent versions
that statically enforce user-provided privacy policies. We have
implemented this approach in a new MPC language, called ; our
experimental evaluation demonstrates that the resulting system
features considerable performance improvements on a variety of MPC
applications involving structured data and complex privacy polices.

§ INTRODUCTION

Secure multiparty computation (MPC) techniques allow multiple
parties to jointly compute a function over their private data while
keeping that data secure. A variety of privacy-focused applications
are instances of MPC problems, including secure auctions, voting, and
privacy-preserving machine learning <cit.>. MPC solutions typically depend on powerful cryptographic
techniques, e.g., Yao's Garbled Circuits <cit.> or secret
sharing <cit.>, to provide strong privacy
guarantees. Several high-level languages have been proposed to help
non-experts write MPC applications atop these cryptographic
techniques <cit.>. Almost all of these languages require the programmers to
explicitly enforce the high-level privacy policies within the
application itself, using the secure operations provided by the
language. This makes it hard to update the policies or explore
different policies, while also making it harder to read, write, and
reason about these applications. In the health care field, for
example, the Health Insurance Portability and Accountability Act
allows the disclosure of either the personally identifiable
information or the medical data, but not both. This policy does not
simply specify whether some particular field of a patient's medical
record is private or public; rather it is a relation over how a
program is allowed to access and manipulate different parts of a
particular record. Thus, a program must check, e.g., whether its
access patterns could potentially violate this policy for each field
access, using secure operations if so, or pay the (considerable)
cryptographic overhead of conservatively treating both fields as

These challenges become more acute when deal with structured data,
e.g., lists or trees, whose policies are necessarily more
complex. Consider a classification function that takes as input a
decision tree and a medical record owned by two different parties: if
the owner of the tree stipulates that its depth may be disclosed, the
classification function must use secure operations to ensure that no
other information about the tree is leaked, e.g., its spine of the
tree. If the owner of this tree is willing to share the spine,
however, this function must either be rewritten to take advantage of
the new, more permissive policy, or continue to pay the cost of
providing stricter privacy guarantees. Thus, most MPC languages
require users to write different implementations of essentially the
same program for different privacy policy.

The one exception is  <cit.>, a recently proposed
language that decouples privacy policies from programmatic concerns,
allowing users to write applications over structured data that are
agnostic to any particular privacy policy. To do so, implements
a novel form of the tape semantics proposed by <cit.>.
These semantics can then be used to dynamically enforce a
policy at runtime, enabling users to modularly build a secure
application by stipulating the particular policy a standard non-secure
implementation of the function must follow, in the form of a
dependent type equipped with security labels. Unfortunately,
while this dynamic enforcement strategy effectively disentangles
privacy concerns from program logic, it also introduces considerable
overhead for many applications particularly those that construct or
manipulate structured data with complicated privacy requirements,
e.g., filtering a list which is allowed to disclose its maximum length. Thus, this strategy does not
scale to the sorts of complex applications that could
greatly benefit from this separation of concerns.

This work presents , a policy-agnostic language for writing MPC
applications that eliminates this overhead by instead transforming
non-secure functions into a version statically enforce a
user-provided privacy policy. extends the source language of
with a form of dependent sums that package together the public
and private components of an algebraic data type (ADT). This type,
which we term -types, allows to automatically infer arguments to
dependent types needed to correctly enforce a particular top-level
privacy policy, which users had to manually provide. Each -type is equipped with a set
of , which, among other things, enable our
translation to efficiently combine instances of ADTs that have
different privacy policies. Our experimental evaluation demonstrates
that this strategy yields considerable performance improvements over
the dynamic enforcement used by , offering exponential
improvement on the most complex benchmarks in our evaluation suite.

We make the following contributions:

* We have developed , a version of extended with a
form of dependent sums that enables modular translation of
non-secure programs into efficient, secure versions. This language
is equipped with a security type system that offers the same
guarantees as : after jointly computing a well-typed function,
neither party can learn more about the private data of the other
outside of what can be gleaned from their own data and the output of
the function.

* We present an algorithm that combines a program written in the
non-secure fragment of and a privacy policy to produce a
secure private versions that statically enforces the desired
policy. We prove that our approach generates well-typed (and hence
secure) target programs that are additionally guaranteed to logically
refine the source program.

* We have evaluated our approach on a range of case studies and
microbenchmarks. Importantly, our experimental results demonstrate
exponential performance improvement over the previous
state-of-the-art () on several complicated benchmarks, while
simultaneously showing no performance regression on other

§ OVERVIEW

Consider the simple |filter| function
in <Ref>, which drops all the elements in a list
above a certain bound.[Our language supports higher-order
functions, but we use this specialized version for presentation

data list = Nil | Cons int list
fn filter : list -> int -> list = ?xs y =>
match xs with Nil => Nil
| Cons x xs' =>
if x <= y then Cons x (filter xs' y)
else filter xs' y

List filtering

Suppose Alice owns some integers, and wants to know which
of those integers are less than some threshold integer belonging to Bob, but
neither party wants to share their data with the other.
MPC protocols allow Alice and Bob to encrypt their data and then
jointly compute |filter| using secure operations, without
leaking information about the encrypted data. One implementation
strategy would be to simply encrypt everyone's integers and use a
secure comparison operation to compute the resulting list. Under a
standard semi-honest threat model[In this threat model, all
parties can see the execution trace produced by a small-step
semantics <cit.>.], however, this naive strategy can reveal
private information, via the shape of the input and output list. For
example, assume Alice's input list is
|Cons [2] (Cons [7] (Cons [3] Nil))|, and Bob's input is
|[5]|, where box values are encrypted, i.e., only the owner
of the integer can observe its value. By observing that Alice's
private data is built from three |Cons|s, Bob can already
tell Alice owns exactly $3$ integers, information that Alice may want
to keep secret. In addition, both parties can learn information from
the control flow of the execution of |filter|. By observing
which branch of |if| is executed, Bob can infer that the
second element of Alice's list is greater than $5$, for

In conclusion, even if the integers are encrypted, both parties can
still glean information about the other's private data. While that
Alice and Bob must agree to share some information about their
data to ensure termination, e.g., the maximum length of the input
list, a single datatype may have many policies about what can be
shared. If Alice only wants to share the maximum length of her list,
the encrypted list must be padded with dummy encrypted values. On the
other hand, if Alice does not mind sharing the exact number of
integers she owns, the joint computation will not have to go over these
values, allowing secure functions on list to be computed much more
efficiently. is a language that allows Alice and Bob to
specify a policy on their private data, i.e. what public information
can be shared, that guarantees that these policies are not violated
when jointly computing a function.

§.§ How to encode policies?

obliv @list<= (k : nat) =
if k = 0 then unit
else unit @+ @int * @list<= (k-1)
obliv @list== (k : nat) =
if k = 0 then unit
else @int * @list== (k-1)

Oblivious lists with maximum and exact length public views

Informally, a privacy policy for a structured (i.e. algebraic)
datatype stipulates which of its components are private and that a
secure application must protect, and a projection or public
view of the data that can be freely shared. Formally, a policy for
a datatype can be encoded as oblivious algebraic data types
(OADT) <cit.>, a dependent type built from oblivious
(i.e, secure) type formers whose shape is completely determined by a
public type argument (i.e., its public view). The key invariant of
OADTs is that two OADTs with the same public view are
indistinguishable to an attacker. <Ref> shows an OADT, !@list<=!,
for |list|s whose public view is their maximum length. All
oblivious lists of maximum length $2$ is computed to the same
oblivious type value, regardless of the actual length of the
|@list<= 2| ≡|unit @+ @int * (unit @+ @int *
Every list with this type is padded to length $2$, with the help of
oblivious sum<EMAIL_ADDRESS>convention, we use
$\hat{\dot}$ to denote the oblivious version of something.]  An
oblivious sum is similar to a standard sum, but both its tag and
“payload” (i.e. component) are obfuscated, so that an attacker
cannot distinguish between a left and right injection. Thus, an
attacker cannot learn anything about the structure of an OADT, outside
of what is entailed by its public view: an empty list, singleton list,
or a list with two elements of type |@list<= 2| all appear the
same to an attacker.

§.§ How to enforce policies?

Although this strategy ensures that the representation of private
information does not leak anything, both parties can still learn
information by observing control flow. In order to protect private
data from control flow channels, provides oblivious operations
to manipulate the private data safely. One such operation is the
atomic conditional |@if|,[This operation is usually
called !mux!, but we use !@if! for consistency
with other operations with secure/insecure version.], a version of
|if| that fully evaluates both branches before
producing its final result. Consider the following execution trace:

\[
\begin{array}{l}
\li!@if [0] @<= [1] then [2] @+ [3] else [4] @+ [5]! \steparrow
\li!@if [true] then [2] @+ [3] else [4] @+ [5]! \steparrow \\
\li!@if [true] then [5] else [4] @+ [5]! \steparrow
\li!@if [true] then [5] else [9]! \steparrow
\li![5]!
\end{array}
\]

Since both branches are evaluated regardless of the private
condition, an attacker cannot infer that condition from this execution
trace, since all boxed (encrypted) values are indistinguishable to an
attacker. Thus, falsifying the condition produces an equivalent trace,
modulo the encrypted data:

\[
\begin{array}{l}
\li!@if [6] @<= [1] then [2] @+ [3] else [4] @+ [5]! \steparrow
\li!@if [false] then [2] @+ [3] else [4] @+ [5]! \steparrow \\
\li!@if [false] then [5] else [4] @+ [5]! \steparrow
\li!@if [false] then [5] else [9]! \steparrow
\li![9]!
\end{array}
\]

The secure-type system of ensures all operations on private
data are done in a way that does not reveal any private information,
outside the public information specified by the policies.

§.§ How to automatically enforce policies?

Users can directly implement privacy-preserving applications in
using OADTs and secure operations, but this requires manually
enforcing policies so that the control flow depends only on public
information. Under this discipline, the implementation of a secure
function depends on both the program logic and the users privacy
policies: the secure version of |filter| requires a
different implementation, depending on whether Alice is willing to
share the exact length of her list, or an upper bound on that length.
Previous work <cit.> has considered how to decouples these
concerns by enforcing policies dynamically, through a novel
form of runtime semantics called tape semantics. To do so,
programmers only need to ascribe !@filter! a type signature
stipulating the policy that needs to be enforced by the runtime,
|fn @filter : (k : nat) -> @list<= k -> @int -> @list<= k|.
One shortcoming of this specification is that programmers have to
manually supply all public views: if the programmers mistakenly give
return type
!@list<= (k-1)!, for example, the last element of the list
may be truncated. More
problematically, the runtime overhead of dynamic policy enforcement
makes it hard to scale private applications manipulating structured
data. For example, the secure version of !filter! takes more
than $5$ seconds to run with an oblivious list !@list<=! of
length $16$, and its performance grows exponentially worse as the
number of elements increases.

To remedy these limitations, we propose to instead automatically
compile an insecure program into a secure version that
statically enforces a specified policy. To do so, we extend
, the secure language of <cit.> with -types,
a form of dependent sums (or dependent pairs) that packs public
views and the oblivious data into a uniform representation. For
example, !   @list<=! is the oblivious list !@list<=!
with its public view. This allows users to again derive a private
filter function from its type signature:
|fn @filter :    @list<= -> @int ->    @list<=|.
Importantly, users no longer need to explicitly provide the public
view for either the output or any intermediate subroutines: both are
automatically inferred.

To understand how our translation works, consider a naive approach
where each algebraic data type (ADT) is thought of as an abstract
interface, whose operations correspond to the introduction and
elimination forms of the algebraic data type[We adopt
pattern matching as elimination form instead of a recursion scheme
because supports general recursion.]. An ADT, e.g.,
!list!, and any corresponding -type, e.g.,
!   @list<=! and !   @list==!, are implementations or
instances of this interface. For example, an interface for a
!list! abstract data type is:

ListLike = type t; Nil : unit -> t; Cons : @int * t -> t; Imatch : t -> (unit -> alpha) -> (@int * t -> alpha) -> alpha

As long as !@list<=! and !@list<=! implement this
interface, we could straightforwardly translate !filter! to
a secure version:

fn @filter :    @list<= -> @int ->    @list<= = ?xs y =>
@list<=#Imatch xs (?_ => @list<=#Nil ())
(?(x, xs') =>
@if x @<= y then @list<=#Cons x (@filter xs' y)
else @filter xs' y)

fn @filter' :    @list== -> @int ->    @list== = ?xs y =>
@list==#Imatch xs (?_ => @list==#Nil ())
(?(x, xs') =>
@if x @<= y then @list==#Cons x (@filter' xs' y)
else @filter' xs' y)

Unfortunately, there are several obstacles to implementing this naive
strategy. First, the argument types of operations like
!Cons!  and !Imatch! are fixed to
!@int!. Thus, !list! is not an instance of this
abstract interface, despite !list! being a very reasonable
(albeit very permissive) policy! In general, different secure types may only
be able to implement operations with specific signatures. Second, some
functions may need to coerce from one type to a “more” secure
version. For example, if the policy of !@filter! is
!   @list<= -> int ->    @list<=!,
its second argument !y! will need to be converted to
in order to evaluate
!x @<= y!. The public view of a secure list may similarly
need to be converted from its exact length to some bounded length.
Third, this naive translation results in ill-typed programs: in
!@filter!, for example, the branches of |@if| may
evaluate to
!   (3, xs)   ! and !   (2, ys)   !, respectively, where
!xs! and !ys! are secure lists with public views
of $2$ and $3$. Thus, 's secure type system will (rightly)
reject !@filter! as leaky.  Lastly, the signatures that
should be ascribed to any subsidiary function calls may not be
obvious.  Consider the following client of !filter!:
|fn filter5 : list -> list = ?xs => filter xs 5|.
If |filter5| is given a signature
!   @list<= ->    @list<=!, we should infer a !filter!
function with the type
!   @list<= -> int ->    @list<=!, as the threshold argument is
publicly known. In general, a function may have many private versions,
and we must infer which versions to use at each callsite: a recursive
function may even recursively call a different “version” of itself.

To solve these challenges, we generalize the notion of abstract
interfaces described above to a set of more flexible structures,
dubbed (<Ref>). Our translation algorithm
(<Ref>) generates a set of typing constraints for the
intermediate expressions in a program. These constraints are then
solved using the set of available , resulting in
multiple private versions of the necessary functions and ruling out
the infeasible ones, e.g., !@filter'!.

fn @list<=#s : (k : nat) -> list -> @list<= k =
?k xs =>
if k = 0 then ()
else match xs with Nil => @inl ()
| Cons x xs' =>
@inr (s_@int x, @list<=#s (k-1) xs')

fn @list<=#view : list -> nat = length

fn @list<=#Nil : unit ->    @list<= = ?_ =>    (0, ())

fn @list<=#Cons : @int *    @list<= ->    @list<= =
?(x,    (k, xs)   ) =>
(k+1, @inr (x, xs))

fn @list<=#join : nat -> nat -> nat = max

fn @list<=#reshape : (k : nat) -> (k' : nat) -> @list<= k -> @list<= k' = ?k k' =>
if k' = 0 then ?_ => ()
else if k = 0 then ?_ => @inl ()
else ?xs => @match xs with @inl _ => @inl ()
| @inr (x, xs') => @inr (x, @list<=#reshape (k-1) (k'-1) xs')

fn' @list<=#r : (k : nat) -> @list<= k -> list =
?k =>
if k = 0 then ?_ => Nil
else ?xs =>
@match xs with @inl _ => Nil
| @inr (x, xs') =>
Cons (r_@int x) (@list<=#r (k-1) xs')

fn @list<=#Imatch :
@list<= -> (unit -> alpha) -> (@int *    @list<= -> alpha) -> alpha =
?   (k, xs)    f1 f2 =>
(if k = 0 then ?_ => f1 ()
else ?xs =>
@match xs with @inl _ => f1 ()
| @inr (x, xs') => f2 (x,    (k-1, xs')   )
: @list<= k -> alpha) xs

of !@list<=!

<Ref> presents the methods of of !@list<=!. The first two methods, !@list<=#s! and
!@list<=#r!, are the section and retraction
functions, similar to <cit.>. They convert a normal ADT, e.g.,
!list!, to its OADT counterpart, e.g., !@list<=!,
and back, effectively similar to encryption and decryption. The names
reflect their expected semantics: applying retraction to the section
of a value should produce the same value. Note that retraction may
reveal private information (indicated by the keyword !fn'!),
but our type system guarantees these “unsafe” functions are never
used in a secure function.
The !view! method selects a valid public view for the
structured data, so that the translation can safely convert a
!list!  to !   @list<=!.

The types of the introduction and elimination operations are specified
by the programmers. For example, the argument of
!@list<=#Cons! can have type !int *    @list<=! or even
!@int *    @list==!, as long as the types are compatible
!int * list!.
<Ref> does not show the coercion method,
but the programmers can define a coercion from !@list==! to
!@list<=!, for example.

The join structure, consisting of !join! and
!reshape!  methods, is the key to identifying what
-type is used under a private condition.  Recall the previous
example of a private conditional with -type branches: in order to
execute !@if [b] then    (3,xs)    else    (2,ys)   ! without
revealing ![b]!, we use the !join! method to
calculate a common public view that “covers” both branches. A public
view of $3$ works here, as a list with maximum length $2$ also has
maximum length $3$. Then our translation uses the !reshape!
method to convert both branches to use this common public view. In our
example, !ys!, an oblivious list of maximum length $2$, will
be converted to !ys'! of maximum length $3$. Finally, since
both branches now have the same public view, executing this
conditional no longer reveals ![b]!: the result is
equivalent to !   (3, @if [b] then xs else ys')   !. As we shall
discuss later, not all OADTs admit join structure, e.g.,
!@list==!, but our translation will generate constraints that
take advantage of any that are available and fail when they cannot be
resolved in a way that guarantees security.

In summary, to develop a secure applications in , programmers
first implement the functionality, e.g., !filter! in the
public fragment of , independently of particular policies, which
are separately defined via oblivious algebraic data types, e.g.,
!@list<=!, and their . Users can then derive
the secure version of their function by specifying its policy using
-types, relying on our compilation algorithm to produce the
desired implementation. In the next few sections, we formally develop
the language , the , and our translation

§ , FORMALLY

This section presents , the core calculus for secure
computation that we will use to explain our translation. This calculus
extends the existing  <cit.> calculus with -types,
and uses ML-style ADTs in lieu of explicit !fold! and
!unfold! operations. For simplicity, this calculus does not
include public sums, as these can be modeled using ADTs.

§.§ Syntax

|e,tau|                    Expressions

|    !unit! |!bool! |!@bool! |
!tau*tau! |!tau@+tau!     public & oblivious types
|    !   @T!     -type

|    !Pix:tau,tau! |
!?x:tau=>e!     dependent function
|    !(e,e)! |
!   (e,e)   !     pair & -pair

|    !()! |!b! |!x!
literals & variables
|    !pi_1 e! |
!pi_2 e!     product and -type projection

|    !let x = e in e!     let binding
|    !@inl<tau> e! |
!@inr<tau> e!     oblivious sum injection

|    !e e! ||C e| ||@T e|
|    !@match e with x=>e|x=>e!     oblivious sum elimination

|    !if e then e else e!     conditional
|    !match e with !!C x=>e!
ADT elimination

|    !@if e then e else e!     oblivious conditional
|    !s_@bool e!     boolean section

|D|           Global Definitions
|@w|        !unit! |!@bool! |
!@w*@w! |!@w@+@w!
Obliv. Type Values

|    !data T = !!C tau!
algebraic data type
|@v|        !()! |![b]! |
Obliv. Values

|    !fn x:tau = e!     (recursive) function
|   ![inl<@w> @v]! |![inr<@w> @v]!

|    !obliv @T (x:tau) = tau!
(recursive) obliv. type
|v|        |@v| |!b! |
!(v,v)! |!   (v,v)   ! |
!?x:tau=>e! |!C v!     Values

syntax with extensions to highlighted

<Ref> presents the syntax of . Types and
expressions are in the same syntax class, as is dependently
typed, but we use !e! for expressions and !tau!
for types when possible. A program consists of a set of
global definitions of data types, functions and oblivious
types. Definitions in each of these classes are allowed to refer to
themselves, permitting recursive types and general recursion in both
function and oblivious type definitions. We use !x!  for
variable names, !C! for constructor names, !T!
for type names, and !@T! for oblivious type names. Each
constructor of an ADT definition takes exactly one argument, but this
does not harm expressivity: this argument is !unit! for
constructors that take no arguments, e.g., !Nil!, and a
tuple of types for constructors that have more than one argument,
e.g., !Cons! takes an argument of type
!int * list!.

In addition to standard types and dependent function types
(!Pi!), includes oblivious booleans
(!@bool!) and oblivious sum types
(!@+!).[For simplicity, does not include
oblivious integers, but it is straightforward to add them.]
Oblivious conditional !@if! and pattern matching
!@match!  are the elimination forms of these two oblivious
types. The branches of these expressions must be private and are
evaluated to values before taking an atomic step to the final result.
Boolean section !s_@bool! is a primitive operation that
“encrypts” a boolean expression to an oblivious version. Oblivious
injection !@inl! and !@inr! are the oblivious
counterparts of the standard constructors for sums. Other terms are
mostly standard, although note that let bindings (!let!),
conditionals (!if!) and pattern matching (!match!)
are also allowed to return a type, as supports type-level

The key addition over is the -type,
!   @T!. It is constructed from a pair expression
!   (DOT,DOT)   ! that packs the public view and the oblivious
data together, and has the same eliminators !pi_1!  and
!pi_2! as normal products. As an example,
!   (3, @list<=#s 3 (Cons 1 Nil))   ! creates a -pair of type
!   @list<=! with public view $3$, using the section function
from <Ref>. Projecting out the second component
of pair using !pi_2! produces a value of type
!@list<= 3!. A -type is essentially a dependent sum type
(!Sigmax:tau,@T x!), with the restriction that
!tau!  is the public view of !@T!, and that
!@T x! is an oblivious type.

Since has type-level computation, oblivious types have
normal forms; oblivious type values (!@w!) are essentially
polynomials formed by primitive oblivious types.  We also have the
oblivious values of oblivious boolean and sum type. Note that these
“boxed” values only appear at runtime, our semantics use these to
model encrypted booleans and tagged sums.

§.§ Semantics

!e!  > !e'!

!e!  > !e'!

!ectx[e]!  > !ectx[e']!

!fn x:tau = e! ∈
!x!  > !e!

!obliv @T (x:tau) = tau'! ∈
!@T v!  > ![v/x]tau'!

!(?x:tau=>e) v!  > ![v/x]e!

!if true then e_1 else e_2!  > !e_1!

!@if [true] then v_1 else v_2!  > !v_1!

!match C_i v with !!C x=>e!  > ![v/x]e_i!

!pi_1 (v_1,v_2)!  > !v_1!

!s_@bool!  > ![b]!

!@inl<@w> @v!  > ![inl<@w> @v]!

!pi_1    (v_1,v_2)   !  > !v_1!

!@v_2! <  !@w_2!

!@match [inl<@w_1@+@w_2> @v] with x=>e_1|x=>e_2!  >
!@if [true] then [@v/x]e_1 else [@v_2/x]e_2!

|ectx|       Evaluation Context

|    ![]*tau! |!@w*[]! |
![]@+tau! |!@w@+[]! |
!e []! |![] v! |
!C []! |!@T []! |
!if [] then e else e!

|    !@if [] then e else e! |
!@if v then [] else e! |!@if v then v else []!

|    !([],e)! |!(v,[])! |
!   ([],e)   ! |!   (v,[])   ! |
!pi_1 []! |
!match [] with !!C x => e!

|    !@inl<[]> e! |!@inl<@w> []! |
!@match [] with x=>e|x=>e! |
!s_@bool []! |…

Selected small-step semantics rules of

<Ref> shows a selection of the small-step semantics
rules of (the full rules are included in the appendix). The
semantics of is similar to , with the addition of
S-PsiProj$_1$ (and S-PsiProj$_2$) to handle the
projection of dependent pair, which is simply the same as normal
projection. S-Ctx reduces subterms according to the
evaluation contexts defined in <Ref>. The first few
contexts take care of the type-level reduction of product and
oblivious sum type. The type annotation of oblivious injection
!@inl! and !@inr! is reduced to a type value
first, before reducing the payload. The evaluation contexts for
!@if! capture the intuition that all components of a private
conditional have to be normalized to values first to avoid leaking the
private condition through control flow channels.

S-OMatchL (and S-OMatchR) evaluates a pattern
matching expression for oblivious sums. Similar to |@if|,
oblivious pattern matching needs to ensure the reduction does not
reveal private information about the discriminee, e.g., whether it is
the left injection or right injection. To do so, we reduce a
|@match| to an oblivious conditional that uses the private
tag. The pattern variable in the “correct” branch is of course
instantiated by the payload in the discriminee, while the pattern
variable in the “wrong” branch is an arbitrary value of the
corresponding type, synthesized from the judgment !@v! <
!@w!, whose definition is in appendix. When evaluating a
|@match| statement whose discriminee is
![inl<@bool@+@bool*@bool> [true]]!, the pattern variable in
the second branch can be substituted by
!([true],[true])!, !([false],[true])!, or any
other oblivious pair of oblivious booleans.

§.§ Type System

Similar to , types in are classified by kinds
which specify how protected a type is, in addition to ensuring the
types are well-formed. For example, an oblivious type, e.g.,
!@bool!, kinded by !*@O!, can be used as branches
of an oblivious conditional, but not as a public view, which can only
be kinded by !*@P!. A mixed kind !*@M! is used to
classify function types and types that consist of both public and
oblivious components, e.g., !bool*@bool!. A type with a
mixed kind cannot be used as a public view or in private context.

!e! :: !tau!

!e! :: !tau!

!tau! == !tau'!

!tau'! :: !*@*!

!e! :: !tau'!

!x! :: !tau_1! |- !e! :: !tau_2!

!tau_2! :: !*@*!

!?x:tau_1=>e! :: !Pix:tau_1,tau_2!

!e_2! :: !Pix:tau_1,tau_2!

!e_1! :: !tau_1!

!e_2 e_1! :: ![e_1/x]tau_2!

!e_0! :: !bool!

!e_1! :: ![true/y]tau!

!e_2! :: ![false/y]tau!

!if e_0 then e_1 else e_2! :: ![e_0/y]tau!

!e_0! :: !@bool!

!tau! :: !*@O!

!e_1! :: !tau!

!e_2! :: !tau!

!@if e_0 then e_1 else e_2! :: !tau!

!obliv @T (x:tau) = tau'! ∈

!e_1! :: !tau!

!e_2! :: !@T e_1!

!   (e_1,e_2)   ! :: !   @T!

!obliv @T (x:tau) = tau'! ∈

!e! :: !   @T!

!pi_1 e! :: !tau!

!obliv @T (x:tau) = tau'! ∈

!e! :: !   @T!

!pi_2 e! :: !@T (pi_1 e)!

!tau! :: !kappa!

!tau! :: !kappa!

!kappa! ⊑!kappa'!

!tau! :: !kappa'!

!obliv @T (x:tau) = tau'! ∈

!e! :: !tau!

!@T e! :: !*@O!

!tau_1! :: !*@*!

!x! :: !tau_1! |- !tau_2! :: !*@*!

!Pix:tau_1,tau_2! :: !*@M!

!tau_1! :: !*@O!

!tau_2! :: !*@O!

!tau_1@+tau_2! :: !*@O!

!obliv @T (x:tau) = tau'! ∈
!   @T! :: !*@M!

!e_0! :: !bool!

!tau_1! :: !*@O!

!tau_2! :: !*@O!

!if e_0 then tau_1 else tau_2! :: !*@O!

Selected typing and kinding rules of

|- !tau! :: !*@*!

|- !e! :: !tau!

!fn x:tau = e!

∀i.  |- !tau_i! :: !*@P!

!data T = !!C tau!

|- !tau! :: !*@P!

!x! :: !tau! |- !tau'! :: !*@O!

!obliv @T (x:tau) = tau'!

global definitions typing

The type system of is defined by a pair of typing and
kinding judgments, ; |- !e! :: !tau! and
; |- !tau! :: !kappa!. The global context
is a map from names to a global definition, while the typing
context  is standard. <Ref> presents a subset of
our typing and kinding rules; the full rules are in appendix. For
brevity, we elide the global context as it is fixed in these rules.

The security type system <cit.> of enforces a
few key invariants. First, oblivious types can only be constructed
from oblivious types, which is enforced by the kinding rules, such as
K-OSum. Otherwise, the attacker could infer the private tag
of an oblivious sum, e.g., !bool@+unit!, by observing its
public payload. Second, oblivious operations, e.g., !@if!,
require their subterms to be oblivious, to avoid leaking private
information via control flow channels. T-OIf, for example,
requires both branches to be typed by an oblivious type, otherwise an
attacker may infer the private condition by observing the result, as
!@if [true] then true else false!. Third, type-level
computation is only defined for oblivious types and cannot depend on
private information. Thus, K-If requires both branches to
have oblivious kinds, and the condition to be a public boolean. The
!@if [true] then unit else @bool! is ill-typed, since the
“shape” of the data reveals the private condition.

The typing rules for -types are defined similarly to the rules of
standard dependent sums. T-PsiPair introduces a dependent
pair, where the the type of the second component depends on the first
component. In contrast to standard dependent sum type, -type has
the restriction that the first component must be public and the second
component must be oblivious. This condition is implicitly enforced by
the side condition that !@T! is an OADT with public view
type !tau!. <Ref> shows the typing rules
for global definitions; DT-OADT prescribes exactly this
restriction. The rules for the first and second projection of
-type, T-PsiProj$_1$ and T-PsiProj$_2$, are
very similar to the corresponding rules for standard dependent sum
types. Observe that a -type always has mixed kind, as in
K-Psi, because it consists of both public and oblivious

T-Conv allows conversion between equivalent types, such as
!if true then @bool else unit! and !@bool!. The equivalence
judgment !tau! == !tau'! is defined by a set of parallel
reduction rules, which we elide here. The converted type is nonetheless
required to be well-kinded.

Note that this type system does not allow type checking retraction
functions, e.g., !@list<=#r! from
<Ref>, as such functions reveal private
information. To type check these “unsafe” functions, we simply omit
some side-conditions related to oblivious kinding. For example,
removing !tau! :: !*@O! from T-OIf allows the
expressions to disclose the private condition.

§.§ Metatheory

With our addition of -type, still enjoys a standard
type soundness property (i.e. progress and preservation), and, more
importantly, the same security guarantees as :

If !e_1!   !e_2! and |- !e_1! ::
!tau_1! and |- !e_2! :: !tau_2!, then

* [n]!e_1!  > !e_1'! if and only if [n]!e_2!  >
!e_2'! for some |e_2'|.

* if [n]!e_1!  > !e_1'! and [n]!e_2!  >
!e_2'! , then !e_1'!   !e_2'!.

Here, !e!   !e'! means the two expressions are
indistinguishable, i.e. they only differ in their unobservable
oblivious values, and [n]!e!  > !e'! means !e!
reduces to !e'! in exactly $n$ steps. This obliviousness
theorem provides a strong security guarantee: well-typed programs that
are indistinguishable produce traces that are pairwise
indistinguishable. In other words, an attacker cannot infer any
private information even by observing the execution trace of a
program. All these results are mechanized in the Coq theorem prover,
including the formalization of the core calculus and the proofs of
soundness and obliviousness theorems.

§ AND DECLARATIVE LIFTING

While our secure language makes it possible to encode structured data
and privacy policies, and use them in a secure way, it does not quite
achieve our main goal yet, i.e. to decouple privacy policies and
programatic concerns. To do so, we allow the programmers to implement
the functionality of their secure application in a conventional way,
that is using only the public, nondependent fragment of . We
make this fragment explicit by requiring such programs to have
simple types, denoted by !eta!, defined in
<Ref>. For example, !filter! has simple
type !list -> int -> list!. Programs of simple types are the
source programs to our lifting process that translate them to a
private version against a policy, which stipulates the public
information allowed to disclose in the program input and output. This
policy on private functionality is specified by a specification
type, denoted by !theta!, defined also in
<Ref>. For example, !@filter! has
specification type !   @list<= -> @int ->    @list<=!. Note that
while dependent types are not directly allowed in specifications,
instead they are encapsulated in -types.  Simple types and
specification types are additionally required to be well-kinded under
empty local context, i.e. all ADTs and OADTs appear in them are

However, not all specification types are valid with respect to a
simple type. It is nonsensical to give !@filter! the
specification type !@int -> @bool!, for example. The
specification types should still correspond to the simple types in
some way: the specification type corresponding to !list!
should at least “list-like”. This correspondence is formally
captured in the erasure function in <Ref>, which
maps a specification type to the “underlying” simple type. For
example, !   @list<=! is erased to !list!. This
function clearly induces an equivalence relation: the erasure
|   [theta]   | is the representative of the equivalence
class. We call this equivalence class a compatibility class,
and say two types are compatible if they belong to the same
compatibility class. For example, !list!, !@list<=!
and !@list==!  are in the same compatibility class
![list]!. This erasure operation is straightforwardly
extended to typing contexts, , by erasing every
specification type in  and leaving other types untouched.

Our translation transforms source programs with simple types into
target programs with the desired (compatible) specification types. As
mentioned in <Ref>, this lifting process depends
on a set of $\psi$-structures which explain how to translate
certain operations associated with an OADT.

Simple types

|eta|        !unit! |!bool! |!T! |!eta*eta! |!eta->eta!

specification types

|theta|        !unit! |!bool! |!@bool! |!T! |!   @T! |!theta*theta! |!theta->theta!

!   [theta]   !

!   [unit]   ! = !unit!
!   [bool]   ! = !   [@bool]   ! = !bool!
!   [T]   ! = !T!   where !T! is an ADT

!   [   @T]   ! = !T!   where !@T! is an OADT of !T!

!   [theta*theta]   ! = !   [theta]   *   [theta]   !
!   [theta->theta]   ! = !   [theta]   ->   [theta]   !

Simple types, specification types and erasure

§.§ OADT Structures

Every global OADT definition |@T| must be equipped with an
OADT-structure, defined below.

An OADT-structure of an OADT |@T|, with public view
type |tau|, consists of the following () type and functions:

* A public type !T! :: !*@P!, which is the public
counterpart of |@T|. We say |@T| is an OADT
of |T|.

* A section function !s! :: !Pik:tau,T->@T k!, which
converts a public type to its oblivious counterpart.

* A retraction function !r! :: !Pik:tau,@T k->T!, which
converts an oblivious type to its public version.

* A public view function !VIEW! :: !T->tau!, which creates
a valid view of the public type.

* A binary relation  over values of types !T! and
!tau!; !v! !k! reads as |v| has
public view |k|, or |k| is a valid public view of

These operations are required to satisfy the following axioms:

* (A-O$_{1}$) |s| and |r| are
a valid section and retraction, i.e. |r| is a left-inverse for
|s|, given a valid public view: for any values !v! ::
!T!, !k! :: !tau! and !@v! :: !@T k!,
if !v! !k! and *!s k v!  > !@v!, then
*!r k @v!  > !v!.

* (A-O$_{2}$) the result of |r| always has valid
public view: *!r k @v!  > !v! implies !v! !k! for all values !k! :: !tau!, !@v!
:: !@T k! and !v! :: !T!.

* (A-O$_{3}$) |VIEW| produces a valid public
view: *!VIEW v!  > !k! implies !v! !k!, given any values !v! :: !T! and !k!
:: !tau!.

For example, !@list<=! is equipped with the OADT-structure
with the public type !list!, section function
!@list<=#s!, retraction function !@list<=#r! and view
function !@list<=#view!, all of which are
shown in <Ref>. users do not need to
explicitly give the public type of an OADT-structures, as it can be
inferred from the types of the other functions. The binary relation
is only used in the proof of correctness of our translation,
so users can also elide it. In the case of !@list<=!,
simply states the length of the list is no larger than the
public view.

§.§ Join Structures

In order for -types to be flexibly used in the branches of secure
control flow structures, our translation must be able to find a common
public view for both branches, and to convert an OADT to use this
view. To do so, an OADT can optionally be equipped with a

A join-structure of an OADT |@T| of |T|, with public view
type |tau|, consists of the following operations:

* A binary relation  on |tau|, used to compare
two public views.

* A join function !JOIN! :: !tau->tau->tau!,
which computes an upper bound of two public views[It is a
bit misleading to call the operation !JOIN! “join”, as it
only computes an upper bound, not necessarily the lowest
one. However, it should compute a supremum for
performance reasons: intuitively, larger public view means more

* A reshape function
!RESHAPE! :: !Pik:tau,Pik':tau,@T k->@T k'!, which
converts an OADT to one with a different public view.

such that:

* (A-R$_{1}$)  is a partial order on |tau|.

* (A-R$_{2}$) the join function produces an upper bound: given
values !k_1!, !k_2! and !k! of
type !tau!, if *!k_1JOINk_2!  > !k!, then
!k_1! !k! and !k_2! !k!.

* (A-R$_{3}$) the validity of public views is monotone with
respect to the binary relation : for any values !v! ::
!T!, !k! :: !tau! and !k'! :: !tau!,
if !v! !k! and !k! !k'!, then
!v! !k'!.

* (A-R$_{4}$) the reshape function produces equivalent value,
as long as the new public view is valid: for any values !v! ::
!T!, !k! :: !tau!, !k'! :: !tau!,
!@v! :: !@T k! and !@v'! :: !@T k'!, if
*!r k @v!  > !v! and !v! !k'! and
*!RESHAPE k k' @v!  > !@v'!, then *!r k' @v'!  >

<Ref> defines the join and reshape functions
!@list<=#join! and !@list<=#reshape!. The partial
order for this join structure is simply the total order on integers,
and the join is simply the maximum of the two numbers. Not all OADTs
have a sensible join-structure: oblivious lists using their exact
length as a public view cannot be combined if they have different
lengths. If such lists are the branches of an oblivious conditional,
lifting will either fail or coerces both to an OADT with a

!theta! |> !@ite!

!theta! ∈!unit!, !@bool!

!theta! |> !?@b x y=>@if @b then x else y!

!theta_1! |> !@ite_1!

!theta_2! |> !@ite_2!

!theta_1*theta_2! |>
!?@b x y=>(@ite_1 @b (pi_1 x) (pi_1 y),@ite_2 @b (pi_2 x) (pi_2 y))!

!theta_2! |> !@ite_2!

!theta_1->theta_2! |> !?@b x y=>?z=>@ite_2 @b (x z) (y z)!

(!@T!, !JOIN!, !RESHAPE!) ∈
!   @T! |>

!?@b x y=>let k = pi_1 x JOIN pi_1 y in!

!        &(k,@if @b then RESHAPE (pi_1 x) k (pi_2 x))!

!           else RESHAPE (pi_1 y) k (pi_2 y))&!

Join structures induce a mergeability relation, defined in
<Ref>, that can be used to decide if a specification
type can be used in oblivious conditionals. We say |theta|
is mergeable if !theta! |> !@ite!, with
witness |@ite| of type
|@bool->theta->theta->theta|. We will write
!theta! when we do not care about the witness. This
witness can be thought of as a generalized, drop-in replacement of
!@if!: we simply translate !@if! to the derived
!@ite! if the result type is mergeable. The case of
-type captures this intuition: we first join the public views,
and reshape all branches to this common public view, before we select
the correct one privately using !@if!. This rule looks up the necessary methods from the context of join structures . Other cases are
straightforward: we simply fall back to !@if! for primitive
types, and the derivation for product and function types are done

§.§ Introduction and Elimination Structures

An ADT is manipulated by its introduction and elimination forms. To
successfully lift a public program using ADTs, we need structures to
explain how these primitive operations of ADTs are handled in their
OADT counterparts. Thus, an OADT |@T| can optionally
be equipped with an introduction-structure (intro-structure)
and an elimination-structure (elim-structure), defined
below. These structures are optional because, e.g., some programs may
not construct an ADT, only traverse them, such as a function that
checks membership in a list.

An intro-structure of an OADT |@T| for a global definition
!data T = !$\overline{\li!C eta!}$, consists of a set of
functions |@C_i|, each corresponding to a constructor
|C_i|. The type of |@C_i| is
|theta_i->   @T|, where !   [theta_i]   ! =
!eta_i! (note that DT-ADT guarantees that
|eta_i| is a simple type).  Which |theta_i| to
use is decided by the programmers providing this structure.

Each |@C_i| is required to logically refine the corresponding
constructor (A-I$_1$): given any values !v! ::
!   [theta]   ! and !v'! :: !theta!, if (!v!,
!v'!) ∈!theta!, then (!C_i v!, !@C_i v'!) ∈!   @T!.

An elim-structure of an OADT |@T| for a global definition
!data T = !$\overline{\li!C eta!}$, consists of a family
of functions |@Imatch_alpha|, indexed by the possible
return types.  The type of |@Imatch_alpha| is
|   @T->|$\overline{\li!(theta->alpha)!}$|->alpha|,
where !   [theta_i]   ! = !eta_i! for each
|theta_i| in the function arguments corresponding to

Each |@Imatch_alpha| is required to logically refine the
pattern matching expression, specialized with ADT |T| and
return type |alpha|. The sole axiom of this structure
(A-E$_1$) only considers return type |alpha|
being a specification type: given values !v_i! ::
!   (k,@v)   ! :: !@T k!,
!?x=>e_i! :: !   [theta_i]   ->   [alpha]   ! and
!?x=>e_i'! :: !theta_i->alpha!,
if *!r k @v!  > !C_i v_i! and
(!?x=>e_i!, !?x=>e_i'!) ∈!theta_i->alpha! then
!@Imatch    (k,@v)    !!(?x=>e')!) ∈!alpha!.

The types of the oblivious introduction and elimination forms in these
structures are only required to be compatible with the public
counterparts. The programmers can choose which specific OADTs to use
according to their desired privacy
policy. <Ref> shows the constructors and
pattern matching functions for !@list<=!.

The elim-structure of an OADT consists of a family of destructors, whose return
type !alpha! does not necessarily range over all types. For example,
!@Imatch_alpha! of !@list<=!, !@list<=#Imatch! in
<Ref>, requires !alpha! to be a mergeable type,
due to the use of !@match!, which imposes a restriction similarly to !@if!.
Such constraints on !alpha! are automatically inferred and enforced.

Intuitively, the axioms of these structures essentially state that the
introduction and elimination methods of an OADT should behave like
those of the corresponding ADT. Their relationship is expressed as
logical refinement, formally defined in <Ref>,
!DOT! and !DOT!.

§.§ Coercion Structures

As discussed in <Ref>, we may need to convert an
oblivious type to another, either due to a mismatch from input to
output, or due to its lack of certain structures. For example,
!@list==! does not have join structure, so if the branches of
an oblivious conditional has type !   @list==!, they should be
coerced to !   @list<=!, when such a coercion is available.

Two compatible OADTs may form a coercion-structure, shown below.

A coercion-structure of a pair of compatible OADTs |@T|
and |@T'| of |T|, with public view type |tau|
and |tau'| respectively, consists of a coercion
function |COER| of type |   @T->   @T'|. The coercion should
produce an equivalent value (A-C$_1$): given values !v!
:: !T!, !   (k,@v)   ! :: !   @T! and !   (k',@v')   !
:: !   @T'!, if *!r k @v!  > !v! and *!COER   (k,@v)   !
> !   (k',@v')   !, then *!r k' @v'!  > !v!.

!theta!  > !theta'! |> !COER!

!theta!  > !theta! |> !?x=>x!

!bool!  > !@bool! |> !?x=>s_@bool x!

(!@T!, !T!, !s!, !r!, !VIEW!, ) ∈
!T!  > !   @T! |> !?x=>   (VIEW x,s (VIEW x) x)   !

!COER! :: !   @T->   @T'! ∈
!   @T!  > !   @T'! |> !COER!

!theta_1!  > !theta_1'! |> !COER_1!

!theta_2!  > !theta_2'! |> !COER_2!

!theta_1*theta_2!  > !theta_1'*theta_2'! |>
!?x=>(COER_1(pi_1 x),COER_2(pi_2 x))!

!theta_1'!  > !theta_1! |> !COER_1!

!theta_2!  > !theta_2'! |> !COER_2!

!theta_1->theta_2!  > !theta_1'->theta_2'! |>
!?x=>?y=>COER_2(x (COER_1y))!

This structure only defines the coercion between two -types.
<Ref> generalize the coercion relation to any (compatible)
specification types. We say |theta| is coercible to
|theta'| if !theta!  > !theta'! |> !COER!, with
witness |COER| of type |theta->theta'|. We may write
!theta!  > !theta'! when we do not care about the witness. The
rules of this relation are straightforward. The context of coercion structures
and the context of OADT structures  are used to look up the
necessary methods in the corresponding rules. The rule for coercing a function
type is contravariant. Note that we can always coerce a public type to an OADT
by running the section function, and the public view can be selected by the view
function in the OADT structure.

§.§ Declarative Lifting

!e! :: !theta! |> !Oe!

!b! :: !bool! |> !b!

!x! :: !theta! ∈
!x! :: !theta! |> !x!

!x! :: !theta! |> !Ox! ∈
!x! :: !theta! |> !Ox!

!x! :: !theta_1! |- !e! :: !theta_2! |> !Oe!

!?x:   [theta_1]   =>e! :: !theta_1->theta_2! |>

!e_2! :: !theta_1->theta_2! |> !Oe_2!

!e_1! :: !theta_1! |> !Oe_1!

!e_2 e_1! :: !theta_2! |> !Oe_2 Oe_1!

!e_1! :: !theta_1! |> !Oe_1!

!x! :: !theta_1! |-
!e_2! :: !theta_2! |> !Oe_2!

!let x = e_1 in e_2! :: !theta_2! |> !let x = Oe_1 in Oe_2!

!e_0! :: !bool! |> !Oe_0!

!e_1! :: !theta! |> !Oe_1!

!e_2! :: !theta! |> !Oe_2!

!if e_0 then e_1 else e_2! :: !theta! |>
!if Oe_0 then Oe_1 else Oe_2!

!e_0! :: !@bool! |> !Oe_0!

!theta! |> !@ite!

!e_1! :: !theta! |> !Oe_1!

!e_2! :: !theta! |> !Oe_2!

!if e_0 then e_1 else e_2! :: !theta! |>
!@ite Oe_0 Oe_1 Oe_2!

!data T = !!C eta! ∈

!e! :: !eta_i! |> !Oe!

!C_i e! :: !T! |> !C_i Oe!

!@C_i! :: !theta_i->   @T! ∈

!e! :: !theta_i! |> !Oe!

!C_i e! :: !   @T! |> !@C_i Oe!

!data T = !!C eta! ∈

!e_0! :: !T! |> !Oe_0!

∀i.  !x! :: !eta_i! |-
!e_i! :: !theta'! |> !Oe_i!

!match e_0 with !!C x=>e! :: !theta'! |>
!match Oe_0 with !!C x=>Oe!

!@Imatch! ::
!   @T->!!(theta->theta')!!->theta'! ∈

!e_0! :: !   @T! |> !Oe_0!

∀i.  !x! :: !theta_i! |-
!e_i! :: !theta'! |> !Oe_i!

!match e_0 with !!C x=>e! :: !theta'! |>
!@Imatch Oe_0 !!(?x:theta=>Oe)!

!e! :: !theta! |> !Oe!

!theta!  > !theta'! |> !COER!

!e! :: !theta'! |> !COEROe!

Selected declarative lifting rules

With these , we define a declarative lifting relation, which
describes what the lifting procedure is allowed to derive at a high level. This
lifting relation is given by the judgment ; ; ; |-
!e! :: !theta! |> !Oe!. It is read as the expression |e| of
type |   [theta]   | is lifted to the expression |Oe| of target
type |theta|, under various contexts. The context
consists of the set of OADT-structures (), join-structures
(), intro-structures (), elim-structures ()
and coercion-structures (), respectively. The global definition
context  is the same as the one used in the typing relation. The local
context  is also similar to the one in the typing relation, but it keeps
track of the target types of local variables instead of source types. Finally,
the lifting context  consists of entries of the form !x! ::
!theta! |> !Ox!, which associates the global function |x| of
type |   [theta]   | with a generated function |Ox| of the
target type |theta|. A single global function may have multiple target
types, i.e. multiple private versions, either specified by the users or by the
callsites. For example,  may contain !filter! ::
!@list<= -> @int -> @list<=! |> !@filter_1! and
!filter! ::
!@list== -> @int -> @list<=! |> !@filter_2!.

<Ref> shows a selection of rules of the declarative
lifting relation (the full rules are in appendix). We elide most
contexts as they are fixed, and simply write !e! ::
!theta! |> !Oe! for brevity. Most rules are simply
congruences and similar to typing rules. L-Fun outsources the
lifting of a function call to the lifting context. L-If$_2$
handles the case when the condition is lifted to an oblivious boolean
by delegating the translation to the mergeability relation. Similarly,
L-Ctor$_2$ and L-Match$_2$ query the contexts of the
intro-structures and elim-structures, and use the corresponding
instances as the drop-in replacement, when we are constructing or
destructing -types. Lastly, L-Coerce coerces an
expression nondeterministically using the coercion relation.

This lifting relation in <Ref> only considers one expression. In
practice, the users specify a set of functions and their target types to lift.
The result of our lifting procedure is a lifting context  which maps
these functions and target types to the corresponding generated functions, as
well as any other functions and the inferred target types that these functions
depend on. The global context  is also extended with the definitions of
the generated functions. To make this more clear, we say a lifting context is
derivable, denoted by , if and only if, for any
!x! :: !theta! |> !Ox! ∈,
!fn x:   [theta]    = e! ∈ and
!fn Ox:theta = Oe! ∈ for some |e| and
|Oe|, such that ; ; ; |- !e! ::
!theta! |> !Oe!. In other words, any definitions of the lifted functions
in  can be derived from the lifting relation in <Ref>. Note
that the derivation of a function definition is under a lifting context with
possibly an entry of this function itself. This is similar to the role of global
context in type checking, as supports mutually recursive functions. The
goal of our algorithm (<Ref>) is then to find such a derivable lifting
context that includes the user-specified liftings.

§.§ Logical Refinement

The correctness of the lifting procedure is framed as logical
refinement between expressions of specification types and those of
simple types; this relationship is defined as a step-indexed logical
relation <cit.>. As is common, this relation is defined via
a pair of set-valued type denotations: a value interpretation
!theta! and a expression interpretation
!theta!. We say an expression |e'| of type
|theta| refines |e| of type |   [theta]   |
(within $n$ steps) if (!e!, !e'!) ∈!theta!. In other words, |e'| preserves the
behavior of |e|, in that if |e'| terminates at a
value, |e| must terminate at an equivalent value. The
equivalence between values is dictated by !theta!.

<Ref> shows the complete definition of the logical relation. All
pairs in the relations must be closed and well-typed, i.e. their interpretations
have the forms:

\begin{gather*}
\interpV{\li!theta!} = \Set{(\li!v!, \li!v'!) |%
\type{\empctx |- \li!v! :: \li!&[theta]&!} \land%
\type{\empctx |- \li!v'! :: \li!theta!} \land%
\ldots} \\
\interpE{\li!theta!} = \Set{(\li!e!, \li!e'!) |%
\type{\empctx |- \li!e! :: \li!&[theta]&!} \land%
\type{\empctx |- \li!e'! :: \li!theta!} \land%
\ldots}
\end{gather*}

For brevity, we leave this requirement implicit in

!unit! =
!bool! =
!T! = (!v!, !v'!) |
0 < n !v! = !v'!
!@bool! =
(!b!, ![b']!) |
0 < n !b! = !b'!
!   @T! =
(!v!, !   (k,@v)   !) |
0 < n *!r k @v!  > !v!
!theta_1*theta_2! =
(!(v_1,v_2)!, !(v_1',v_2')!) |
(!v_1!, !v_1'!) ∈!theta_1!
(!v_2!, !v_2'!) ∈!theta_2!
!theta_1->theta_2! =
(!?x:   [theta_1]   =>e!, !?x:theta_1=>e'!) |
∀i < n.
∀(!v!, !v'!) ∈[i]!theta_1!.
(![v/x]e!, ![v'/x]e'!) ∈[i]!theta_2!

!theta! = (!e!, !e'!) |
∀i < n.
[i]!e'!  > !v'!
∃!v!.  *!e!  > !v!
(!v!, !v'!) ∈[n-i]!theta!

A logical relation for refinement

The definitions are mostly standard. The most interesting case is the
value interpretation of -type: we say the pair of a public view
and an oblivious value of an OADT is equivalent to a public value of
the corresponding ADT when the oblivious value can be retracted to the
public value. Intuitively, an encrypted value is equivalent to the
value it decrypts to. The base cases of the value interpretation
are also guarded by the condition that we still have steps left,
i.e. greater than $0$. This requirement maintains the pleasant
property that the interpretations [0]!theta! and
[0]!theta! are total relations on closed values and
expressions, respectively, of type |theta|. The proof also
uses a straightforward interpretation of typing context,
, whose definition is in appendix.

This relation also gives rise to a semantic characterization of the lifting
context. We say a lifting context is $n$-valid, denoted by [n],
if and only if, for any !x! :: !theta! |> !Ox! ∈, (!x!, !Ox!) ∈!theta!. If
[n] for any $n$, we say  is valid, denoted by
. The validity is essentially a semantic correctness of

§.§ Metatheory of Lifting

The first key property of the lifting relation is well-typedness,
which guarantees the security of translated programs, thanks to

Suppose  is well-typed and ; ; ; |-
!e! :: !theta! |> !Oe!. We have ;  |-
!e! :: !   [theta]   ! and ; |- !Oe! ::

Our lifting relation ensures that lifted expressions refine source
expressions in fewer than $n$ steps, as long as every lifted programs
in  is also semantically correct in fewer than $n$ steps.  As
is common in logical relation proofs, this proof requires a more
general theorem about open terms.

Suppose ; ; ; |- !e! :: !theta! |>
!Oe! and [n]. We have (!e!, !Oe!) ∈!theta!.

Finally, <Ref> provides a strong result of the
correctness of our translation. Any lifting context that is derived
using rules of <Ref> is semantically correct. In other
words, if every pair of source program and lifted program in
are in our lifting relation, they also satisfy our refinement

implies .

Our logical refinement only provides partial correctness, as can be
seen in the definition of ·. As a result, the lifting
relation does not guarantee equi-termination: it is possible that the
lifted program does not terminate while the source program does. The
main cause is that a private conditional must fully execute both
branches, effectively turning conditionals from lazy evaluation to
eager evaluation.
Using a public value to bound the recursion depth in order to guarantee
termination is a common practice in data-oblivious computation. While a public
view naturally serves as such metric in many cases, some applications may
require rewriting functions to, e.g., recurse on some fuel value. None of the
case studies or benchmarks in our evaluation required this, however.

§ ALGORITHMIC LIFTING

<Ref> presents the overall workflow of our lifting
algorithm. This algorithm starts with a set of goals,
i.e. pairs of source functions tagged with the !Mlift!
keywords and their desired specification types. We then run our
lifting algorithm on all the functions in these goals, as well as any
functions they depend on, transforming each of these functions to the
oblivious version parameterized by typed macros and type
variables, along with a set of constraints over these type variables.
After solving the constraints, we obtain a set of type
assignments. Note that a single function may have multiple type
assignments, one for each of its specifications in the goals or from
callsites. For example, !filter!  may have the type
assignment for
!@list<= -> @int -> @list<=! from !Mlift!, and
assignment for !@list<= -> int -> @list<=! from the function
!filter5! in <Ref>. Finally, we generate the
private versions of all the lifted functions by instantiating their
type variables and expanding away any macros. The lifting context from
the last section is simply these lifted functions and their generated
private versions.

cat = [text centered, align=center]
block = [text centered, align=center, rectangle, draw]
label = [fill=white, align=center, anchor=center]
line = [->]
[auto, node distance=20pt and 0pt]
[block](g) goals from [basicstyle=]!Mlift!;
[block, below=of g](f) functions to lift;
[below=27pt of f](p0) ;
[block, left=of p0](l0) lifted functions with
macros & type var.;
[block, right=of p0](c) constraints over
type var.;
[block, below=of c](a) type assignments;
[below=33pt of p0](p1) ;
[block, below=of p1](l1) lifted functions
with macros;
[block, below=of l1](l2) well-typed & correct
lifted functions;

[line] (g) – node[label] dependency analysis (f);
[line] (f) – (l0);
[line] (f) – (c);
(f) – node[label,yshift=3pt] lifting (p0);
[line] (c) – node[label] constraint solving (a);
[line] (a) – (l1);
[line] (l0) – (l1);
(p1) – node[label] instantiation (l1);
[line] (l1) – node[label] elaboration (l2);

Lifting algorithm pipeline

The lifting algorithm is defined using the judgment ;
|- !e! :: !eta!   !X! |> !Oe!  > . It reads
as the source expression |e| of type |eta| is
lifted to the target expression |Oe| whose type is a
type variable |X| as a placeholder for the
specification type, and generates constraints . The source
expression |e| is required to be in administrative
normal form (ANF) <cit.>, which is guaranteed by our
type checker. In particular, type annotations are added to
|let|-bindings, and the body of every |let| is
either another |let| or a variable. Importantly, this means
the last expression of a sequence of |let| must be a
variable. The output of this algorithm is an expression |Oe|
containing macros (which will be discussed shortly), and the
constraints . Unlike the declarative rules, this algorithm keeps
track of the source type |eta|, which is used to restrict
the range of the type variables. Consequently, every entry of the
typing context  has the form !x! :: !eta!
!X!, meaning that local variable |x| has type
|eta| in the source program and |X| in the target
program. For example, after the lifting algorithm has processed the
function arguments of !filter! in <Ref>,
the typing context contains entries !xs! :: !list!
!X_1! and !y! :: !int!   !X_2!, with freshly
generated type variables !X_1! and !X_2!.

!Mite(theta_0,theta;e_0,e_1,e_2)! |> !Oe!

!Mite(bool,theta;e_0,e_1,e_2)! |> !if e_0 then e_1 else e_2!

!theta! |> !@ite!

!Mite(@bool,theta;e_0,e_1,e_2)! |> !@ite e_0  e_1 e_2!

!MC(theta,theta';e)! |> !Oe!

!data T = !!C eta! ∈
!MC_i(eta_i,T;e)! |> !C_i e!

!@C_i! :: !theta_i->   @T! ∈
!MC_i(theta_i,   @T,e)! |> !@C_i e!

e_0,!!e!!)! |> !Oe!

!data T = !!C eta! ∈
e_0,!!e!!)! |>
!match e_0 with !!C x=>e!

!@Imatch! ::
!   @T->!!(theta->theta')!!->theta'! ∈
!Mmatch(   @T,!!theta!!,theta';
e_0,!!e!!)! |>
!@Imatch e_0 !!(?x:theta=>e)!

!MCOER(theta,theta';e)! |> !Oe!

!theta!  > !theta'! |> !COER!

!MCOER(theta,theta';e)! |> !COERe!

!Mx(theta)! |> !Oe!

!x! :: !theta! |> !Ox! ∈
!Mx(theta)! |> !Ox!

Typed macros

The typed macros, defined in <Ref>, are an essential part of
the output of the lifting algorithm, and permit a form of ad-hoc
polymorphism, that allows the algorithm to cleanly separate constraint
solving from program generation. These macros take types as parameters
and elaborate to expressions, under the contexts ,  and
implicitly. These macros are effectively thin “wrappers” of
their corresponding language constructs and the previously defined
relations. The conditional macro |Mite|, for example,
corresponds to the |if| expression, but the condition may be
oblivious. The constructor macro |MC| is a “smart”
constructor that may construct a -type. The pattern matching
macro |Mmatch| is similar to |MC| but for
eliminating a type compatible with an ADT. Lastly, |MCOER|
and |Mx| is simply a direct wrapper of the mergeable
relation and the lifting context , respectively. Note that the
derivation of these macro are completely determined by the type

<Ref> defines the constraints used in the algorithm,
where |thetaV| is the specification types extended with type
variables.  The constraint !X!   !eta! means type
variable |X| belongs to the compatibility class of
|eta|. In other words, !   [X]   !  = !eta!. Each
macro is accompanied by a constraint on its type parameters. These
constraints mean that the corresponding macros are resolvable. More
formally, this means they can elaborate to some expressions according
to the rules in <Ref> for any expression arguments. As a
result, after solving all constraints and concretizing the type
variables, all macros in the lifted expression |Oe| can be
fully elaborated away.

<Ref> shows a selection of lifting algorithm
rules. Coercions only happen when we lift variables, as in
A-Var. This works because the source program is in ANF, so
each expression is bound to a variable which has the opportunity to
get coerced. For example, the argument to a function or constructor,
in A-App and A-Ctor, is always a variable in ANF,
and recursively lifting it allows the application of
A-Var. On the other hand, the top-level program is always in
!let!-binding form, whose last expression is always a
variable too, allowing coercion of the whole program. However, not all
variables are subject to coercions: the function !x_2! in
A-App, the condition !x_0! in A-If and the
discriminee !x_0! in A-Match are kept as they are,
for example. Coercing these variables would be unnecessary and
undesirable. For example, coercing the condition in a conditional only
makes the generated program more expensive: there is no reason to
coerce from !bool! to !@bool!, and use
!@if! instead of !if!. Another key invariant we
enforce in our algorithmic rules is that every fresh variable is
“guarded” by a compatibility class constraint.  For example, in
A-Abs, the freshly generated variables !X_1!  and
!X_2! belong to the classes !eta_1! and
!eta_2!, respectively. This constraint ensures that every
type variable can be finitely enumerated, as every compatibility class
is a finite set, bounded by the number of available OADTs. As a
result, constraint solving in our context is decidable. Finally, if an
expression is translated to a macro, a corresponding constraint is
added to ensure this macro is resolvable.