\section{Introduction}
Understanding connectivity of a complex dynamical network is a challenging inverse problem in
nonlinear dynamics, with many interdisciplinary applications  in neurosciences, ecology, climate dynamics,
and other fields,
see~\cite{Lehnertz-11,Siguhara_atel-12,Tsonis-Swanson-12}. Many networks, including physically relevant ones like
arrays of lasers and Josephson junctions, power grids, etc., consist of oscillating elements. In this case the essential properties
of the dynamics, especially for weak coupling, can be described in terms of the phases. From the inverse problem
perspective, one faces a task to understand the connectivity of the network from the observations of the oscillatory dynamics of the nodes.
Quite advanced methods have been developed here for a few coupled
oscillators~\cite{Rosenblum-Pikovsky-01,Palus-Stefanovska-03,Tokuda-Jain-Kiss-Hudson-07,Kralemann-08,Penny_et_al-09,%
Kralemann-Pikovsky-Rosenblum-11,Kralemann_etal-13,Kralemann-Pikovsky-Rosenblum-14}. For larger networks
of oscillatory units, approaches based on the information measures and Bayesian estimations have been
developed~\cite{Lobier_etal-14,Wilmer_etal-12,PhysRevE.86.061126,Stankovski12,Ota-Aoyagi-14}. In a recent
paper~\cite{Alderisio_etal-17}, a method allowing to extract some properties of a network but not the exact strengths of coupling,
has been suggested.

In this paper, we present a rather general
approach to reconstruct the coupling phase dynamics functions in a
network of oscillators. It applies also in the cases where all the couplings are different and random,
both to full and to sparse networks. We present several variants of the technique: (i) for the simplest
case of a Kuramoto-Daido
phase dynamics, where the interactions depend on the differences of the phases only; (ii) for
generalized Winfree-type interactions
which are pairwise but otherwise general functions of the phases; and (iii) for hypernetworks with triple interactions.

\section{Hierarchy of phase dynamics models}
\label{sec:hpdm}
Phase model
or phase reduction is a general theoretical tool to describe weakly
coupled oscillators~\cite{Kuramoto-84,Pikovsky-Rosenblum-Kurths-01,Izhikevich-Ermentrout-08}.
It is based on the asymptotic stability of the amplitude of a self-sustained oscillator and on the neutral stability
of its phase. This allows one to assume the amplitudes of coupled oscillators to be nearly constants, and to reduce
the dynamics to that of the phases. In the most general setup, the phases $\theta_i$ of $N$ uncoupled oscillators
just rotate with their natural frequencies
\begin{equation}
\dot\theta_k=\omega_k,\qquad k=1,\ldots,N\;.
\label{eq:p1}
\end{equation}
In the case of coupling they are interdependent:
\begin{equation}
\dot\theta_k=\omega_k+F_k(\theta_1,\ldots,\theta_N)\;.
\label{eq:p2}
\end{equation}
\new{Quite generally, the coupling functions can be represented by Fourier series
\begin{equation}
F_k(\theta_1,\ldots,\theta_N)=\sum_{m_1,m_2,\ldots,m_N}C_k[m_1,m_2,\ldots,m_N]\exp[i(m_1\theta_1+\ldots+m_N\theta_N)]
\label{eq:f1}
\end{equation}
(Note that generally $C_k[0,0,\ldots,0]\neq 0$, what means that there is a contribution of coupling to the natural frequency term;
see Ref.~\cite{Kralemann-08} for a detailed discussion of this issue.)
The number of unknown parameters $C_k[m_1,m_2,\ldots,m_N]$ is very large; however, in many
cases one expect that only a few of them are non-zero.}

Quite often one considers situations simpler than \eqref{eq:p2}, with pairwise coupling between the
oscillators only. In this case, in the
first approximation in the coupling strength, one gets a pairwise coupling in terms of the phases
as well~\cite{Kuramoto-84,Pikovsky-Rosenblum-Kurths-01}:
\begin{equation}
\dot \theta_k=\omega_k+\sum_{j=1,j\neq k}^N Q_{kj}(\theta_j,\theta_k),\qquad 1\leq k\leq N\;.
\label{eq:p3}
\end{equation}
\new{(in this case the general Fourier coefficients \eqref{eq:f1} can be represented as $C_k[m_1,m_2,\ldots,m_N]=\sum_{j\neq k}
\tilde{C}_{kj}(m_j,m_k)$.)}
A particular example of this class is the Winfree model, where the coupling terms $Q_{kj}$ decompose as
\begin{equation}
Q_{kj}(\theta_j,\theta_k)=S(\theta_k) g(\theta_j)\;,
\label{eq:p4}
\end{equation}
where function $S(\theta_k)$ is the phase response curve of oscillator $k$ and function
$g(\theta_j)$ is the driving force
from oscillator $j$. \new{In this case Fourier coefficients $ \tilde{C}_{kj}$ additionally factorise: $ \tilde{C}_{kj}(m_k,m_j)=\tilde{C}_{kj}^S(m_k)
\tilde{C}_{kj}^g(m_j)$.}

Recently, more general cases of phase coupling have been considered~\cite{Kralemann-Pikovsky-Rosenblum-11}.
The next level of complexity in comparison
to the pairwise coupling networks~\eqref{eq:p3} are the hypernetworks with triple coupling
terms~\cite{Komarov-Pikovsky-13,Komarov-Pikovsky-15b,Bick-Ashwin-Rodrigues-16}
\begin{equation}
\dot \theta_k=\omega_k+\sum_{j=1,j\neq k}^N
\sum_{l=1,l\neq k,l> j}^N
G_{kjl}(\theta_k,\theta_j,\theta_l),\qquad 1\leq k\leq N\;,
\label{eq:p5}
\end{equation}
\new{where the condition $l>j$ is needed to count each triplet $kjl$ only once. Here Fourier coefficients have the form
$$C_k[m_1,m_2,\ldots,m_N]=\sum_{j\neq k}\sum_{l=1,l\neq k,l> j}
\tilde{C}_{kjl}(m_j,m_k,m_l).$$}
Such terms also arise for an originally pairwise coupling between the oscillators,
in higher orders of the phase reduction.

The phase model with a pairwise coupling \eqref{eq:p3} can be further reduced under an assumption that
the natural frequencies of the oscillators are large and close to each other, and the coupling is very weak. In this case
one performs an averaging over the fast period of oscillations, so that the resulting coupling terms depend
on the phase differences only. This form of the phase dynamics is often called Kuramoto-Daido model:
\begin{equation}
\dot\theta_k=\omega_k+\sum_{j=1,j\neq k}^N \Gamma_{kj}(\theta_j-\theta_k),\qquad 1\leq k\leq N\;.
\label{eq:p6}
\end{equation}
\new{This model corresponds to an additional diagonal condition on the Fourier coefficients:  $C_k[m_1,m_2,\ldots,m_N]=\sum_{j\neq k}
\tilde{C}_{kj}(m_j)\delta[m_k+m_j]$.}

In this paper we will discuss methods for reconstructing the phase dynamics models (in the order of their complexity:
\eqref{eq:p6},\eqref{eq:p3},\eqref{eq:p5})
from the observations of the dynamics. We will assume here that the phases can be extracted from the time series of the oscillations,
as described, e.g., in Refs.~\cite{Kralemann-08,Kralemann-Pikovsky-Rosenblum-11}.

\section{Reconstruction of phase models}

\subsection{Kuramoto-Daido model}

We consider a set of $N$ phase oscillators $\theta_i(t)$ governed by Eqs.~\eqref{eq:p6}.
We assume that the coupling functions $\Gamma_{kj}$
are arbitrary (e.g., random), as well as the frequencies $\omega_k$,
and the overall dynamics is asynchronous (the case of synchronous dynamics will be treated below separately).
The problem is, how to reconstruct the coupling functions from the multivariate time series $\{\theta_k(t)\}$.
Below for simplicity of presentation, we describe how to reconstruct the coupling functions acting on the first
oscillator, $\Gamma_{1j}$, all other components are obtained similarly.

As the first step we calculate from the data the time derivative $\dot\theta_1$ (the most common approach here is to use
Savitzky-Golay filtering, see \cite{Ahnert-Abel-07}).
Then, we represent the unknown functions $\Gamma$ as a Fourier series
\begin{equation}
\Gamma_{1j}(x)=\sum_{m=1}^M \left(C_{1j,m}\cos m x+S_{1j,m}\sin m x\right)\;.
\label{eq:2}
\end{equation}
\new{Here $M$ is the maximal order of the harmonics in the reconstruction. It is an important parameter of the method
to be discussed in details below.}
At each observation point $t_n$, the following equation should be valid
\begin{equation}
\dot\theta_1(n)=\omega_1+\sum_{j=2}^N \sum_{m=1}^M \left[C_{1j,m}\cos m (\theta_j(n)-\theta_1(n))
+S_{1jm}\sin m(\theta_j(n)-\theta_1(n))\right]\;.
\label{eq:3}
\end{equation}
If we have $L$ observation points, then Eq.~\eqref{eq:3} constitutes $L$ relations for $2M(N-1)+1$
unknown parameters $\{C_{1j,m},S_{1j,m},\omega_1\}$ in \eqref{eq:3}. Because these parameters enter linearly,
determining them can be easily performed with a least squared error approach, i.e. we minimize the mean squared error
\begin{equation}
\sum_{n=1}^L \left(\dot\theta_1(n)- \omega_1-\sum_{j=2}^N \sum_{m=1}^M \left[C_{1j,m}\cos m(\theta_j(n)-\theta_1(n))
+S_{1jm}\sin m(\theta_j(n)-\theta_1(n))\right]\right)^2\;.
\label{eq:mse}
\end{equation}
The unknown parameters $\{C_{1j,m},S_{1j,m},\omega_1\}$ are obtained
by solving the corresponding
system of linear equations, e.g., via singular value decomposition~(SVD, \cite{Press-Flannery-Teukolsky-Vetterling-89}, Ch. 15).
The condition for a successful solution of the problem is $L\geq  2M(N-1)+1$. \new{This relation can be applied if  the data
are not oversampled, i.e. if the observations are independent enough. Lack of independence leads to an underdetermined problem,
what  can be identified by small extremely singular values appearing in course of SVD.}

\subsubsection{Example 1.}
\new{We start with an elementary toy example, where we just construct a network according to the rule~\eqref{eq:2}. It will serve
to clarify the role of parameter $M$, the maximal harmonics order in the reconstruction, in comparison with the maximal order
of the harmonics in the equations.}

In this example we generated a fully connected random network of $N=16$ coupled phase oscillators~\eqref{eq:p4}
by sampling the natural frequencies from the Gaussian distribution  $\mathcal{N}(0,1)$. The coupling
functions have been generated by taking random Fourier harmonics up to order $P$:
\[
C_{kj,m},\;S_{kj,m}=\begin{cases}
\frac{1}{2\sqrt{10}m}\mathcal{N}(0,1), & m\leq P,\\
0& m>P.
\end{cases}
\]
Here $P=5$ is the maximal order of the Fourier components of the coupling.
The dynamics of the network was asynchronous. The phases were sampled with time step $0.01$, and
their time derivatives have been calculated from the time series
using the Savitzky-Golay filter (\cite{Press-Flannery-Teukolsky-Vetterling-89}, Ch. 14).
The time series was stored with time step $\Delta t=1$, \new{to avoid oversampling}.

In the reconstruction procedure as described above, there are two essential parameters: the length of
the time series $L$ and the maximal order of the reconstructed Fourier harmonics $M$. In the case
$M\geq P$, one expects a good reconstruction, and indeed in this case we found that even for a rather short time series $L=200$,
the maximal
error in determining the coupling constants $(C_{1j,m},\;S_{1j,m})$ was less than $10^{-5}$ (Fig.~\ref{fig:reck}).

However, if the number of the harmonics assumed in the reconstruction was insufficient, i.e. $M<P$, then the reconstruction
was not perfect. We illustrate this in Fig.~\ref{fig:reck}. One can see that the quality of reconstruction significantly improves for
longer time series, and when more Fourier harmonics in \eqref{eq:2} are included.

\begin{figure}[!hbt]
\centering
\includegraphics[width=0.6\columnwidth]{fig1_new}
\caption{Errors in the reconstructed coupling  constants$(C_{1j,1},\;S_{1j,1})$  as functions of the maximal Fourier harmonics $M$
(the plots are slightly shifted
horizontally for better visibility). Open circles: short time series $L=200$; squares: the same for $L=2000$.
Black filled circles show median values
of the corresponding errors. }
\label{fig:reck}
\end{figure}

