Secure Multi-party Computation (MPC) enables a set of parties to

collaboratively compute, using cryptographic protocols, a function

over their private data in a way that the participants do not see

each other's data, they only see the final output. Typical MPC

examples include statistical computations over joint private data,

private set intersection, and auctions. While these applications are

examples of monolithic MPC, richer MPC

applications move between "normal" (i.e., per-party local)

and "secure" (i.e., joint, multi-party secure) modes

repeatedly, resulting overall in mixed-mode computations. For

example, we might use MPC to implement the role of the dealer in a

game of mental poker -- the game will be divided into rounds of

local decision-making (e.g. bidding) and joint interaction

(e.g. dealing). Mixed-mode computations are also used to improve

performance over monolithic secure computations.

Starting with the Fairplay project, several MPC frameworks have been

proposed in the last decade to help programmers write MPC applications in

a high-level language, while the toolchain manages the

low-level details. However, these frameworks are either not expressive

enough to allow writing mixed-mode applications or lack formal

specification, and reasoning capabilities, thereby diminishing the

parties' trust in such tools, and the programs written using

them. Furthermore, none of the frameworks provides a verified

toolchain to run the MPC programs, leaving the potential of security holes

that can compromise the privacy of parties' data.

This dissertation presents language-based techniques to make MPC more

practical and trustworthy. First, it presents the design and

implementation of a new MPC Domain Specific Language, called Wysteria,

for writing rich mixed-mode MPC applications. Wysteria provides several

benefits over previous languages, including a conceptual single thread of

control, generic support for more than two parties, high-level abstractions

for secret shares, and a fully formalized type system and operational

semantics. Using Wysteria, we have implemented several MPC applications,

including, for the first time, a card dealing application.

The dissertation next

presents Wys*, an embedding of Wysteria in F*, a

full-featured verification oriented programming language. Wys*

improves on Wysteria along three lines: (a) It enables programmers to

formally verify the correctness and security properties of their

programs. As far as we know, Wys* is the first language to

provide verification capabilities for MPC programs. (b) It provides a

partially verified toolchain to run MPC programs, and finally (c) It

enables the MPC programs to use, with no extra effort, standard

language constructs from the host language F*, thereby making it

more usable and scalable.

Finally, the dissertation develops static analyses that help optimize

monolithic MPC programs into mixed-mode MPC programs, while providing

similar privacy guarantees as the monolithic versions.