Secure multiparty computation (MPC) allows for
joint computation over private data from
multiple entities, usually backed by powerful
cryptographic techniques that protect
sensitive data. Several high-level programming
languages have been proposed to make writing
MPC applications accessible to
non-experts. These languages typically require
developers to enforce security policies within
the logic of the secure application itself,
making it difficult to update security
requirements, or to experiment with different
policies. This paper presents the design and
implementation
of Taype,
a language that permits security concerns to
be decoupled from the program logic. To do so,
Taype,
provides the first implementation of
oblivious
algebraic data types and
tape
semantics, two language features
recently proposed by a core calculus for
oblivious computation, 𝜆OADT✚. We evaluate
our implementation
of Taype
on a range of benchmarks, demonstrating its
ability to encode a range of security polices
for a rich class of data types.