\subsubsection{Example 2.}
In a realistic situation, the coupling functions $\Gamma(\cdot)$ are represented by an infinite Fourier series, where
however higher harmonics are quite small. In this situation, choosing a moderate value
for the maximal reconstruction mode number $M$
yields a good result. We illustrate this by employing the coupling function from the
experiments~\cite{Kiss-Zhai-Hudson-05,Kiss-Zhai-Hudson-06}, where it has been obtained by fitting the observed dynamics
of two electrochemical oscillators. We take the coupling function $H$ corresponding to the relaxation chemical oscillations
(case (c) of Fig. 2 in \cite{Kiss-Zhai-Hudson-05}, see inset in Fig.~\ref{fig:ex_cf2}), and constructed a random network of Kuramoto-Daido type
of $N=32$ phase oscillators, coupled via $H$. The randomness in the networks is not related to the form of the coupling function, but
to the coupling amplitudes $h_{kj}$ and random phase shifts $\Phi_{kj}$:
\begin{equation}
\dot\theta_k=\omega_k+\sum_{j=1,j\neq k}^N h_{kj} H(\theta_j-\theta_k-\Phi_{kj}),\qquad 1\leq k\leq N\;.
\label{eq:exp-1}
\end{equation}
Here the coupling constants are sampled from a  Gaussian distribution; additionally some links are excluded (so that the network is not
fully connected):
\begin{equation}
h_{jk}=\begin{cases} 0.125 \mathcal{N}(0,1)&\text{ with probability } 0.7,\\ 0 &\text{ else, }
\end{cases}
\end{equation}
and the phase shifts $\Phi_{jk}$ are uniformly distributed  in $(0,2\pi)$.

The number of modes $M$ used in the reconstruction is the essential parameter of this problem.
 Fig.~\ref{fig:ex_cf2} shows the reconstructed norm $\lVert \Gamma_{1j}\rVert$
 of the coupling function, for different values of $M$.
This norm is plotted vs the coupling constant $|h_{1j}|$, which is proportional to the norm  $|h_{1j}|\cdot\lVert H\rVert$ of the true coupling
function . Thus,  a linear relation between these quantities indicates for a good reconstruction.
One can see that starting from $M=3$, the quality of the reconstruction is very good.

\begin{figure}[!hbt]
\centering
\includegraphics[width=0.6\textwidth]{fig2_new}
\caption{
Reconstructed norms of coupling functions in~\eqref{eq:exp-1}, for the 1st oscillator in the network. Red pluses:
reconstruction with $M=1$, green crosses: $M=2$, blue squares: $M=3$.
Dashed line helps to
recognize a linear relation between these quantities; \new{ the slope of this line allows estimating $\lVert H\rVert$}. Inset: Experimentally obtained coupling function $H(x)$
for relaxation electro-chemical oscillators,
after~Refs.~\cite{Kiss-Zhai-Hudson-05,Kiss-Zhai-Hudson-06}.}
\label{fig:ex_cf2}
\end{figure}

\subsection{Generic pairwise coupling}
Here we consider the case of a general pairwise-coupled network of phase oscillators~\eqref{eq:p3}. The basic
idea is the same as above, the only difference is in a more general representation of the coupling functions
through a double Fourier series. Let us consider harmonics up to order $P$, and denote the $2P+1$ basis functions as
\begin{equation}
f_{2n-1}(x)=\cos n x,\quad f_{2n}(x)=\sin nx,\quad f_{2P+1}=1\;,\quad n=1,\ldots,P\;.
\label{eq:bf}
\end{equation}
Then, the entries on the r.h.s. of Eq.~\eqref{eq:p3} can be approximated by
\begin{equation}
Q_{1j}(x,y)=\sum_{m=1}^{2P} \sum_{l=1}^{2P+1} q_{jml}^{(1)} f_m(x)f_l(y)\;.
\label{eq:w2}
\end{equation}
In this representation we assume that the forcing does not contain constant terms  (in presence of such terms,
one cannot distinguish, which
driving oscillator produces them), but the coupling function can contain terms
depending on the driving phase only. Thus, each coupling function $Q$ is characterized by
$(2P+1)2P$ real numbers. In the reconstruction we use the same representation \eqref{eq:w2}, however the maximal order
of the harmonics $M$ may deviate from $P$.

The unknown parameters $\{q_{jml}^{(1)},\tilde\omega_1\}$ appear linearly in expression~\eqref{eq:w2}.
Thus, for $L$ observations
of the phases at time instants $t_n$, minimization of the squared error
\begin{equation}
\sum_n\left(\dot\theta_1(n)-\sum_{j=2}^N \sum_{m=1}^{2M} \sum_{l=1}^{2M+1} q_{jml}^{(1)} f_m(\theta_j(n))f_l(\theta_1(n)) -
\tilde\omega_1\right)^2
\label{eq:w4}
\end{equation}
leads to a linear problem of finding the unknown parameters. The length of the time series
should be at least $(N-1)2M(2M+1)+1$ to ensure
solvability, \new{provided that there is no oversampling}.

In the illustration of this approach we consider a fully connected random network with $N=16$. The frequencies are
chosen from the Gaussian distribution $\mathcal{N}(10,1)$ (contrary to the Kuramoto-Daido-type model, here the natural frequencies cannot
be shifted arbitrary, thus one has to assume them to be relatively large compared to the coupling terms).
The coupling constants are chosen as Fourier series with $P=3$ harmonics, the latter are sampled from a Gaussian distribution. The results
of the reconstruction for $M=1,2,3$ are shown in Fig.~\ref{fig:w-er0}. One can see that for $M=P=3$ the reconstruction
is pretty good, while for an approximation with an insufficient number of
harmonics, errors are significant. Here potentially false positives and false negatives may appear from the reconstruction
(cf.~\cite{Alderisio_etal-17}), these features are under ongoing study.

\begin{figure}[!thb]
\centering
\includegraphics[width=0.6\columnwidth]{fig3}
\caption{Results of the reconstruction of the coupling constants for the 1st oscillator in the random network~\eqref{eq:p3},
for $L=5000$: Norms of the reconstructed couplings $|Q_{1j}|^2$  vs the original ones. Pluses: $M=1$, circles: $M=2$, squares: $M=P=3$.
Dashed lines help to see validity of a linear relation between the reconstructed and true norms.}
\label{fig:w-er0}
\end{figure}

\subsection{Reconstruction of a hypernetwork with triple couplings}
\label{sec:h}
Here we briefly discuss reconstruction of a hypernetwork~\eqref{eq:p5}. In terms of the basis functions~\eqref{eq:bf}, one can represent
the r.h.s. of \eqref{eq:p5}, similarly to \eqref{eq:w2}, as
\begin{equation}
G_{1jl}(x,y,z)=\sum_{m=1}^{2P+1} \sum_{p=1}^{2P} \sum_{s=1}^{2P}C_{jlmps}^{(1)}
f_m(x)f_p(y)f_s(z)\;.
\label{eq:h2}
\end{equation}
The squared error can be written, similarly to~\eqref{eq:w4}, as
\begin{equation}
\sum_n\left(\dot\theta_1(n)-\tilde\omega_1-\sum_{j=2}^N \sum_{l=j+1}^N
\sum_{m=1}^{2M+1} \sum_{p=1}^{2M} \sum_{s=1}^{2M}
C_{jlmps}^{(1)} f_m(\theta_1(n))f_p(\theta_j(n))f_s(\theta_l(n))\right)^2\;.
\label{eq:h3}
\end{equation}
As a result, the unknown parameters $\{C_{jlmps}^{(k)},\tilde\omega_k\}$ can be found by singular value decomposition.
The number of these parameters for each $k$ is $(2M)^2(2M+1)(N-1)(N-2)+1$, this number defines the minimal length of the time series
required for the reconstruction. In a numerical example with $N=12$ and $P=M=2$, we generated a random hypernetwork similarly
to examples above. This network could be reconstructed with absolute
accuracy $< 5\cdot 10^{-3}$ with the method described, for $L=5000$ observation points.

\section{Synchronous dynamics}
\label{sec:sd}
In many cases coupled phase oscillators synchronize. In this regime, the mean frequencies coincide and the phase differences
are nearly constant (or exactly constant for the Kuramoto-Daido-type model~\eqref{eq:p6}). In this case a long observation
of the dynamics does not provide any information about the coupling terms.
\new{This can be reformulated also as follows: a good reconstruction of the dynamics on the high-dimensional
torus, spanned by the phases, requires a good ``filling'' of this torus with trajectories. This is possible in the asynchronous case only;
for synchrony just
one periodic trajectory does not ``fill'' the torus and the reconstruction fails.}
Instead, one can effectively ``fill'' the phase space, and to get an information about the coupling terms,
via observations of the transients to the synchronous state. For a large network, many observations of the transients are necessary,
according to the estimations of the number of independent measurements presented above. These transients can be
implemented, e.g., via random resettings of the phases, as suggested in Ref.~\cite{Levnajic-Pikovsky-11}.

We illustrate this approach with  a random network of Kuramoto-Daido type, where coupling functions are taken from
experiments~\cite{Kiss-Zhai-Hudson-05,Kiss-Zhai-Hudson-06} (cf. Fig.~\ref{fig:ex_cf2} above). In a network of $N=32$
elements,
constructed like in the example of Fig.~\ref{fig:ex_cf2}, but where
all the coupling amplitudes $h_{ij}$ have the same sign, and all phase shifts $\Phi_{jk}$ are the same,
one easily achieves synchronization (Fig.~\ref{fig:ex_syn}(a)).
Just an observation of one process like in Fig.~\ref{fig:ex_syn}(a), is insufficient for the reconstruction. However,   many
such transients, obtained via random resettings of the phases from the synchronized state, yield enough independent data points.
The quality of reconstruction crucially depends on the number of resettings, as illustrated in Fig.~\ref{fig:ex_syn}(b). While for 50 resettings
the reconstruction is relatively poor (the values significantly deviate from a linear dependence), with many false
positives (significantly non-zero values for the coupling norms obtained for non-existing links),
already for 80 resettings the quality is rather good (the relation between the norms is linear with high accuracy).

\begin{figure}[!thb]
\centering
\includegraphics[width=0.46\textwidth]{fig4a_new}\hfill
\includegraphics[width=0.46\textwidth]{fig4b_new}
\caption{Panel (a): Transient to a synchronized state where all the phases are locked \new{and instantaneous frequencies
$d\theta_i/dt$ coincide}.
Panel (b): Reconstructed norms of the coupling terms (with the maximal harmonics number $M=3$), vs norms of the true
coupling constants $|h_{kj}|$ in \eqref{eq:exp-1}. Pluses: 50 resettings; circles: 80 resettings. Dashed line helps to
recognize a linear relation between these quantities.}
\label{fig:ex_syn}
\end{figure}

\new{With this example we would like to discuss predictive features of the reconstruction method.  In Fig.~\ref{fig:bif} we
demonstrate, how good is the reconstruction of the bifurcation diagram of the network. We used the reconstruction
of the synchronous network illustrated in Fig.~\ref{fig:ex_syn}. Then, we took the reconstructed equations of type
~\eqref{eq:p6}, and multiplied
all the terms, except for the constant terms $\omega_k$, with a parameter $\varepsilon$.
Then, varying $\varepsilon$, we simulated the reconstructed network equations, calculated the observed frequencies
$\langle\dot\theta\rangle$
of the oscillators, and plotted them vs. bifurcation parameter $\varepsilon$. The same has
been done for the original network (Fig.~\ref{fig:bif}(b)). One
can see a good qualitative agreement between the original and the reconstructed bifurcation diagrams.}

\begin{figure}[!thb]
\centering
\includegraphics[width=0.7\textwidth]{fig5_new}
\caption{Bifurcation diagrams for the network of oscillators, reconstruction of which is illustrated in Fig.~\ref{fig:ex_syn}.
Panel (a): reconstructed network, panel (b): original network.}
\label{fig:bif}
\end{figure}

\section{Conclusions}
In conclusion, we presented a technique to reconstruct a network from the observations of the phase dynamics of the nodes.
We illustrated it with dynamical equations of different complexity, from the simplest Kuramoto-Daido-type
dynamics, depending on the phase differences only, up to generic nonlinear triple interactions, forming a hypernetwork.
The method works well
if the dynamics on the network is irregular. In the case of synchronous dynamics, in order to obtain
enough independent states, one can
perform several random phase resettings and analyze the corresponding transients.

\new{In this study, we focused on the final stage of the network dynamics analysis problem: on the reconstruction of
interactions, provided the time series of the phases are available. Certainly, the necessary preliminary steps like collecting and
preprocessing original oscillating signals, and extraction of the phases from them, may contain many potential sources
of errors. Many aspects of extraction of the phases from the data have been discussed, also in the context of particular
experimental data, in Refs.~\cite{Tokuda-Jain-Kiss-Hudson-07,Kralemann-08,Stankovski12,Ota-Aoyagi-14}. It remains a challenging task
to combine all the steps, from the data collection to the final network reconstruction, and to analyze relevance of
potential uncertainties at each stage. The main goal of the present study was to demonstrate feasibility of the phase dynamics
reconstruction for a large variety of models, from simple Kuramoto-type ones to complex hypernetworks. Indeed, in particular applications
the complexity of the phase equations is not known in advance. Applying different variants of the reconstruction methods
described in this study, one can select the most adequate level of phase dynamics complexity, describing real interactions.
}

\new{As has been mentioned above, applicability of the approach heavily depends on the synchronization level in the network.
If synchronization is weak (what happens if the variance of the natural frequencies in the network is rather large compared
to the coupling level), the phases are to large extent independent, they cover a large part of the phase space, and the
reconstruction works well. In the opposite case of complete synchrony (what means that the variance of the natural frequencies is
rather small compared to the coupling level), the phases are highly correlated and in fact one has just one periodic orbit,
not suitable for reconstruction. Here, as shown in Section~\ref{sec:sd}, observing transient dynamics can help. However, for this
one needs a possibility to perturb the system, moreover many different perturbations are necessary. In the intermediate case (when
the spread of the natural frequencies is of the same order as the coupling constants), one typically observes a mixed situation:
some oscillators synchronize forming clusters, other remain asynchronous. Here one can consider two situations.
\begin{enumerate}
\item External perturbations are not possible. Here direct application of the reconstruction method described can potentially lead to
a  problem where ambiguous combination of parameters appear. In terms of the Singular Value Decomposition
approach such a situation is related to extremely small singular values.
In this case, one could combine synchronous oscillators, forming a cluster, to
one ``effective'' oscillatory element, and characterized it with just one phase. Then, one will have  a smaller effective network,
where, however, all elements will be not synchronous. Here one can apply the method of reconstruction described above. The method
will, however, provide an ``effective'' coupling to a cluster, and will not allow resolving the couplings to elements of the cluster.
\item If external perturbations are possible, these can be used to destroy clusters -- one does not need to apply them to all the oscillators,
just the existing partial synchrony should be destroyed. Then, application of the approach based on the
transients (Section~\ref{sec:sd}), will allow
reconstructing all the connections.
\end{enumerate}
}

The method is based on the simple linear system of equations, resulting from  the minimization of squared error.
 In this sense it is similar to that
 of Ref.~\cite{Shandilya-Timme-11}, where a general setup of high-dimensional
 dynamical systems coupled via a network of nonlinear interactions was considered. In Ref.~\cite{Shandilya-Timme-11}
 it was, however, assumed that
 all nonlinear functions defining the local dynamics and the coupling are known, so the only unknown
 parameters, the coupling constants, could be reconstructed via minimization
 of the squared error, provided the full high-dimensional time series
 from all sites are available. In our case, no preliminary knowledge about the coupling functions is needed.
 Moreover, we assumed all the couplings to be generally different. If one knows that the coupling functions
 in a network are the same, but still unknown, the number of unknown parameters in the reconstruction decreases. Here
an iterative method for solution of nonlinear equations resulting from the minimizing
of the squared error, suggested in Ref.~\cite{Cestnik-Rosenblum-17}, could be applied.
 Another type of error minimization, mostly suitable
 to reconstruction of very sparse networks, is known as compressive sensing, see
 Ref.~\cite{Wang-Lai-Grebogi-16} where its applications  to network
 reconstruction are reviewed.

\new{Throughout the paper we assumed that the object under study is a network of weakly coupled periodic oscillators. Here
the application of phase reduction is well justified. One can potentially avoid phase reduction by using the full reconstruction
of the equations. For lump oscillators, an efficient method for the reconstruction of the nonlinear dynamical
equations based on the ``Sparse Identification of Nonlinear Dynamics'' has been recently
suggested in Ref.~\cite{Brunton_etal-16}. Here one heavily uses the fact, that only several nonlinear terms are important for the dynamics,
so that the equations are sparse in the space of possible functions. One can potentially extend this approach to networks, where
connections are sparse and are described by simple linear or nonlinear terms. The method, however, requires data of all the dynamical
variables from all the nodes.}

\section{Acknowledgments}
Study presented in Sects. \ref{sec:h},\ref{sec:sd}
was supported by Russian Science Foundation [Contract No. 17 12 01534].

\def$'${$'$}


\subsubsection*{\textbf{\emph{#1}}}}
\newcommand{\Paragraph}[1]{\paragraph*{#1.}}

\usepackage{amsmath}
\usepackage{mathpartir}
\usepackage{multirow}
\usepackage{amssymb}

\begin{document}
\title{\ourlang: A DSL for Verified \\Secure Multi-party Computations}

\iflong
\author{Aseem Rastogi\inst{1} \and
Nikhil Swamy\inst{1} \and
Michael Hicks\inst{2}}

\authorrunning{Rastogi et al.}
\institute{Microsoft Research\\
\email{\{aseemr,nswamy\}@microsoft.com} \and
University of Maryland\\
\email{mwh@cs.umd.edu}}
\else
\author{}
\institute{}
\fi

\maketitle

\begin{abstract}
Secure multi-party computation (\mc) enables a set of mutually
distrusting parties to cooperatively compute, using a cryptographic
protocol, a function over their private data.
This paper presents \ourlang, a new domain-specific language (DSL)
for
writing \emph{mixed-mode} \mc{s}. \ourlang is an embedded DSL hosted in \fstar, a
verification-oriented, effectful programming language.
\ourlang source programs are
essentially \fstar{} programs written in a custom \mc effect, meaning
that the programmers can use \fstar{}'s logic to verify the correctness
and security properties of their programs. To reason about the
distributed runtime semantics of these programs, we formalize a deep
embedding of \ourlang, also in \fstar{}. We mechanize the necessary
metatheory to prove that the properties verified for the \ourlang
source programs carry over to the distributed, multi-party
semantics. Finally, we use \fstar{}'s extraction to
extract an interpreter that we have proved matches this semantics,
yielding a partially verified implementation. \ourlang is the first
DSL to enable formal verification of \mc programs.
We have implemented several \mc protocols in \ourlang, including
private set intersection, joint median, and an \mc-based card dealing
application, and have verified their correctness and security.
\end{abstract}

\section{Introduction}
\label{sec:intro}

Secure multi-party computation (\mc) enables two
or more parties to compute a function $f$ over their private inputs
$x_i$ so that parties don't see each others' inputs, but
rather only see the output $f(x_1,...,x_n)$. Using a trusted
third party to compute $f$ would achieve this goal, but in fact we can
achieve it using one of a variety of cryptographic protocols carried
out only among the
participants~\cite{shamir1980mental, Yao, GMW, BMR}.
One example use of \mc is private set intersection (PSI): the
$x_i$ could be individuals' personal interests, and the function $f$
computes their intersection, revealing which interests the group has
in common, but not any interests that they don't. \mc has also been used for
auctions~\cite{Bogetoft2009}, detecting tax fraud~\cite{taxfraudsmc},
managing supply chains~\cite{supplychainsmc}, privacy
preserving statistical analysis~\cite{UT:Kamm15}, and more recently
for machine learning tasks~\cite{ezpc,Buscher:2018:HCH:3243734.3243786,gazelle,secureml,Liu:2017:ONN:3133956.3134056}.

Typically, cryptographic protocols expect $f$ to be specified as a
boolean or arithmetic circuit. Programming directly with circuits and
cryptography is painful,
so starting with the Fairplay project~\cite{fairplay} many researchers
have designed higher-level domain-specific languages (DSLs) in which
to program
\mc{s}~\cite{Huang11,viff,Malka2011,fairplaymp,Holzer12,Nielsen07,Nielsen09,sharemind,Schropfer2011,wysteria,Liu2014,Laud:2015:DLL:2810103.2813664,Crockett:2018:ALC:3243734.3243828,Araki:2018:GSC:3243734.3243854,Buscher:2018:HCH:3243734.3243786,frigate}.
These DSLs compile source code to
circuits which are then given to the underlying protocol. While doing this
undoubtedly makes it easier to program \mc{s}, these languages still
have several drawbacks regarding both security and usability.

This paper presents \ourlang, a new \mc DSL that addresses several
problems in prior DSLs. Unlike most previous \mc DSLs, \ourlang is not a
standalone language, but is rather an embedded DSL hosted in
\fstar~\cite{fstar2016}, a full-featured, verification-oriented, effectful
programming language. \ourlang has the following two distinguishing
elements:

\Paragraph{1. A program logic for \mc} (\S\ref{sec:overview} and \S\ref{sec:formal}.)
In their most general form, \mc applications are \emph{mixed-mode}:
they consist of parties
performing (potentially different)
local, in-clear computations (e.g. I/O, preprocessing
inputs) interleaved with joint, secure computations. \ourlang is the
first MPC DSL to provide a program logic to formally reason about the
\emph{correctness and security} of such applications,
e.g., to prove that the outputs will not reveal too much information
about a party's inputs~\cite{mardziel13belief}.\footnote{Our attacker
  model is the ``honest-but-curious'' model where the attackers are
  the participants themselves,
  who play their
  roles in the protocol faithfully, but are motivated to deduce as much as they
  can about the other participants' secrets by observing the
  protocol. \S\ref{sec:wysts} makes the security model of \ourlang more precise.}

To avoid reasoning about separate programs for each
  party, \ourlang builds on the basic programming model of the
  Wysteria \mc DSL~\cite{wysteria} that allows applications to be
  written as a single specification. \ourlang presents a
\emph{shallow embedding} of the Wysteria programming model in \fstar.
When writing \ourlang source programs, programmers essentially write
\fstar programs in a new \ls{Wys} effect,
against a library of \mc combinators. The pre- and
postcondition specifications on the combinators encode a program logic
for MPC. The logic provides
\emph{observable traces}---a novel addition to the Wysteria
semantics---which programmers can use to
specify security properties such as delimited release~\cite{sm03delimited}.
Since \ourlang programs are \fstar programs, \fstar computes
verification conditions (VCs) for
them which are discharged using Z3~\cite{z3} as usual.

We prove the soundness of the program logic---that the properties proven about
the \ourlang source programs carry over when these programs are run by
multiple parties in a distributed manner---also in \fstar. The proof connects
the pre- and postconditions of the \ourlang combinators to their distributed
semantics in two steps.
First, we implement the combinators in \fstar, proving the
validity of their pre- and postconditions of against their implementation.
Next, we reason about this implementation and the distributed runtime
semantics through a deepembedding of \ourlang in \fstar.
Essentially, we deep-embed the \ourlang combinator abstract syntax trees (ASTs)
as an \fstar
datatype and formalize two operational semantics for them:
a conceptual single-threaded semantics that models their \fstar implementation,
and the actual distributed
semantics that models the multi-party runs of the
programs. We prove, in \fstar, that the single-threaded
semantics is sound with respect to the distributed semantics (\S\ref{sec:formal}).
While we use \fstar, the program logic is general and
it should be possible to embed it in other verification frameworks
(e.g., in Coq, in the style of Hoare Type Theory~\cite{ynot-icfp08}).

\paragraph*{2. A full-featured, partially verified implementation}
(\S\ref{sec:formal}.)
\ourlang's implementation is, in part, formally verified. The hope is
that formal verification will reduce the occurrence of security
threatening bugs, as it has in prior
work~\cite{csmith,Leroy2009Formal,BhargavanFKPS13,polarssl,export:122884}.

We define an interpreter in \fstar that operates over the \ourlang
ASTs produced by a custom \fstar
extraction for the \ls{Wys} effect.
While the local computations are executed locally by the interpreter,
the interpreter compiles secure-computation ASTs
to circuits, on the fly, and executes them using the Goldreich, Micali and
Wigderson (GMW) multi-party computation protocol~\citep{GMW}. The
\ourlang AST (and hence the interpreter) does not ``bake in'' standard
\fstar{} constructs like numbers and lists. Rather, inherited language
features appear abstractly in the AST, and their semantics is handled
by a foreign function interface (FFI). This permits \ourlang programs
to take advantage of existing code and libraries available in \fstar{}.

To prove the interpreter behaves correctly, we prove, in \fstar,
that it correctly implements the formalized distributed semantics.
The circuit library and the GMW implementation
are not verified---while it is possible to verify the circuit
library~\cite{Almeida:2017:FVS:3133956.3134017}, verifying a GMW
implementation is an open research question.
But the stage is set for verified versions to be plugged into
the \ourlang codebase. We characterize the Trusted Computing Base
(TCB) of the \ourlang toolchain in \S\ref{sec:impl}.

Using \ourlang we have
implemented several programs, including PSI,
joint median, and a card dealing application
(\S\ref{sec:apps}). For PSI and joint median we
implement two versions: a straightforward one and an optimized one that
improves performance but increases
the number of adversary-observable events. We formally
prove that the optimized and unoptimized
versions are equivalent,
both functionally and w.r.t. privacy of parties' inputs.
Our card dealing application relies on \ourlang's support
for secret shares~\citep{Shamir79}. We formally prove that the card
dealing algorithm always deals a fresh card.

In sum, \ourlang constitutes the first DSL that supports proving
security and correctness properties about \mc programs, which are
executed by a partially verified implementation of a full-featured
language. No prior DSL provides these benefits
(\S\ref{sec:related}).
The \ourlang implementation, example programs, and
proofs are publicly available on
\iflong
Github at \url{https://github.com/FStarLang/FStar/tree/stratified_last/examples/wysteria}.\footnote{This development was
  done on an older \fstar version, but the core ideas of what we
  present here apply to the present version as well.}
\else
Github.\footnote{This development was
  done on an older \fstar version, but the core ideas of what we
  present here should apply to the present version as well.

\fi

\section{Verifying and deploying \ourlang programs}
\label{sec:overview}

We illustrate the main concepts of \ourlang by showing, in
several stages, how to program, optimize, and verify the two-party
joint median example~\cite{Kerschbaum11,rastogi13knowledge}.
In this example, two parties, Alice and Bob, each have a set of $n$ distinct,
locally sorted integers, and they want to compute the median of the union of
their sets without revealing
anything else; our running example fixes $n = 2$, for simplicity.

\subsection{Secure computations with \ls$as_sec$}
\label{sec:assec}
In \ourlang, as in its predecessor Wysteria~\cite{wysteria},
an \mc is written as a single specification that
executes in one of two \emph{computation modes}. The primary mode is called \ls$sec$
mode. In it, a computation is carried out using a \mc protocol
among multiple principals on separate hosts. Here is joint median in \ourlang:
\begin{lstlisting}[xleftmargin=1em, numbers=left, frame=single]
let median a b in_a in_b =
  as_sec {a, b} (fun () -> let cmp = fst (reveal in_a) > fst (reveal in_b) in $\label{line:acomp}$
                        let x3 = if cmp then fst (reveal in_a) else snd (reveal in_a) in $\label{line:acull}$
                        let y3 = if cmp then snd (reveal in_b) else fst (reveal in_a) in $\label{line:bcull}$
                        if x3 > y3 then y3 else x3)
\end{lstlisting}
The four arguments to \ls$median$ are, respectively, principal
identifiers for Alice and Bob, and Alice and Bob's secret inputs expressed as
tuples.
In \ourlang, values specific to each
principal are
\emph{sealed} with the principal's name (which appears in the sealed
container's type). As such, the types of \ls$in_a$ and \ls$in_b$
are, respectively, \ls$sealed {a} (int * int)$ and
\ls$sealed {b} (int * int)$.
The \ls$as_sec ps f$
construct indicates that thunk \ls$f$
should be run in \ls$sec$ mode among principals in the set \ls{ps}.
In this mode, the code has access to the secrets of the principals
\ls$ps$,
which it can reveal using the \ls{reveal} coercion.
As we will see later, the type of \ls{reveal} ensures that
parties cannot \ls{reveal} each others' inputs outside \ls{sec}
mode.\footnote{The runtime
representation of \ls{sealed {a} v} at \ls{b}'s host is an opaque constant
$\bullet$ (\S\ref{sec:deployoverview}).} Also note that the
code freely uses standard \fstar library functions like \ls{fst} and \ls{snd}.
The example extends naturally
to $n > 2$~\cite{10.1007/978-3-540-24676-3_3}.

To run this program, both Alice and Bob would start a \ourlang
interpreter at their host and direct it to run the \ls$median$ function
Upon reaching the
\ls$as_sec$ thunk, the interpreters coordinate with each other to compute the
result using the underlying \mc protocol.
\S\ref{sec:deployoverview} provides more details.

\subsection{Optimizing \ls{median} with \ls$as_par$}

Although \ls$median$ gets the job done, it can
be inefficient for large $n$.
However, it turns out if we reveal the result
of comparison on line~\ref{line:acomp} to both the parties,
then the computation on line~\ref{line:acull} (resp. line~\ref{line:bcull})
can be performed locally
by Alice (resp. Bob) without need of cryptography. Doing so can
massively improve performance:
previous work~\cite{Kerschbaum11} has observed a
$30\times$ speedup for $n = 64$.

This optimized variant is a \emph{mixed-mode} computation, where participants
perform some local computations interleaved with small, jointly
evaluated secure computations. \ourlang's second
computation mode, \ls$par$ mode, supports such mixed-mode computations. The
construct \ls$as_par ps f$ states that each principal in \ls$ps$
should locally execute the thunk \ls$f$, simultaneously; any
principal not in the set \ls$ps$ simply skips the computation. Within
\ls$f$, while running in \ls$par$ mode, principals may engage in
secure computations via \ls$as_sec$.

Here
is an optimized version of \ls{median} using \ls{as_par}:

\begin{lstlisting}[xleftmargin=1em, numbers=left, frame=single]
let median_opt a b in_a in_b =
 let cmp = as_sec {a, b} (fun () -> fst (reveal in_a) > fst (reveal in_b)) in$\label{line:optacomp}$
 let x3 = as_par {a} (fun () -> if cmp then fst (reveal in_a) else snd (reveal (in_a))) in $\label{line:optacull}$
 let y3 = as_par {b} (fun () -> if cmp then snd (reveal in_b) else fst (reveal (in_b))) in $\label{line:optbcull}$
 as_sec {a, b} (fun () -> if reveal x3 > reveal y3 then reveal y3 else reveal x3) $\label{line:finalm}$
\end{lstlisting}

The secure computation on (line~\ref{line:optacomp}) \emph{only}
computes \ls{cmp} and returns the result to both the parties. Line~\ref{line:optacull}
is then a \ls{par} mode computation involving only Alice
in which she discards one of her inputs based on \ls{cmp}.
Similarly, on line~\ref{line:optbcull}, Bob discards
one of his inputs. Finally, line~\ref{line:finalm} compares the remaining
inputs using \ls{as_sec} and returns the result as the final median.

One might wonder whether \ls$par$ mode is necessary. Could we
program the local parts of a mixed-mode program in normal \fstar, and
use a special compiler to convert the \ls$sec$ mode parts to circuits
and pass them to a GMW \mc service? We could, but it would complicate
both writing \mc{s} and formally reasoning that the whole computation is
correct and secure.
In particular, programmers would need to write one program for each
party that performs a different local computation (as in
\ls{median_opt}). The potential interleaving among local computations
and their synchronization behavior when securely computing together
would be a source of possible error and thus must be considered in any
proof. For example, Alice's code might have a bug in it that prevents
it from reaching a synchronization point with Bob, to do a GMW-based
\mc. For \ourlang, the situation is much simpler. Programmers may
write and maintain a single program. This program can be formally
reasoned about directly using a SIMD-style, ``single-threaded''
semantics, per the soundness result from \S\ref{sec:metatheory}. This
semantics permits reasoning about the coordinated behavior of multiple
principals, without worry about the effects of interleavings or wrong
synchronizations. Thanks to \ls{par} mode, invariants about
coordinated local computations are directly evident since we can
soundly assume about lockstep behavior (e.g., loop iterations in the
PSI example in \S\ref{sec:apps}).

\subsection{Embedding a type system for \ourlang in \fstar}
\label{sec:wysts}

Designing high-level, multi-party computations is relatively
easy using Wysteria's abstractions. Before trying to run such a
computation, we might wonder:

\begin{enumerate}
\item Is it \emph{realizable}? For example, does a computation
that is claimed to be executed only by some principals \ls$ps$ (e.g.,
using an \ls$as_par ps$ or an \ls$as_sec ps$) only ever access data
belonging to \ls$ps$?

\item Is it \emph{correct?} For example, does \ls$median_opt$
  correctly compute the median of Alice and Bob's inputs?

\item Is it \emph{secure}? For example, do the optimizations in
  \ls$median_opt$, which produce more visible outputs, potentially
  leak more about the inputs?
\end{enumerate}

By embedding \ourlang in \fstar and leveraging its extensible,
monadic, dependent type-and-effect system, we address each of these
three questions.
We define a new indexed monad called \ls$Wys$ for computations that
use \mc combinators \ls$as_sec$ and \ls$as_par$. Using \ls$Wys$
along with the \ls$sealed$ type, we can ensure that protocols are
realizable. Using \fstar's capabilities for formal verification, we
can reason about a computation's correctness. By characterizing
observable events as part of \ls$Wys$, we can define trace
properties of \mc programs, to reason about security.

To elaborate on the last: we are interested in \emph{application-level} security
properties, assuming that the underlying
cryptographic \mc protocol (GMW~\cite{GMW} in our implementation) is secure.
In particular,
the \ls{Wys} monad models the \emph{ideal} behavior of \ls{sec} mode---a
secure computation reveals only the final output and nothing
else. Thus the programmer could reason, for example, that optimized
\mc programs reveal no more than their unoptimized versions.
To relate the proofs over ideal functionality to the actual
implementation, as is standard, we rely on the security of the
cryptographic protocol and the composition theorem~\cite{Canetti:2000:SCM:2724987.2725177}
to postulate that the implementation securely realizes the ideal
specification.

\Paragraph{The \ls$Wys$ monad} The \ls$Wys$ monad provides several features. First, all DSL code is
typed in this monad, encapsulating it from the rest of \fstar. Within
the monad, computations and their specifications can make use of two
kinds of \emph{ghost state}: \emph{modes} and \emph{traces}.
The mode of a computation indicates whether the computation is running
in an \ls$as_par$ or in an \ls$as_sec$ context.
The trace of a computation records the sequence and nesting structure
of  outputs of the jointly executed \ls$as_sec$ expressions---the result of a
computation and its trace constitute its observable behavior.
The \ls$Wys$ monad is, in essence, the product of a reader monad on
modes and a writer monad on traces~\cite{Wadler:1995:MFP:647698.734146,Moggi:1991:NCM:116981.116984}.

Formally, we define the following \fstar types for modes and traces. A
mode \ls$Mode m ps$ is a pair of a mode tag (either \ls$Par$
or \ls$Sec$) and a set of principals \ls$ps$. A \ls$trace$ is a forest
of trace element (\ls$telt$) trees. The leaves of the trees record
messages \ls$TMsg x$ that are received as the result of executing
an \ls$as_sec$ thunk. The tree structure represented by the
\ls$TScope ps t$ nodes record the set of principals that are able to
observe the messages in the trace \ls$t$.

\begin{lstlisting}
type mtag = Par | Sec
type mode = Mode: m:mtag -> ps:prins -> mode
type telt = | TMsg  : x:$\alpha$ -> telt | TScope: ps:prins -> t:list telt -> telt
type trace = list telt
\end{lstlisting}

Every \ourlang computation $e$ has a monadic computation
type \ls$Wys t pre post$.
The type indicates that $e$ is in the \ls$Wys$ monad (so it may
perform multi-party computations);
\ls$t$ is its result type;
\ls$pre$ is a pre-condition on the mode in which \ls$e$ may be executed;
and \ls$post$ is a post-condition relating the computation's mode, its
result value, and its trace of observable events.
When run in a context with mode \ls$m$ satisfying the pre-condition
predicate \ls$pre m$, $e$ may produce the trace \ls$tr$,
and if and when it returns, the result is
a \ls$t$-typed value \ls$v$ validating \ls@post m v tr@.
The style of indexing a monad with a computation's pre- and
post-condition is a standard
technique~\citep{atkey09parameterised,nmb08htt,fstar2016}---we defer
the definition of the monad's \ls$bind$ and \ls$return$ to the
actual implementation and focus instead on specifications of \ourlang
specific combinators.
We describe
\ls$as_sec$, \ls$reveal$, and \ls$as_par$, and how we give them types in
\fstar, leaving the rest to
Figure~\ref{fig:wysstar-api} in the Appendix.
By convention, any free variables in the type signatures are
universally prenex quantified.

\Paragraph{Defining \ls$as_sec$ in \ourlang}
~

\begin{lstlisting}[numbers=left]
val as_sec: ps:prins -> f:(unit -> Wys a pre post) -> Wys a
  (requires (fun m     -> m=Mode Par ps /\ pre (Mode Sec ps))) $\label{line:assec-requires}$
  (ensures  (fun m r tr -> tr=[TMsg r] /\ exists t. post (Mode Sec ps) r t)))$\label{line:assec-ensures}$
\end{lstlisting}

The type of \ls$as_sec$ is \emph{dependent} on the first
parameter, \ls$ps$. Its second argument \ls$f$ is the thunk to be
evaluated in \ls$sec$ mode. The result's computation type has the
form
\ls@Wys a (requires $\phi$) (ensures $\psi$)@, for some pre-condition
and post-condition predicates $\phi$ and $\psi$, respectively.
We use the
\ls$requires$ and \ls$ensures$ keywords for readability---they are not semantically significant.

The pre-condition of \ls$as_sec$ is a predicate on the mode \ls$m$ of
the computation in whose context
\ls$as_sec ps f$ is called.
For all the \ls$ps$ to jointly execute \ls$f$, we require all
of them to transition to perform the \ls$as_sec ps f$ call
simultaneously, i.e., the current mode must be
\ls$Mode Par ps$.
We also require the pre-condition \ls$pre$
of \ls$f$ to be valid once the mode has transitioned to
\ls$Mode Sec ps$---line~\ref{line:assec-requires} says just this.

The post-condition of \ls$as_sec$ is a predicate
relating the initial mode \ls$m$, the result \ls$r:a$, and the
trace \ls$tr$ of the computation.
Line~\ref{line:assec-ensures} states that the trace of a secure
computation \ls$as_sec ps f$ is just a singleton \ls$[TMsg r]$,
reflecting that its execution reveals only result
\ls$r$.
Additionally, it ensures that the result \ls$r$ is related to the mode
in which \ls$f$ is run (\ls$Mode Sec ps$) and some trace \ls$t$
according to \ls$post$, the post-condition of \ls$f$. The API models the
``ideal functionality'' of secure computation protocols (such as GMW)
where the participants only observe the final result.

\Paragraph{Defining \ls$reveal$ in \ourlang} As discussed earlier, a
value \ls$v$ of type \ls$sealed ps t$ encapsulates a \ls$t$ value that
can be accessed by calling \ls$reveal v$. This call should only
succeed under certain circumstances. For example, in \ls$par$ mode, Bob
should not be able to reveal a value of type \ls$sealed {Alice} int$.
The type of \ls$reveal$ makes the access control rules clear:

\begin{lstlisting}
val unseal: sealed ps $\alpha$ -> Ghost $\alpha$

val reveal: x:sealed ps $\alpha$ -> Wys $\alpha$
  (requires (fun m -> m.mode=Par ==> m.ps $\subseteq$ ps /\ m.mode=Sec ==> m.ps $\cap$ ps $\neq$ $\emptyset$))
  (ensures (fun m r tr -> r=unseal x /\ tr=[]))
\end{lstlisting}

The \ls{unseal} function is a \ls{Ghost} function, meaning that it can
only be used in specifications for reasoning purposes. On the other
hand, \ls{reveal} can be called in the concrete \ourlang programs.
Its precondition says that when executing in \ls$Mode Par ps'$,
\emph{all} current participants must be listed in the seal, i.e.,
\ls@ps' $\subseteq$ ps@.
However, when executing in \ls$Mode Sec ps'$, only a subset of
current participants is required:
\ls@ps' $\cap$ ps $\neq$ $\emptyset$@.
This is because the secure computation is executed jointly by all of
\ls$ps'$, so it can access any of their individual data.
The postcondition of \ls{reveal} relates the result \ls{r} to the
argument \ls{x} using the \ls{unseal} function.

\Paragraph{Defining \ls$as_par$ in \ourlang}
~

\begin{lstlisting}[numbers=left]
val as_par: ps:prins -> (unit -> Wys a pre post) -> Wys (sealed ps a)
  (requires (fun m     -> m.mode=Par    /\ ps $\subseteq$ m.ps /\ can_seal ps a /\ pre (Mode Par ps)))
  (ensures  (fun m r tr -> exists t. tr=[TScope ps t] /\ post (Mode Par ps) (unseal r) t)))
\end{lstlisting}

The type of \ls{as_par} enforces the current mode to be \ls{Par},
and \ls{ps} to be a subset of current principals. Importantly,
the API scopes the trace \ls{t} of \ls{f} to model the fact that
any observables of \ls{f} are only visible to the
principals in \ls{ps}. Note that \ls{as_sec} did not require such scoping,
as there \ls{ps} and the set of current principals in \ls{m} are the same.

\subsection{Correctness and security verification}
\label{sec:verification}

Using the \ls$Wys$ monad and the \ls$sealed$ type, we can write down
precise types for our \ls$median$ and \ls$median_opt$ programs,
proving various useful properties. We discuss
the statements of the main lemmas and the overall proof structure.
By programming the protocols as a single specification using the high-level
abstractions provided by \ourlang, our proofs are relatively straightforward---in
all the proofs of this section, \fstar required no additional hints.
In particular, we rely heavily on the view that both parties execute
(different fragments of) the same code, thus avoiding the unwieldy
task of reasoning about low-level message passing.

\Paragraph{Correctness and security of \ls{median}} We first define a pure specification of median of
two \ls{int} tuples:

\begin{lstlisting}
let median_of (x1, x2) (y1, y2) = let (_, m, _, _) = sort x1 x2 y1 y2 in m
\end{lstlisting}

Further, we capture the preconditions using the following predicate:

\begin{lstlisting}
let median_pre (x1, x2) (y1, y2) = x1 < x2 $\wedge$ y1 < y2 $\wedge$ distinct x1 x2 y1 y2
\end{lstlisting}

Using these, we prove the following top-level specification for \ls{median}:

\begin{lstlisting}
val median: in_a:sealed {a} (int * int) -> in_b:sealed {b} (int * int) -> Wys int
  (requires (fun m -> m = Mode Par {a, b}))  (* should be called in the Par mode *)
  (ensures (fun m r tr -> let in_a, in_b = unseal in_a, unseal in_b in
      (median_pre in_a in_b ==> r = median_of in_a in_b) /\    (* functional correctness *)
      tr = [TMsg ra]))    (* trace is just the final value *)
\end{lstlisting}

This signature establishes that when Alice and Bob
simultaneously execute \ls$median$ (in \ls$Par$
mode), with secrets \ls$in_a$ and \ls$in_b$, then if and when the
protocol terminates,
(a) if their inputs satisfy the
precondition \ls{median_pre}, then the result is the joint median of
their inputs and (b) the observable trace consists
only of the final result, as there is but  a single \ls{as_sec} thunk
in \ls{median}, i.e., it is \emph{secure}.

\Paragraph{Correctness and security of \ls{median_opt}}
The security proof of \ls{median_opt} is particularly interesting, because
the program intentionally reveals more than just the final result,
i.e., the output of the first comparison.
We would like to verify that this additional information does not
compromise the privacy of the parties' inputs.
To do this, we take the following approach.

First, we characterize the observable trace of \ls{median_opt} as a pure,
specification-only function. Then, using relational reasoning, we prove
a \emph{noninteference with delimited release} property~\citep{sm03delimited}
on these traces. Essentially we prove that, for two runs of \ls{median_opt}
where Bob's inputs and the output median are the same, the observable traces
are also same irrespective of Alice's inputs. Thus, from Alice's perspective, the
observable trace does not reveal more to Bob than what the output already does.
We prove this property symmetrically for Bob.

We start by defining a trace function for \ls{median_opt}:

\begin{lstlisting}
let opt_trace a b (x1, _) (y1, _) m = [
  TMsg (x1 > y1);  (* observable from the first as_sec *)
  TScope {a} []; TScope {b} [];  (* observables from two local as_par *)
  TMsg m ]  (* observable from the final as_sec *)
\end{lstlisting}

\noindent A trace will have four elements: output of the first \ls{as_sec}
computation, two empty scoped traces for the two local \ls{as_par}
computations, and the final output.

Using this function, we prove correctness of \ls{median_opt}, thus:

\begin{lstlisting}
val median_opt: in_a:sealed {a} (int * int) -> in_b:sealed {b} (int * int) -> Wys int
  (requires (fun m -> m = Mode Par {a, b}))  (* should be called in the Par mode *)
  (ensures (fun m r tr -> let in_a = unseal in_a in let in_b = unseal in_b in
    (median_pre in_a in_b ==> r = median_of in_a in_b) /\  (* functional correctness *)
    tr = opt_trace a b in_a in_b m  (* opt_trace precisely describes the observable trace *)

\end{lstlisting}

The delimited release property is then captured by the following lemma:

\begin{lstlisting}
val median_opt_is_secure_for_alice: a:prin -> b:prin
  -> in_a$_1$:(int * int) -> in_a$_2$:(int * int) ->  in_b:(int * int) (* possibly diff a1, a2 *)
  -> Lemma (requires (median_pre in_a$_1$ in_b /\ median_pre in_a$_2$ in_b /\
                      median_of in_a$_1$ in_b = median_of in_a$_2$ in_b)) (* but same median *)
            (ensures  (opt_trace a b in_a$_1$ in_b (median_of in_a$_1$ in_b) = (* ensures .. *)
                     opt_trace a b in_a$_2$ in_b (median_of in_a$_2$ in_b))) (* .. same trace *)
\end{lstlisting}

The lemma proves that for two runs of \ls$median_opt$ where Bob's
input and the final output remain same, but Alice's inputs vary
arbitrarily, the observable traces are the same. As such, no more
information about information leaks about Alice's inputs via the traces than
what is already revealed by the output. We
also prove a symmetrical lemma \ls{median_opt_is_secure_for_bob}.

In short, because the \ls{Wys} monad provides programmers
with the observable traces in the logic, they can then be used to prove
properties, relational or otherwise, in the pure fragment of
\fstar outside the \ls{Wys} monad. We present more examples and their
verification details in \S\ref{sec:apps}.

\subsection{Deploying \ourlang programs}
\label{sec:deployoverview}

\begin{figure}[t]
\centering
  \includegraphics[scale=0.55]{sec2fig.png}
  \caption{Architecture of an \ourlang deployment}
  \label{fig:distarch}
\end{figure}

Having defined a proved-secure \mc program in \ourlang, how do we run it?
Doing so requires the following steps (Figure~\ref{fig:distarch}).
First, we run the
\fstar compiler in a special mode that \emph{extracts} the \ourlang
code (say \ls{psi.fst}),
into the \ourlang AST as a data structure (in \ls{psi.ml}).
Except for the \ourlang specific nodes (\ls{as_sec}, \ls{as_par}, etc.),
the rest of the program is extracted
into \emph{FFI nodes} that indicate the use of, or calls into,
functionality provided by \fstar itself.

The next step is for each party to run the extracted
AST using the \ourlang interpreter. This interpreter is written in
\fstar and we have proved (see \S\ref{sec:impl}) it implements a deep embedding of the \ourlang
semantics, also specified in \fstar (Figures~\ref{fig:dsl-proto-semantics} and \ref{fig:dsl-tgt-semantics},
\S\ref{sec:formal}). The
interpreter is extracted to OCaml by the usual \fstar extraction.
Each party's interpreter executes the AST locally
until it reaches an \ls$as_sec ps f$ node,
where the interpreter's back-end compiles
\ls$f$, on-the-fly, for particular values of the secrets in \ls$f$'s
environment, to a boolean circuit. First-order, loop-free code can be
compiled to a circuit; \ourlang provides specialized support for
several common combinators
(e.g., \ls{fst}, \ls{snd}, list combinators such as \ls$List.intersect$, \ls$List.mem$,
\ls$List.nth$ etc.).

The circuit is handed to a library by Choi et al.~\citet{cryptoeprint:2011:257}
that implements the GMW~\citep{GMW} \mc protocol.
Running the GMW protocol involves the parties in \ls{ps}
generating and communicating (XOR-based) secret shares \citep{Shamir79} for
their secret inputs, and then cooperatively evaluating the boolean
circuit for \ls$f$ over them.

One obvious question is how both parties are able to get this process
off the ground, given that they don't know some of the inputs (e.g., other
parties' secrets).
The \ls{sealed} abstraction helps here.
Recall that for \ls$median$,
the types of the inputs are of the form \ls$sealed {a} (int * int)$ and
\ls$sealed {b} (int * int)$. When the program is run on Alice's host,
the former will be a pair of Alice's values, whereas the latter
will be an opaque constant (which we denote as $\bullet$). The
reverse will be true on Bob's host. When the circuit is constructed,
each principal links their non-opaque inputs to the relevant input
wires of the circuit. Similarly, the output map component of each party
is derived from their output wires in the circuit, and thus,
each party only gets to see their own output.

\section{Formalizing and implementing \ourlang}
\label{sec:formal}

\newcommand{\ext}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\ensuremath{s}}{\ensuremath{s}}

\begin{figure}[t]
\[
\begin{array}{@{}@{}rlcl}
\text{Principal} \quad p & & & \text{        Principal set} \quad \ensuremath{s} \quad \text{                    FFI const} \quad \ext{c}, \ext{f}\\
\text{Constant} & c & ::= & p \mid \ensuremath{s} \mid () \mid \kw{true} \mid \kw{false} \mid \ext{c}\\
\text{Expression} & e & ::=
& \kw{as_par}\;e_1\;e_2 \mid \kw{as_sec}\;e_1\;e_2 \mid \kw{seal}\;e_1\;e_2 \mid \kw{reveal}\;e \mid \kw{ffi}\;\ext{f}\;\bar{e}\\
& & \mid & \kw{mkmap}\;e_1\;e_2 \mid \kw{project}\;e_1\;e_2 \mid \kw{concat}\;e_1\;e_2\\
& & \mid & c \mid x \mid \kw{let}\;x = e_1\;\kw{in}\;e_2 \mid \lambda x.e \mid e_1\;e_2 \mid \kw{fix}\;f.\lambda x.e \mid \kw{if}\;e_1\;\kw{then}\;e_2\;\kw{else}\;e_3\\
\end{array}
\]
\caption{\ourlang syntax}
\label{fig:dsl-syntax}
\end{figure}

In the previous section, we presented examples of verifying properties
about \ourlang programs using \fstar{}'s logic. However,
these programs are not executed using the \fstar{} (single-threaded) semantics; they
have a distributed semantics involving multiple parties. So,
how do the properties that we verify using \fstar{} carry over?

In this section, we present the metatheory that answers this
question. First, we formalize the \ourlang single-threaded (ST) semantics,
that
faithfully models the \fstar{} semantics of the \ourlang API presented
in \S\ref{sec:overview}. Next, we formalize
the distributed (DS) semantics that multiple parties use
to run \ourlang programs. Then we prove the former is \emph{sound}
with respect to the latter, so that properties proved of programs
under ST apply when run under DS\@. We have mechanized the proof of
this theorem in \fstar{}.

\subsection{Syntax}

Figure~\ref{fig:dsl-syntax} shows the complete
syntax of \ourlang. Principals and principal sets are first-class
values, and are denoted by $p$ and $\ensuremath{s}$ respectively. Constants in
the language also include $()$ (unit), booleans, and FFI
constants \ext{c}.
Expressions $e$ include the regular forms for functions, applications,
let bindings, etc. and the \ourlang-specific constructs. Among the
ones that we have not seen in \S\ref{sec:overview}, expression
$\kw{mkmap}\;e_1\;e_2$ creates a map from principals in $e_1$
(which is a principal set) to the value computed by
$e_2$. $\kw{project}\;e_1\;e_2$ projects the value of principal $e_1$
from the map $e_2$, and $\kw{concat}\;e_1\;e_2$ concatenates the two
maps. The maps are used if an \ls{as_sec} computation returns
different outputs to the parties.

Host language (i.e., \fstar) constructs are also part of the syntax of
\ourlang, including constants \ext{c} include strings, integers, lists,
tuples, etc. Likewise, host language functions/primitives can be called
from \ourlang---$\kw{ffi}\;\ext{f}\;\bar{e}$ is the invocation of a
host-language function \ext{f} with arguments
$\bar{e}$. The FFI confers two benefits. First, it simplifies the core
language while still allowing full consideration of security relevant
properties. Second, it helps the language scale by incorporating
many of the standard features, libraries, etc. from the host language.

\begin{figure}[t]
\[
\begin{array}{@{}rlcl}
\text{Map} & m & ::= & \cdot \mid m[p \mapsto v]\\
\text{Value} & v & ::= & p \mid \ensuremath{s} \mid () \mid \kw{true} \mid \kw{false} \mid \kw{sealed}\;\ensuremath{s}\;v \mid m \mid \ext{v} \mid (L, \lambda x.e) \mid (L, \kw{fix}\;f.\lambda x.e) \mid \bullet\\
\text{Mode} & M & ::= & \kw{Par}\;\ensuremath{s} \mid \kw{Sec}\;\ensuremath{s}\\
\text{Context} & E & ::= & \langle\rangle \mid \kw{as_par}\;\langle\rangle\;e \mid \kw{as_par}\;v\;\langle\rangle \mid \kw{as_sec}\;\langle\rangle\;e \mid \kw{as_sec}\;v\;\langle\rangle \mid \ldots\\
\text{Frame} & F & ::= & (M, L, E, T)\\
\text{Stack} & X & ::= & \cdot \mid F,X\\
\text{Environment} & L & ::= & \cdot \mid L[x \mapsto v]\\
\text{Trace element} & t & ::= & \kw{TMsg}\;v \mid \kw{TScope}\;\ensuremath{s}\;T\\
\text{Trace} & T & ::= & \cdot \mid t, T\\
\text{Configuration} & C & ::= & M; X; L; T; e\\\\
\text{Par component} & P & ::= & \cdot \mid P[p \mapsto C]\\
\text{Sec component} & S & ::= & \cdot \mid S[\ensuremath{s} \mapsto C]\\
\text{Protocol} & \pi & ::= & P; S\\
\end{array}
\]
\caption{Runtime configuration syntax}
\label{fig:dsl-runtime-syntax}
\end{figure}

\begin{figure*}[t]
\[
\begin{array}{l}
\inferrule*[lab=S-aspar]
{
e_1 = \kw{as_par}\;\ensuremath{s}\;(L_1, \lambda x.e) \quad M = \kw{Par}\;\ensuremath{s}_1 \quad \ensuremath{s} \subseteq \ensuremath{s}_1 \\\\
X_1 = (M; L; \kw{seal}\;\ensuremath{s}\;\langle\rangle; T), X
}
{
M; X; L; T; e_1 \rightarrow \kw{Par}\;\ensuremath{s};X_1; L_1[x \mapsto ()]; \cdot; e
}
\hspace{0.3cm}
\inferrule*[lab=S-parret]
{
X = (M_1; L_1; \kw{seal}\;\ensuremath{s}\;\langle\rangle; T_1), X_1\\\\
\kw{can_seal}\;\ensuremath{s}\;v \quad
T_2 = \kw{append}\;T_1\;[\kw{TScope}\;\ensuremath{s}\;T]
}
{
M; X; L; T; v \rightarrow M_1; X_1; L_1; T_2; \kw{sealed}\;\ensuremath{s}\;v
}
\\\\
\inferrule*[lab=S-assec]
{
e_1 = \kw{as_sec}\;\ensuremath{s}\;(L_1, \lambda x.e) \quad M = \kw{Par}\;\ensuremath{s} \\\\
X_1 = (M; L; \langle\rangle\; T), X
}
{
M; X; L; T; e_1  \rightarrow \kw{Sec}\;\ensuremath{s}; X_1; L_1[x \mapsto ()]; \cdot; e
}
\hspace{0.9cm}
\inferrule*[lab=S-secret]
{
\kw{is_sec}\;M \quad X = (M_1; L_1; \langle\rangle; T), X_1 \\\\
T_1 = \kw{append}\;T\;[\kw{TMsg}\;v] \quad
}
{
M; X; L; \cdot; v \rightarrow M_1; X_1; L_1; T_1; v
}
\end{array}
\]
\caption{\ourlang ST semantics (selected rules)}
\label{fig:src-semantics}
\end{figure*}

\subsection{Single-threaded semantics}
\label{sec:st}
We formalize the semantics in the style of Hieb and
Felleisen~\cite{felleisen1992revised}, where the redex is chosen by
(standard, not shown) \emph{evaluation contexts} $E$, which prescribe
left-to-right, call-by-value evaluation order.
The ST semantics, a model of the \fstar{} semantics and the \ourlang API,
defines a judgment
$C \rightarrow C'$ that represents a single step of an abstract
machine (Figure~\ref{fig:src-semantics}). Here, $C$ is a \emph{configuration} $M; X; L; T; e$. This
five-tuple consists of a mode $M$, a stack $X$, a local environment
$L$, a trace $T$, and an expression $e$. The syntax for these elements
is given in Figure~\ref{fig:dsl-runtime-syntax}. The value form
$\ext{v}$ represents the host language (FFI) values. The stack and
environment are standard; trace $T$ and mode $M$ were discussed in
the previous section.

For space reasons, we focus on the two main \ourlang constructs \kw{as_par}
and \kw{as_sec}.
Appendix B shows rules for other \ourlang specific constructs.

Rules {\sc{S-aspar}} and {\sc{S-parret}} (Figure~\ref{fig:src-semantics})
reduce an \kw{as_par}
expression once its arguments are fully evaluated---its first argument $s$
is a principal set, while the second argument $(L_1, \lambda x.e)$ is a closure
where $L_1$ captures the free variables of thunk $\lambda x.e$. {\sc{S-aspar}}
first checks that the current mode $M$ is \kw{Par} and contains all the
principals from the set $\ensuremath{s}$. It then pushes a
$\kw{seal}\;\ensuremath{s}\;\langle\rangle$ frame on the stack, and starts evaluating
$e$ under the environment $L_1[x \mapsto ()]$. The rule {\sc{S-asparret}} pops the frame and
seals the result,
so that it is accessible only to the
principals in $\ensuremath{s}$. The rule also creates a trace element
$\kw{TScope}\;\ensuremath{s}\;T$, essentially making observations during the
reduction of $e$ (i.e., $T$) visible only to principals in $\ensuremath{s}$.

Turning to \kw{as_sec}, the rule {\sc{S-assec}} checks the precondition of the API,
and the rule {\sc{S-assecret}} generates a trace observation $\kw{TMsg}\;v$,
as per the postcondition of the API. As mentioned before, \ls{as_sec} semantics
models the ideal, trusted third-party semantics of secure computations where the
participants only observe the final output. We
can confirm that the rules implement the types of \kw{as_par} and
\kw{as_sec} shown in \S\ref{sec:overview}.

\begin{figure*}[t]
\[
\begin{array}{l}
\inferrule*[lab=P-par]
{
C \leadsto C'
}
{
P[p \mapsto C]; S \longrightarrow P[p \mapsto C']; S
}
\hspace{0.6cm}
\inferrule*[right=P-enter]
{
\forall p \in \ensuremath{s}.\;P[p].e = \kw{as_sec}\;\ensuremath{s}\;(L_p, \lambda x.e) \\\\
\ensuremath{s} \not\in \kw{dom}(S) \quad
L = \kw{combine}\;\bar{L}_p \quad
}
{
P; S \longrightarrow P; S[\ensuremath{s} \mapsto \kw{Sec}\;\ensuremath{s}; \cdot; L[x \mapsto ()]; \cdot; e]
}
\\\\
\inferrule*[lab=P-sec]
{
C \rightarrow C'
}
{
P; S[\ensuremath{s} \mapsto C] \longrightarrow P; S[\ensuremath{s} \mapsto C']
}
\hspace{0.6cm}
\inferrule*[lab=P-exit]
{
S[\ensuremath{s}] = \kw{Sec}\;\ensuremath{s}; \cdot; L; T; v \\\\
P' = \forall p \in \ensuremath{s}.\;P[p \mapsto P[p] \triangleleft (\kw{slice_v}\;p\;v)] \quad
S' = S \setminus \ensuremath{s}
}
{
P; S \longrightarrow P'; S'
}
\end{array}
\]
\caption{Distributed semantics, multi-party rules}
\label{fig:dsl-proto-semantics}
\end{figure*}

\begin{figure*}[t]
\[
\begin{array}{l}
\inferrule*[lab=L-aspar1]
{
e_1 = \kw{as_par}\;\ensuremath{s}\;(L_1, \lambda x.e) \quad p \in \ensuremath{s} \\\\
X_1 = (M; L; \kw{seal}\;\ensuremath{s}\;\langle\rangle; T), X
}
{
\kw{Par}\;p; X; L; T; e_1 \leadsto \kw{Par}\;p; X_1; L_1[x \mapsto ()]; \cdot; e
}
\hspace{0.3cm}
\inferrule*[lab=L-parret]
{
X = (M; L_1; \kw{seal}\;\ensuremath{s}\;\langle\rangle; T_1), X_1 \\\\
T_2 = \kw{append}\;T_1\;T \quad v_1 = \kw{sealed}\;\ensuremath{s}\;v
}
{
\kw{Par}\;p; X; L; T; v \leadsto \kw{Par}\;p; X_1; L_1; T_2; v_1
}
\\\\
\hspace{1cm}\inferrule*[left=L-aspar2]
{
p \not\in \ensuremath{s}
}
{
\kw{Par}\;p; X; L; T; \kw{as_par}\;\ensuremath{s}\;(L_1, \lambda x.e) \leadsto \kw{Par}\;p; X; L; T; \kw{sealed}\;\ensuremath{s}\;\bullet
}
\end{array}
\]
\caption{Distributed semantics, selected local rules {\small{(the mode $M$ is always \kw{Par}\;$p$)}}}
\label{fig:dsl-tgt-semantics}
\end{figure*}

\subsection{Distributed semantics}
\label{sec:ds}
In the DS semantics, principals
evaluate the same program locally and
asynchronously until they reach a secure computation, at which point
they synchronize to jointly perform the computation.
The semantics consists of two parts: (a) a judgment of the form
$\pi \longrightarrow \pi'$ (Figure~\ref{fig:dsl-proto-semantics}),
where a protocol $\pi$ is a tuple $(P; S)$
such that $P$ maps each principal to its local
configuration and $S$ maps a set of principals to the configuration of
an ongoing, secure computation; and (b) a local evaluation judgment
$C \leadsto C'$ (Figure~\ref{fig:dsl-tgt-semantics}) to model how a single
principal behaves while in \ls$par$ mode.

Rule {\sc{P-Par}} in Figure~\ref{fig:dsl-proto-semantics} models a
single party taking a step, per the local evaluation rules.
Figure~\ref{fig:dsl-tgt-semantics} shows these rules
for \ls{as_par}.
(See Appendix B for more local evaluation rules.)
A principal either participates in the
\kw{as_par} computation, or skips it. Rules {\sc{L-aspar1}} and {\sc{L-parret}}
handle the case when $p \in \ensuremath{s}$, and so, the principal $p$
participates in the computation. The rules closely mirror the
corresponding ST semantics rules in Figure~\ref{fig:src-semantics}. One difference in the rule
{\sc{L-asparret}} is that the trace $T$ is not scoped. In the DS
semantics, traces only contain \kw{TMsg} elements; i.e., a trace is
the (flat) list of secure computation outputs observed by that
active principal.
If $p \not\in \ensuremath{s}$, then the principal skips the computation with the
result being a sealed value containing the opaque constant $\bullet$ (rule
{\sc{L-aspar2}}). The contents of the sealed value do not matter,
since the principal will not be allowed to unseal the value anyway.

As should be the case, there
are no local rules for \kw{as_sec}---to perform a
secure computation parties need to combine their data and jointly do
the computation. Rule {\sc{P-enter}} in Figure~\ref{fig:dsl-proto-semantics}
handles the case when principals enter a secure
computation. It requires that all
the principals $p \in \ensuremath{s}$ must have the expression form
$\kw{as_sec}\;\ensuremath{s}\;(L_p, \lambda x.e)$, where $L_p$ is their local
environment associated with the closure. Each party's local
environment contains its secret values (in addition to some public
values). Conceptually, a secure computation \emph{combines} these
environments, thereby producing a joint view, and evaluates $e$ under
the combination. We define an auxiliary \ls$combine$ function for this
purpose:

\begin{lstlisting}
combine_v ($\bullet$, v) = v
combine_v (v, $\bullet$) = v
combine_v (sealed s v$_1$, sealed s v$_2$) = sealed s (combine_v v$_1$ v$_2$)
...
\end{lstlisting}

The rule {\sc{P-enter}} combines the principals' environments, and
creates a new entry in the $S$ map. The principals are now waiting for
the secure computation to finish. Rule {\sc{P-sec}} models a stepping rule
inside the \ls{sec} mode.

The rule {\sc{P-exit}} applies when a secure computation has
completed and returns results to the waiting principals. If the
secure computation terminates with value $v$, each principal $p$ gets
the value $\kw{slice_v}\;p\;v$. The \kw{slice_v} function is
analogous to \kw{combine}, but in the opposite direction---it
strips off the parts of $v$ that are not accessible to $p$:

\begin{lstlisting}
slice_v p (sealed s v) = sealed s $\bullet$, if p $\not\in$ s
slice_v p (sealed s v) = sealed s (slice_v p v), if p $\in$ s
...
\end{lstlisting}

In the rule {\sc{P-exit}}, the $\triangleleft$ notation is defined as:

\vspace{0.1cm}
$M; X; L; T; \_\;\triangleleft\;v = M; X; L; \kw{append}\;T\;[\kw{TMsg}\;v]; v$
\vspace{0.1cm}

That is, the returned value is also added to the principal's trace to
note their observation of the value.

\subsection{Metatheory}
\label{sec:metatheory}

Our goal is to show that the ST semantics faithfully represents the
semantics of \ourlang programs as they are executed by multiple parties, i.e.,
according to the DS semantics. We do this by proving
\emph{simulation} of the ST semantics by the DS semantics, and by
proving \emph{confluence} of the DS semantics. Our \fstar{}
development mechanizes all the metatheory presented in this section.

\Paragraph{Simulation} We define a \kw{slice}\;\ensuremath{s}\;$C$
function that returns the corresponding protocol $\pi_C$ for an ST
configuration $C$. In the $P$ component of $\pi_C$, each
principal $p \in \ensuremath{s}$ is mapped to their \emph{slice} of the
protocol. For slicing values, we use the same \kw{slice_v}
function as before. Traces are sliced as follows:

\begin{lstlisting}
slice_tr p (TMsg v) = [TMsg (slice_v p v)]
slice_tr p (TScope s T) = slice_tr p T,  if p $\in$ s
slice_tr p (TScope s T) = [],  if p $\not\in$ s
\end{lstlisting}

The slice of an expression (e.g., the source program) is itself. For
all other components of $C$, slice functions are defined analogously.

We say that $C$ is \emph{terminal} if it is in \kw{Par} mode and is fully
reduced to a value
(i.e. when $C = \_; X; \_; \_; e$,  $e$ is a value and $X$ is empty). Similarly, a protocol
$\pi = (P, S)$ is terminal if $S$ is empty and all the local
configurations in $P$ are terminal. The simulation theorem
is then the following:

\begin{theorem}[Simulation of ST by DS]
Let $\ensuremath{s}$ be the set of all principals. If $C_1 \rightarrow^{*} C_2$,
and $C_2$ is terminal, then there exists some derivation
$(\kw{slice}\;\ensuremath{s}\;C_1) \longrightarrow^{*} (\kw{slice}\;\ensuremath{s}\;C_2)$
such that
$(\kw{slice}\;\ensuremath{s}\;C_2)$ is terminal.
\end{theorem}

To state \emph{confluence}, we first
define the notion of \emph{strong termination}.

\begin{definition}[Strong termination]
If all possible runs of protocol $\pi$ terminate at $\pi_t$, we say
$\pi$ \emph{strongly terminates in $\pi_t$}, written $\pi \Downarrow
\pi_t$.
\end{definition}

Our confluence result then says:

\begin{theorem}[Confluence of DS]
If $\pi \longrightarrow^{*} \pi_t$ and $\pi_t$ is terminal, then
$\pi \Downarrow \pi_t$.
\end{theorem}

Combining the two theorems, we get a corollary that establishes the
soundness of the ST semantics w.r.t. the DS semantics:

\begin{corollary}[Soundness of ST semantics]
Let $\ensuremath{s}$ be the set of all principals. If $C_1 \rightarrow^* C_2$,
and $C_2$ is terminal, then
$(\kw{slice}\;\ensuremath{s}\;C_1) \Downarrow (\kw{slice}\;\ensuremath{s}\;C_2)$.
\end{corollary}

Now suppose that for a \ourlang source program, we prove in \fstar{}
a post-condition that the result is \kw{sealed} \kw{alice} $n$, for
some $n > 0$. By the soundness of the ST semantics, we can conclude
that when the program is run in the DS semantics, it may diverge, but
if it terminates, \kw{alice}'s output will also
be \kw{sealed} \kw{alice} $n$, and for all other principals their
outputs will be \kw{sealed} \kw{alice} $\bullet$. Aside from the
correspondence on results, our semantics also covers correspondence
on traces. Thus the
correctness and security properties that we prove about a \ourlang
program using \fstar's logic, hold for the program that actually runs.

\subsection{Implementation}
\label{sec:impl}

The formal semantics presented in the prior section is
mechanized as
an inductive type in \fstar. This style is useful for
proving properties, but does not directly translate to an
implementation. Therefore, we implement an interpretation function
\ls$step$ in \fstar and prove that it corresponds to the rules; i.e.,
that for all input configurations $C$, \ls{step}$(C) = C'$ implies
that $C \rightarrow C'$ according to the
semantics. Then, the core of each principal's implementation is
an \fstar{} stub function \kw{tstep} that repeatedly invokes \ls{step} on the
AST of the source program (produced by the \fstar extractor run
in a custom mode), unless the AST is an \kw{as_sec}
node. Functions \ls{step} and \kw{tstep} are extracted to OCaml by the
standard \fstar{} extraction process.

Local evaluation is not defined for \ls$as_sec$, so the stub
implements what amounts to {\sc{P-enter}} and {\sc{P-exit}} from
Figure~\ref{fig:dsl-proto-semantics}. When the stub notices the
program has reached an \kw{as_sec} expression, it calls into a circuit
library we have written that converts the AST of the second argument
of \kw{as_sec} to a boolean circuit. This circuit and the encoded inputs are
communicated to a co-hosted server that implements the GMW \mc
protocol~\cite{cryptoeprint:2011:257}.
The server evaluates the circuit, coordinating with the GMW
servers of the other principals, and sends back the result. The
circuit library decodes the result and returns it to the stub.
The stub then carries on with the local evaluation. Our FFI interface
currently provides a form of monomorphic, first-order
interoperability between the (dynamically typed) interpreter and the
host language.

Our \fstar{} formalization of the \ourlang semantics, including the AST
specification, is 1900 lines of code. This formalization is used both
by the metatheory as well as by the (executable) interpreter. The
metatheory that connects the ST and DS semantics
(\S\ref{sec:formal}) is 3000 lines. The interpreter
and its correctness proof are another 290 lines of \fstar{} code.
The interpreter \kw{step} function is essentially a
big switch-case on the current expression, that calls into the
functions from the semantics specification. The \kw{tstep} stub is
another 15 lines. The size of the circuit
library, not including the GMW implementation, is 836 lines.
The stub, the implementation of GMW, the circuit library, and \fstar
toolchain (including the custom \ourlang extraction mode) are part
of our Trusted Computing Base (TCB).

\section{Applications}
\label{sec:apps}

In addition to joint median, presented in \S\ref{sec:overview}, we have
implemented and proved properties of two other \mc applications,
\emph{dealing for on-line card games} and \emph{private set intersection} (PSI).

\Paragraph{Card dealing} We have implemented an \mc-based card
dealing application in \ourlang. Such an application can play the
role of the dealer in a game of online poker, thereby eliminating the
need to trust the game portal for card dealing. The application relies
on \ourlang's support for \emph{secret
shares}~\citep{Shamir79}. Using secret shares, the participating
parties can share a value in a way that none of the parties can
observe the actual value individually (each party's share consists of
some random-looking bytes), but they can recover the value by combining
their shares in \ls{sec} mode.

In the application, the parties maintain a list of secret shares of
already dealt cards (the number of already dealt cards is public
information). To deal a new card, each party first generates a random
number locally. The parties then perform a secure computation to
compute the sum of their random numbers modulo 52, let's call it
$n$. The output of the secure computation is secret shares of $n$. Before
declaring $n$ as the newly dealt card, the parties needs to ensure
that the card $n$ has not already been dealt. To do so, they
iterate over the list of secret shares of already dealt cards, and for
each element of the list, check that it is different from $n$. The
check is performed in a secure computation that simply combines the shares
of $n$, combines the shares of the list element, and checks the
equality of the two values. If $n$ is different from all the
previously dealt cards, it is declared to be the new card, else the
parties repeat the protocol by again generating a fresh random number
each.

\ourlang provides the following API for secret shares:

\begin{lstlisting}
type Sh: Type -> Type
type can_sh: Type -> Type
assume Cansh_int: can_sh int

val v_of_sh: sh:Sh $\alpha$ -> Ghost $\alpha$
val ps_of_sh: sh:Sh $\alpha$ -> Ghost prins

val mk_sh: x:$\alpha$ -> Wys (Sh $\alpha$)
    (requires (fun m -> m.mode = Sec /\ can_sh $\alpha$))
    (ensures (fun m r tr -> v_of_sh r = x /\ ps_of_sh r = m.ps /\ tr = [])
val comb_sh: x:Sh $\alpha$ -> Wys $\alpha$ (requires (fun m -> m.mode = Sec /\ ps_of_sh x = m.ps))
                             (ensures (fun m r tr -> v_of_sh x = r /\ tr = [])
\end{lstlisting}

Type \ls{Sh $\alpha$} types the shares of values of type \ls{$\alpha$}. Our
implementation currently supports shares of \ls{int} values only;
the \ls{can_sh} predicate enforces this restriction on the source
programs. Extending secret shares support to other
types (such as pairs) should be straightforward (as in~\cite{wysteria}).
Functions \ls{v_of_sh}
and \ls{ps_of_sh} are marked \ls{Ghost}, meaning that they can only
be used in specifications for reasoning purposes. In the concrete
code, shares are created and combined using the \ls{mk_sh}
and \ls{comb_sh} functions. Together, the specifications of these
functions enforce that the shares are created and combined by the same
set of parties (through \ls{ps_of_sh}), and that \ls{comb_sh} recovers
the original value (through \ls{v_of_sh}).
The \ourlang interpreter transparently handles the low-level details of
extracting shares from the GMW implementation of Choi et
al. (\ls{mk_sh}), and reconstituting the shares back (\ls{comb_sh}).

In addition to implementing the card dealing application
in \ourlang, we have formally verified that the
returned card is fresh. The signature of the function that checks for
freshness of the newly dealt card is as follows (\ls{abc} is the set
of three parties in the computation):

\begin{lstlisting}
val check_fresh: l:list (Sh int){forall s'. mem s' l ==> ps_of_sh s' = abc}
  -> s:Sh int{ps_of_sh s = abc}
  -> Wys bool (requires (fun m -> m = Mode Par abc))
    (ensures (fun _ r _ -> r <==> (forall s'. mem s' l ==> not (v_of_sh s' = v_of_sh s))))
\end{lstlisting}

The specification says that the function takes two arguments: \ls{l}
is the list of secret shares of already dealt cards, and \ls{s} is the
secret shares of the newly dealt card. The function returns a boolean
\ls{r} that is \ls{true} iff the concrete value (\ls{v_of_sh})
of \ls{s} is different from the concrete values of all the elements
of the list \ls{l}. Using \fstar{}, we verify that the implementation
of \ls{check_fresh} meets this specification.

\Paragraph{PSI}
Consider a dating application that enables its users to compute their
common interests without revealing all of them.
This is an instance of the more general private set intersection
(PSI) problem~\cite{Huang12}.

We implement a straightforward version of PSI in \ourlang:

\begin{lstlisting}[frame=single]
let psi a b (input_a:sealed {a} (list int)) (input_b:sealed {b} (list int)) (l_a:int) (l_b:int) =
  as_sec {a,b} (fun () -> List.intersect (reveal input_a) (reveal input_b) l_a l_b)
\end{lstlisting}

\noindent where the input sets are expressed as lists with public lengths.

Huang et al.~\cite{Huang12} provide an optimized PSI algorithm
that performs much better when the density of common elements in
the two sets is high. We implement their algorithm in \ourlang.
The optimized version consists of two nested loops -- an outer loop for Alice's
set and an inner loop for Bob's -- where an iteration of the inner loop
compares the current element of Alice's set with the current element of
Bob's. The nested loops are written using \ls{as_par} so that both Alice and
Bob execute the loops in lockstep (note that the set sizes are public), while
the comparison in the inner loop happens using \ls{as_sec}.
Instead of naive \ls{l_a * l_b} comparisons, Huang et al.~\cite{Huang12} observe
that once an element of Alice's set \ls{ax}
matches an element of Bob's set \ls{bx}, the inner loop can return immediately,
skipping the comparisons of \ls{ax} with the rest of Bob's set. Furthermore,
\ls{bx} can be removed from Bob's set, excluding it from any further comparisons
with other elements in Alice's set. Since there are no repeats in the input sets,
all the excluded comparisons are guaranteed to be false. We show the full code
and its performance comparison with \ls{psi} in
Appendix A.

As with the median example from \S\ref{sec:overview}, the optimized PSI
intentionally reveals more for performance gains. As such, we would like
to verify that the optimizations do not reveal more about parties' inputs.
We take the following stepwise refinement approach. First, we characterize the trace of
the optimized implementation as a pure function \ls{trace_psi_opt la lb}
(omitted for space reasons),
and show that the trace of \ls{psi_opt} is precisely \ls{trace_psi_opt la lb}.

Then, we define an intermediate PSI implementation that has the same
nested loop structure, but performs
\ls{l_a * l_b} comparisons without any optimizations. We characterize
the trace of this intermediate implementation as the pure function
\ls{trace_psi}, and show that it precisely captures the trace.

To show that \ls{trace_psi} does not reveal more than the intersection of
the input sets, we prove the following lemma.

\newcommand\defeq{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\sffamily def}}}{=}}}

\begin{lstlisting}
$\Psi$ la$_0$ la$_1$ lb$_0$ lb$_1$ $\defeq$ (* possibly diff input sets, but with *)
  la$_0$ $\cap$ lb$_0$ = la$_1$ $\cap$ lb$_1$ /\ (* intersections the same *)
  length la$_0$ = length la$_1$ /\ length lb$_0$ = length lb$_1$ (* lengths the same *)

val psi__interim_is_secure: la$_0$:_ -> lb$_0$:_ -> la$_1$:_ -> lb$_1$:_ -> Lemma
  (requires ($\Psi$ la$_0$ la$_1$ lb$_0$ lb$_1$)) (ensures (permutation (trace_psi la$_0$ lb$_0$) (trace_psi la$_1$ lb$_1$)))
\end{lstlisting}

The lemma essentially says that for two runs on same length inputs,
if the output is the same, then the resulting traces are permutation of
each other.\footnote{Holding Bob's
  (resp. Alice's) inputs fixed and varying Alice's (resp. Bob's) inputs,
  as done for \ls$median$ in \S\ref{sec:verification},
  is covered by this more general property.}
We can reason about the traces of \ls$psi_interim$ up to
permutation because Alice has no prior knowledge of the choice of
representation of Bob's set (Bob can shuffle his list), so cannot
learn anything from a permutation of the trace.\footnote{We could formalize
this observation using a probabilistic, relational variant
of \fstar~\citep{rfstar14}.} This establishes the security of
\ls{psi_interim}.

Finally, we can connect \ls$psi_interim$ to \ls$psi_opt$
by showing that there exists a function \ls$f$, such that for
any trace \ls$tr=trace_psi la lb$, the trace of \ls$psi_opt$,
\ls$trace_psi_opt la lb$, can be computed by
\ls$f (length la) (length lb) tr$.
In other words, the trace produced by the optimized implementation can be computed
using a function of information already available to Alice (or Bob)
when she (or he) observes a run of the secure, unoptimized version
\ls$psi_interim la lb$. As such, the optimizations do not reveal
further information.

\section{Related work}
\label{sec:related}

\Paragraph{Source \mc verification} While the verification of the
underlying crypto protocols has received some attention
\cite{Almeida:2017:FVS:3133956.3134017,cryptoeprint:2014:456},
the verification of correctness and security properties of \mc source
programs has remained largely unexplored, surprisingly so given that
the goal of \mc is to preserve the privacy of secret inputs.
The only previous work that
we know of is Backes et. al. \cite{backes_et_al:LIPIcs:2010:2877} who
devise an applied pi-calculus based abstraction for \mc, and use it
for formal verification. For an auction protocol that computes the
\kw{min} function, their abstraction comprises about 1400 lines of
code. \ourlang, on the other hand, enables direct verification of the
higher-level \mc source programs, and not their models,
and in addition provides a partially verified toolchain.

\Paragraph{Wysteria}
\ourlang's computational model is based on programming
abstractions of a previous domain-specific language,
Wysteria~\citep{wysteria}. \ourlang's realization as an embedded DSL in
\fstar{} makes important advances. In particular, \ourlang (a) enhances the
Wysteria semantics to include a notion of observable traces, and provides
the novel capability to prove security and correctness properties
about mixed-mode \mc source programs, (b) expands the
programming constructs available by drawing on features and libraries
of \fstar, and (c) adds assurance via a (partially) proved-correct
implementation.

\Paragraph{Verified \mc toolchain} Almeida et al.~\cite{Almeida:2017:FVS:3133956.3134017}
build a verified toolchain consisting of (a) a verified
circuit compiler from (a subset of) C to boolean circuits, and
(b) a verified implementation of Yao's~\cite{Yao}
garbled circuits protocol for 2-party \mc.
They use CompCert~\cite{Leroy2009Formal}
for the former, and EasyCrypt~\cite{Barthe:2011:CSP:2033036.2033043}
for the latter. These are significant advances, but there are several distinctions
from our work.
The MPC programs in their toolchain are not \emph{mixed-mode},
and thus it cannot express examples like \ls{median_opt} and the optimized PSI.
Their framework does not enable formal verification of source programs
like \ourlang does. It may be possible to use other frameworks for
verifying C programs (e.g. Frama-C~\cite{framac}), but it is inconvenient
as one has to work in the subset of C that falls in the intersection
of these tools. \ourlang is also more general as it supports
general $n$-party MPC; e.g., the card dealing application in \S\ref{sec:apps}
has 3 parties. Nevertheless, \ourlang may use the
verified Yao implementation for the special case of 2 parties.

\Paragraph{\mc DSLs and DSL extensions} In addition to Wysteria
several other \mc DSLs have been proposed in the
literature~\cite{Huang11,viff,Malka2011,fairplaymp,Holzer12,Nielsen07,Nielsen09,sharemind,Schropfer2011,wysteria,Liu2014,Laud:2015:DLL:2810103.2813664}. Most
of these languages have standalone implementations, and the
(usability/scalability) drawbacks
that come with them. Like \ourlang,
a few are implemented as language extensions. Launchbury et
al.~\citet{Launchbury2012} describe a Haskell-embedded DSL for writing
low-level ``share protocols'' on a multi-server ``SMC machine''.
OblivC~\cite{oblivc} is an extension to C for two-party \mc that
annotates variables and conditionals with an \kw{obliv} qualifier to
identify private inputs; these programs are compiled by
source-to-source translation.
The former is essentially a shallow embedding, and the latter is
compiler-based; \ourlang is unique in that it combines a shallow embedding
to support source program
verification and a deep embedding to support a non-standard
target semantics. Recent work~\cite{ezpc,Buscher:2018:HCH:3243734.3243786} compiles
to cryptographic protocols that include both arithmetic and boolean
circuits; the compiler decides which fragments
of the program fall into which category. It would be interesting work
to integrate such a backend in \ourlang.

\Paragraph{Mechanized metatheory} Our
verification results are different from a typical verification result
that might either mechanize metatheory for
an idealized language~\cite{Aydemir:2005:MMM:2145056.2145062}, or
might prove an interpreter or compiler correct w.r.t. a formal
semantics~\cite{Leroy2009Formal}---we do both. We mechanize the
metatheory of \ourlang establishing the soundness of the conceptual
ST semantics w.r.t. the actual DS semantics, and
mechanize the proof that the interpreter implements
the correct DS semantics.

\Paragraph{General DSL implementation strategies} DSLs (for \mc or
other purposes) are implemented
in various ways, such as by developing a standalone
compiler/interpreter, or by shallow or deep embedding in
a host language. Our approach bears relation
to the approach taken in LINQ~\cite{Meijer:2006:LRO:1142473.1142552},
which embeds a query language in normal C\# programs, and implements
these programs by extracting the query syntax tree and passing it to a
\emph{provider} to implement for a particular backend. Other
researchers have embedded DSLs in verification-oriented host languages
(e.g., Bedrock~\cite{bedrock} in Coq~\cite{coq}) to permit formal
proofs of DSL programs. Low$^\star$~\cite{Protzenko:2017:VLP:3136534.3110261}
is a shallow-embedding of a small, sequential,
well-behaved subset of C in \fstar that extracts to C using a \fstar-to-C
compiler. Low$^\star$ has been used to verify and implement several cryptographic
constructions. Fromherz et al.~\cite{valepopl} present a deep embedding
of a subset of x64 assembly in \fstar that allows efficient verification of
assembly and its interoperation with C code generated from Low$^\star$.
They design (and verify) a custom VC generator for the deeply embedded DSL,
that allows for the proofs of assembly crypto routines to scale.

\section{Conclusions}

This paper has presented \ourlang, the first DSL to enable formal
verification of efficient source \mc programs as written in a
full-featured host programming language, \fstar. The paper presented
examples such as joint median, card dealing, and PSI, and showed
how the DSL enables their correctness and security proofs.
\ourlang implementation, examples, and
proofs are publicly available on
\iflong
Github at \url{https://github.com/FStarLang/FStar/tree/stratified\_last/examples/wysteria}.
\else
Github.
\fi

\bibliographystyle{splncs04}