\section{Appendix}
\label{sec:appA}
\begin{figure}[h]
\begin{lstlisting}[language=C,basicstyle=\scriptsize\ttfamily]
void TFHE_Addition(TFheGateBootstrappingCloudKeySet* x0,
  TFheGateBootstrappingParameterSet* x1){
  TFheGateBootstrappingSecretKeySet* x2 =
    new_random_gate_bootstrapping_secret_keyset(x1);
  x0 = &x2->cloud;
  LweSample* x3 =
    new_gate_bootstrapping_ciphertext_array(64, x2->params);
  for(uint64_t i = 0; i < 64; i ++) {
    bootsSymEncrypt(&x3[i], ((uint64_t) value>>i)&10, x2);
  }
  LweSample* x4 =
    new_gate_bootstrapping_ciphertext_array(64, x2->params);
  for(uint64_t i = 0; i < 64; i ++) {
    bootsSymEncrypt(&x4[i], ((uint64_t) value>>i)&5, x2);
  }
  LweSample* x5 =
    new_gate_bootstrapping_ciphertext_array(64, x2->params);
  fhe_add(x5, a, b, 64, bk);
  printf(
}
\end{lstlisting}
\caption{Generated the TFHE program that perforom a secure addition of two 64-bit integers (10 and 5). For simplicity, the program uses plaintext values as input instead of obtaining them at runtime.}
\label{fig:add-tfhe}
\end{figure}

\begin{figure}[h]
\begin{lstlisting}[language=C,basicstyle=\scriptsize\ttfamily]
/************* Functions **************/
static inline Plaintext num_eval(CryptoContext<Poly> cc,
    const LPPrivateKey<Poly> pk,
	const Ciphertext<Poly> value) {
  Plaintext ret;
  cc->Decrypt(pk, value, &ret);
  return ret;
}
/**************** BGV_Addition ****************/
void BGV_Addition(CryptoContext<Poly> x0){
  LPKeyPair<Poly> x2 = x0->KeyGen();
  x0->EvalMultKeyGen(x2.secretKey);
  cout << num_eval(x0, x2.secretKey,
    x0->EvalAdd(x0->Encrypt(x2.publicKey,
    x0->MakeFractionalPlaintext(10)),
    x0->Encrypt(x2.publicKey, x0->MakeFractionalPlaintext(5))
  )) << endl;
 }
\end{lstlisting}
\caption{Generated the HElib program that perforom a secure addition of two integers (10 and 5). For simplicity, the program uses plaintext values as input instead of obtaining them at runtime.}
\label{fig:add-bgv}
\end{figure}

\begin{figure}[h]
\begin{lstlisting}[language=Python,basicstyle=\scriptsize\ttfamily]
def auction():
  x0 = sint(15) # owned by 2
  x1 = sint(12) # owned by 0
  x2 = sint(20) # owned by 1
  x3 = x1<x2 # owned by 0 1
  x4 = x3 * x1 + (1 - x3) * x2 # owned by 0 1
  x5 = x0<x4 # owned by 0 1 2
  x6 = x5 * x4 + (1 - x5) * x0 # owned by 0 1 2
  x6.reveal_to(0)
  x6.reveal_to(1)
  x6.reveal_to(2) # owned by
  x10 = sint(2) # owned by 2
  x7 = sint(1) # owned by 1
  x8 = sint(0) # owned by 0
  x9 = x3 * x7 + (1 - x3) * x8 # owned by 0 1
  x11 = x5 * x9 + (1 - x5) * x10 # owned by 0 1 2
  x11.reveal_to(0)
  x11.reveal_to(1)
  x11.reveal_to(2)
\end{lstlisting}
\caption{Generate SPDZ program that computes a second-price auction. For simplicity, the program uses plaintext values as input instead of obtaining them at runtime. There are three bids (15, 12 and 20) whose holders are denoted as 0, 1 and 2 respectively.}
\label{fig:spdz-auction}
\end{figure}

\begin{figure}[h]
\begin{lstlisting}[language=Python,basicstyle=\scriptsize\ttfamily,morekeywords={async, await}]
from honeybadgermpc.progs.mixins.share_comparison
  import Equality, LessThan
from honeybadgermpc.preprocessing import
  (PreProcessedElements as FakePreProcessedElements,)
from honeybadgermpc.progs.mixins.share_arithmetic import
  (BeaverMultiply, BeaverMultiplyArrays, MixinConstants, )
import logging
import sys
import asyncio
from time import time
mpc_config = {
  MixinConstants.MultiplyShareArray: BeaverMultiplyArrays(),
  MixinConstants.MultiplyShare: BeaverMultiply(),
  MixinConstants.ShareLessThan: LessThan(),}

async def Auction(x0): # x0: an MPC context
  x2 = x0.ShareFuture()
  x2.ret.set_result(Share(12))
  x3 = x0.ShareFuture()
  x3.ret.set_result(Share(20))
  x4 = x0.ShareFuture()
  x4.ret.set_result(Share(15))
  x5 = (x2 < x3)
  x6 = x5 * x2 + (1 - x5) * x3
  x7 = (x4 < x6)
  print(await (x7 * x6 + (1 - x7) * x4).open())
  print(await (x7 * (x5 * num(x0,1) + (1 - x5) * num(x0,0))
    + (1 - x7) * num(x0,2)).open())

async def _run(peers, n, t, my_id, k):
  from honeybadgermpc.ipc import ProcessProgramRunner
  async with ProcessProgramRunner(
    peers, n, t, my_id, mpc_config) as runner:
    await runner.execute("0", Auction)
    bytes_sent = runner.node_communicator.bytes_sent
    print(f"[my_id] Total bytes sent out: bytes_sent")

if __name__ == "__main__":
  from honeybadgermpc.config import HbmpcConfig
  import sys
  HbmpcConfig.load_config()

  asyncio.set_event_loop(asyncio.new_event_loop())
  loop = asyncio.get_event_loop()
  loop.set_debug(False)
  try:
    pp_elements = FakePreProcessedElements()
    k = 3
    if HbmpcConfig.my_id == 0:
      num_bits = 40
      pp_elements.generate_triples(num_bits * 20 * k,
        HbmpcConfig.N, HbmpcConfig.t)
      pp_elements.generate_share_bits(num_bits * k,
        HbmpcConfig.N, HbmpcConfig.t)
      pp_elements.preprocessing_done()

    else:
      loop.run_until_complete(
        pp_elements.wait_for_preprocessing())

    loop.run_until_complete(
    _run(HbmpcConfig.peers, HbmpcConfig.N,
      HbmpcConfig.t, HbmpcConfig.my_id, k)
    )

  finally:
    loop.close()

\end{lstlisting}
\caption{Generate HoneyBadgerMPC that computes a second-price auction. For simplicity, the program uses plaintext values as input instead of obtaining them at runtime. There are three bids (15, 12 and 20) whose holders are denoted as 0, 1 and 2 respectively. For testing and development, the HoneyBadgerMPC program runs in a single-process simulated network.}
\label{fig:hbmpc-auction}
\end{figure}

\begin{figure}[h]
\begin{lstlisting}[language=C,basicstyle=\scriptsize\ttfamily]
#include <helib/FHE.h>
#include <iostream>
#include <stdlib.h>
#include <stdio.h>
#include <stdint.h>
#include <stdbool.h>
using namespace std;
/************* Functions **************/
static inline NTL::ZZX unum_eval(Ctxt n,
  FHESecKey secretKey) {
  NTL::ZZX ret;
  secretKey.Decrypt(ret, n);
  return ret;
}
static inline Ctxt unum_add(Ctxt n1, Ctxt n2) {
  Ctxt ret = n1;
  ret += n2;
  return ret;
}
static inline Ctxt unum_init(int value,
  const FHEPubKey& publicKey) {
  Ctxt ret(publicKey);
  publicKey.Encrypt(ret, NTL::to_ZZX(value));
  return ret;
}
static inline Ctxt unum_mul_plain(Ctxt n1, int n2) {
  Ctxt ret = n1;
  ret.multByConstant(NTL::to_ZZX(n2));
  return ret;
}
/**************** Multiply ****************/
void multiply(FHEcontext& x0, int x1){
  FHESecKey x2(x0);
  x2.GenSecKey();
  cout  << unum_eval(unum_add(unum_add(
    unum_init(1, x2), unum_mul_plain(unum_init(2, x2), 2)),
    unum_init(3, x2)), x2) <<
    unum_eval(unum_add(unum_add(unum_init(4, x2),
    unum_mul_plain(unum_init(5, x2), 2)),
    unum_init(6, x2)), x2) << endl;
}
/*****************************************
End of C Generated Code
*******************************************/
int main(){
  long m = 0;                   // Specific modulus
  long p = 1021;                // Plaintext base [default=2], should be a prime number
  long r = 1;                   // Lifting [default=1]
  long L = 16;                  // Number of levels in the modulus chain [default=heuristic]
  long c = 3;                   // Number of columns in key-switching matrix [default=2]
  long w = 64;                  // Hamming weight of secret key
  long d = 0;                   // Degree of the field extension [default=1]
  long k = 128;                 // Security parameter [default=80]
  long s = 0;                   // Minimum number of slots [default=0]
  m = FindM(k, L, c, p, d, s, 0);
  FHEcontext context(m, p, r);
  buildModChain(context, L, c);
  NTL::ZZX  G =  context.alMod.getFactorsOverZZ()[0];
  multiply(context, 0);
  return 0;
}

\end{lstlisting}
\caption{Generated HElib program that computes matrix-vector multiplication of \CODE{Array(Array(1, 2, 3), Array(4, 5, 6))} and  \CODE{Array(1, 2, 1)}. For simplicity, the program uses plaintext values as input instead of obtaining them at runtime.}
\label{fig: helib-mul}
\end{figure}

\begin{figure}[h]
\begin{lstlisting}[language=C,basicstyle=\scriptsize\ttfamily]
#include <stdlib.h>
#include <tfhe/tfhe.h>
#include "ir.h"
#include <stdio.h>
#include <stdint.h>
#include <stdbool.h>
static inline LweSample* add(const LweSample* a,
  const LweSample* b, uint64_t size,
  const TFheGateBootstrappingCloudKeySet* bk) {
  LweSample* ret =
    new_gate_bootstrapping_ciphertext_array(size, bk->params);
  fhe_add(ret, a, b, size, bk);
  return ret;
}
static inline LweSample* unum_init(uint64_t value,
  uint64_t size,
  const TFheGateBootstrappingSecretKeySet* bk) {
  LweSample* ret =
    new_gate_bootstrapping_ciphertext_array(size, bk->params);
  for(uint64_t i = 0; i < size; i++) {
    bootsSymEncrypt(&ret[i], ((uint64_t) value>>i)&1, bk);
  }
  return ret;
}
static inline LweSample* unum_mul_plain(const LweSample* a,
  const int b, uint64_t size,
  const TFheGateBootstrappingCloudKeySet* bk) {
  LweSample* c_b =
    new_gate_bootstrapping_ciphertext_array(size, bk->params);
  for(uint64_t i = 0; i < size; i ++) {
    bootsCONSTANT(&c_b[i], ((uint64_t) b>>i)&1, bk);
  }
  LweSample* ret =
    new_gate_bootstrapping_ciphertext_array(size, bk->params);
  fhe_mul(ret, a, c_b, size, bk);
  return ret;
}
static inline uint64_t unum_eval(const LweSample* a,
  uint64_t size,
  const TFheGateBootstrappingSecretKeySet* key) {
  assert(size <= 64);
  uint64_t res[size];
  uint64_t ret = 0;
  for(uint64_t i=0; i<size; i++){
    res[i] = bootsSymDecrypt(&a[i], key)>0;
  }
  for(uint64_t i=0; i<size; i++){
    ret |= ((uint64_t) res[i])<<((uint64_t) i);
  }
  return ret;
}
void multiply(TFheGateBootstrappingCloudKeySet* x0,
  TFheGateBootstrappingParameterSet* x1){
  TFheGateBootstrappingSecretKeySet* x2 =
    new_random_gate_bootstrapping_secret_keyset(x1);
  x0 = &x2->cloud;
  const LweSample** x3 =
    (const LweSample**)malloc(2 * sizeof(const LweSample*));
  LweSample* x4 = add(unum_init(1, 64 ,x2), x3[0], 64 , x0);
  x3[0] = x4;
  LweSample* x5 = add(unum_mul_plain(
    unum_init(2, 64 ,x2), 2, 64, x0), x4, 64 , x0);
  x3[0] = x5;
  LweSample* x6 = add(unum_init(3, 64 ,x2), x5, 64 , x0);
  x3[0] = x6;
  printf(
  x3[1] = add(unum_init(6, 64 ,x2),
    add(unum_mul_plain(unum_init(5, 64 ,x2), 2, 64, x0),
    add(unum_init(4, 64 ,x2), x3[1], 64, x0), 64, x0), 64, x0);
}
int main(){
  const int minimum_lambda = 110;
  TFheGateBootstrappingParameterSet* params =
    new_default_gate_bootstrapping_parameters(minimum_lambda);
  uint32_t seed[] = { 314, 1592, 657 };
  tfhe_random_generator_setSeed(seed,3);
  TFheGateBootstrappingSecretKeySet* s_key =
    new_random_gate_bootstrapping_secret_keyset(params);
  const TFheGateBootstrappingCloudKeySet* c_key = &s_key->cloud;
  multiply(NULL, params);
  return 0;
}
\end{lstlisting}
\caption{Generated TFHE code that computes matrix-vector multiplication of \CODE{Array(Array(1, 2, 3), Array(4, 5, 6))} and  \CODE{Array(1, 2, 1)}. For simplicity, the program uses plaintext values as input instead of obtaining them at runtime.}
\label{fig:tfhe-matrxi-vec}
\end{figure}

\begin{figure}[h]
\begin{lstlisting}[language=C,basicstyle=\scriptsize\ttfamily]
#include <assert.h>
#include <stdlib.h>
#include <tfhe/tfhe.h>
#include "ir.h"
#include <stdio.h>
#include <stdint.h>
#include <stdbool.h>
#include <stdarg.h>
/************* Functions **************/
static inline LweSample* add(const LweSample* a,
  const LweSample* b, uint64_t size,
  const TFheGateBootstrappingCloudKeySet* bk) {
  LweSample* ret =
    new_gate_bootstrapping_ciphertext_array(size, bk->params);
  fhe_add(ret, a, b, size, bk);
  return ret;
}
LweSample* num_array_init(const uint64_t bit_width,
  const TFheGateBootstrappingSecretKeySet* bk,
  const uint64_t size, ...){
  va_list valist;
  va_start(valist, size);
  LweSample* ret =
    new_gate_bootstrapping_ciphertext_array(bit_width * size,
      bk->params);
  for (uint64_t i = 0; i < size ; i ++) {
    uint64_t tmp = va_arg(valist, int);
    for(uint64_t j = 0; j < bit_width; j ++) {
      bootsSymEncrypt(&ret[i * bit_width + j],
        ((uint64_t) tmp>>j)&1, bk);
    }
  }
  va_end(valist);
  return ret;
}
static inline LweSample* num_init(uint64_t value, uint64_t size,
  const TFheGateBootstrappingSecretKeySet* bk) {
  LweSample* ret =
    new_gate_bootstrapping_ciphertext_array(size, bk->params);
  for(uint64_t i = 0; i < size; i ++) {
    bootsSymEncrypt(&ret[i], ((uint64_t) value>>i)&1, bk);
  }
  return ret;
}
static inline LweSample* num_leq(const LweSample* a,
  const LweSample* b, uint64_t size,
  const TFheGateBootstrappingCloudKeySet* bk) {
  LweSample* ret =
    new_gate_bootstrapping_ciphertext(bk->params);
  fhe_compare_signed(ret, a, b, size, bk);
  return ret;
}
static inline LweSample* num_array_index(const LweSample* i,
  const LweSample* arr, uint64_t length, uint64_t bit_width,
    const TFheGateBootstrappingCloudKeySet* bk) {
  LweSample * res =
    new_gate_bootstrapping_ciphertext_array(bit_width, bk->params);
  fhe_array_index(res, i, arr, length, bit_width, bk);
  return res;
}
static inline LweSample* num_less(const LweSample* a,
  const LweSample* b, uint64_t size,
  const TFheGateBootstrappingCloudKeySet* bk) {
  LweSample* ret =
    new_gate_bootstrapping_ciphertext(bk->params);
  LweSample* t1 =
    new_gate_bootstrapping_ciphertext_array(size, bk->params);
  LweSample* t2 =
    new_gate_bootstrapping_ciphertext_array(size, bk->params);
  fhe_neg(t1, b, size, bk);
  fhe_add(t2, a, t1, size, bk);
  bootsCOPY(ret, &t2[size-1], bk);
  return ret;
}
static inline LweSample* bit_and(const LweSample* a,
  const LweSample* b,
  const TFheGateBootstrappingCloudKeySet* bk) {
  LweSample* ret = new_gate_bootstrapping_ciphertext(bk->params);
  bootsAND(ret, a, b, bk);
  return ret;
}
\end{lstlisting}
\caption{Generated TFHE program that merge sort an array of [3, 1, 5, 2]. For simplicity, the program uses plaintext values as input instead of obtaining them at runtime. (part 1)}
\label{fig:tfhe-merge1}
\end{figure}
\begin{figure}[h]
\begin{lstlisting}[language=C,basicstyle=\scriptsize\ttfamily]
static inline LweSample* num_mux(const LweSample* a,
  const LweSample* b, const LweSample* c, uint64_t size,
  const TFheGateBootstrappingCloudKeySet* bk) {
  LweSample* ret =
    new_gate_bootstrapping_ciphertext_array(size,
    bk->params);
  fhe_mux(ret, a, b, c, size, bk);
  return ret;
}

static inline int64_t num_eval(const LweSample* a,
  uint64_t size,
  const TFheGateBootstrappingSecretKeySet* key) {
  assert(size <= 64);
  uint64_t res[size];
  int64_t ret = 0;
  for(uint64_t i=0; i<size; i++){
    res[i] = bootsSymDecrypt(&a[i], key)>0;
  }
  if(res[size-1]!=0){
    for(uint64_t i=0; i<size; i++){
      res[i] = 1 - res[i];
      ret |= ((uint64_t) res[i]<<((uint64_t) i));
    }
    ret = -(ret + 1);
  }
  else{
    for(uint64_t i=0; i<size; i++){
      ret |= ((uint64_t) res[i]<<((uint64_t) i));
    }
  }
  return ret;
}
/**************** MergeSort ****************/
void MergeSort(TFheGateBootstrappingCloudKeySet* x0,
  TFheGateBootstrappingParameterSet* x1){
  TFheGateBootstrappingSecretKeySet* x2 =
    new_random_gate_bootstrapping_secret_keyset(x1);
  x0 = &x2->cloud;
  LweSample* x3 = num_array_init(16, x2, 2, 5 ,8);
  LweSample* x4 = num_array_init(16, x2, 2, 2 ,4);
  LweSample* x5 = num_init(0, 16, x2);
  LweSample* x6 = num_init(0, 16, x2);
  LweSample* x7 = num_leq(
    num_array_index(x5, x3, 2, 16, x0),
    num_array_index(x6, x4, 2, 16, x0), 16 , x0);
  const LweSample* x8 =
    num_less(x5, num_init(2, 16 ,x2), 16 , x0);
  const LweSample* x9 =
    num_less(x6, num_init(2, 16 ,x2), 16 , x0);
  LweSample* x10 = bit_and(x8, x9, x0);
  LweSample* x11 = num_mux(num_mux(add(x5,
    num_init(1, 16 ,x2), 16, x0), x5, x7, 16 , x0),
    num_mux(add(x5, num_init(1, 16 ,x2), 16, x0),
      x5, x8, 16 , x0), x10, 16 , x0);
  LweSample* x12 = num_mux(num_mux(x6, add(x6,
    num_init(1, 16 ,x2), 16, x0), x7, 16 , x0),
    num_mux(add(x6, num_init(1, 16 ,x2), 16, x0),
      x6, x9, 16 , x0), x10, 16 , x0);
  LweSample* x13 = num_leq(
    num_array_index(x11, x3, 2, 16, x0),
    num_array_index(x12, x4, 2, 16, x0), 16 , x0);
  const LweSample* x14 =
    num_less(x11, num_init(2, 16 ,x2), 16 , x0);
  const LweSample* x15 =
    num_less(x12, num_init(2, 16 ,x2), 16 , x0);
  LweSample* x16 = bit_and(x14, x15, x0);
  LweSample* x17 = num_mux(num_mux(
    add(x11, num_init(1, 16 ,x2), 16, x0),
    x11, x13, 16 , x0), num_mux(
    add(x11, num_init(1, 16 ,x2),
    16, x0), x11, x14, 16 , x0), x16, 16 , x0);
  LweSample* x18 =
    num_mux(num_mux(x12,
    add(x12, num_init(1, 16 ,x2), 16, x0),
    x13, 16 , x0), num_mux(add(x12, num_init(1, 16 ,x2),
    16, x0), x12, x15, 16 , x0), x16, 16 , x0);
  LweSample* x19 =
    num_leq(num_array_index(x17, x3, 2, 16, x0),
    num_array_index(x18, x4, 2, 16, x0), 16 , x0);
  const LweSample* x20 =
    num_less(x17, num_init(2, 16 ,x2), 16 , x0);
\end{lstlisting}
\caption{Generated TFHE program that merge sort an array of [3, 1, 5, 2]. For simplicity, the program uses plaintext values as input instead of obtaining them at runtime. (part 2)}
\label{fig:tfhe-merge2}
\end{figure}
\begin{figure}[h]
\begin{lstlisting}[language=C,basicstyle=\scriptsize\ttfamily]
const LweSample* x21 =
  num_less(x18, num_init(2, 16 ,x2), 16 , x0);
LweSample* x22 = bit_and(x20, x21, x0);
LweSample* x23 = num_mux(num_mux(add(x17,
  num_init(1, 16 ,x2), 16, x0), x17, x19, 16 , x0),
  num_mux(add(x17, num_init(1, 16 ,x2),
  16, x0), x17, x20, 16 , x0), x22, 16 , x0);
LweSample* x24 = num_mux(num_mux(x18,
  add(x18, num_init(1, 16 ,x2), 16, x0), x19, 16 , x0),
  num_mux(add(x18, num_init(1, 16 ,x2), 16, x0),
  x18, x21, 16 , x0), x22, 16 , x0);
const LweSample* x25 =
  num_less(x23, num_init(2, 16 ,x2), 16 , x0);
printf(
  num_array_index(x5, x3, 2, 16, x0),
  num_array_index(x6, x4, 2, 16, x0), x7, 16 , x0),
  num_mux(num_array_index(x5, x3, 2, 16, x0),
  num_array_index(x6, x4, 2, 16, x0), x8, 16 , x0),
  x10, 16 , x0), 16, x2));
printf(
  num_array_index(x11, x3, 2, 16, x0),
  num_array_index(x12, x4, 2, 16, x0), x13, 16 , x0),
  num_mux(num_array_index(x11, x3, 2, 16, x0),
  num_array_index(x12, x4, 2, 16, x0), x14, 16 , x0),
  x16, 16 , x0), 16, x2));
printf(
  num_array_index(x17, x3, 2, 16, x0),
  num_array_index(x18, x4, 2, 16, x0), x19, 16 , x0),
  num_mux(num_array_index(x17, x3, 2, 16, x0),
  num_array_index(x18, x4, 2, 16, x0), x20, 16 , x0),
  x22, 16 , x0), 16, x2));
printf(
  num_array_index(x23, x3, 2, 16, x0),
  num_array_index(x24, x4, 2, 16, x0),
  num_leq(num_array_index(x23, x3, 2, 16, x0),
  num_array_index(x24, x4, 2, 16, x0), 16 , x0), 16 , x0),
  num_mux(num_array_index(x23, x3, 2, 16, x0),
  num_array_index(x24, x4, 2, 16, x0), x25, 16 , x0),
  bit_and(x25, num_less(x24, num_init(2, 16 ,x2), 16 , x0),
  x0), 16 , x0), 16, x2));
}
int main(){
  const int minimum_lambda = 110;
  TFheGateBootstrappingParameterSet* params =
    new_default_gate_bootstrapping_parameters(minimum_lambda);
  uint32_t seed[] = { 314, 1592, 657 };
  tfhe_random_generator_setSeed(seed,3);
  TFheGateBootstrappingSecretKeySet* s_key =
    new_random_gate_bootstrapping_secret_keyset(params);
  const TFheGateBootstrappingCloudKeySet* c_key = &s_key->cloud;
  MergeSort(NULL, params);
  return 0;
}

\end{lstlisting}
\caption{Generated TFHE program that merge sort an array of [3, 1, 5, 2]. For simplicity, the program uses plaintext values as input instead of obtaining them at runtime. (part 3)}
\label{fig:tfhe-merge3}
\end{figure}
\section{Motivating Example and Background}
\label{sec:bkg}
\vspace{-1ex}
As an example of secure MPC, consider online auctions.
Online auctions have great practical importance and different models are widely used by eBay, Google AdWords and Facebook.
In general, a secure online auction works as follows.
Buyers place their sealed bids on items and the highest bidder is chosen to buy the item.
In this setup, parties are not permitted to know others' bids, unlike in an English auction where the auctioneer starts with a minimum price and buyers openly shout out their bids.
Hence, conducting successful secret auctions in the absence of a trusted authority requires cryptographic techniques to preserve the secrecy of bids while performing necessary computations such as finding the highest bidder.
One of the significant use cases of secure auctions is procurement via a competitive bidding process, where no participant trusts each other, including the auctioneer.
While a trusted third party handling the auction may be acceptable when the items under auction have low value, this is generally a less desirable option in high-value and corruption-prone environments such as procurement for public construction contracts.

There are many different types of auction policies studied by economists and game theorists.
An auction where the highest bidder is chosen to buy the item by paying the highest bid is known as a {\em first-price} auction.
A second-price or Vickrey auction~\cite{vickrey61} is a well-known auction policy where the highest bidder is chosen to buy the item by paying the {\em second} highest price.
Second-price auctions provide buyers with the incentive to bid their true valuation and does not allow for price discovery (\textit{i.e.}, no ramping up prices).
Hence, second-price auctions are especially suitable for high-value low-trust environments such as public procurements.
Second-price auctions also apply to settings where multiple items are auctioned and bids may have additional structure, such as if/then conditions, that need to be taken into account for comparison. Such settings are described as generalized second-price auctions.
Given that secrecy of the bids is preserved, the computations required when a single item is auctioned are simpler than when multiple items are auctioned.
Hence it is desirable both from programmability and efficiency viewpoints that the online auction application is written once for the general case and gets automatically and correctly specialized for the desired number of items, number of bidders, comparison logic, etc. We will discuss an implementation in our HACCLE toolchain in more detail in Section~\ref{sec:auctions}.

To continue with necessary background on cryptography, we first take a look at \emph{Secret Sharing} -- a cryptographic technique that allows to perform computations on secret data.

\paragraph{Secret sharing}
Secret sharing~\cite{secrectshare79} is a cryptographic technique that distributes a piece of secret data amongst a group of parties and allows the secret to be reconstructed only when a sufficient portion of shares are combined.
A $(t, n)$-secret sharing allows the secret $s$ to be split into $n$ shares.
Any $t-1$ of the shares reveal no information about $s$, while any $t$ shares allow complete reconstruction of the secret $s$.

The SPDZ~\cite{SPDZ} and HoneyBadgerMPC~\cite{lu2019honeybadgermpc} frameworks serve as our secret sharing backends and provide Python-style programming environments for writing custom MPC programs.
These frameworks let developers express MPC programs (\textit{e.g.}, second-price auction) as arithmetic expressions.
Constructing the most efficient MPC programs is the major challenge faced by developers.
First, developers constantly think about the depth of the overall circuit results from their arithmetic expressions (\textit{e.g.}, performing a linear reduction over a list of elements can be realized as a balanced tree reduction with smaller depth).
Second, developers must have a good understanding of the cost of every primitive operation (\textit{e.g.}, logically similar usage of different comparison operators may yield different costs).
Challenges faced here are significantly different from writing an efficient program in the traditional setting and can be successfully overcome by a compiler.

\paragraph{Homomorphic Encryption}
Cloud computing is a scenario where one's privacy may be violated.
In this scenario, one party wants to perform computations by outsourcing to another (possibly untrusted) party, \textit{e.g.}, training machine learning models on private data on a public cloud server.
This can be achieved by homomorphic encryption, another important cryptographic primitive.
{\em Homomorphic encryption} enables operations on encrypted data without access to the secret key.
The existing fully homomorphic encryption (FHE) schemes are lattice-based constructions, and their security mainly relies on hardness assumptions of Learning With Error (LWE) problems.
PALISADE~\cite{palisade}, TFHE~\cite{TFHE}, and HElib~\cite{Helib} serve as our FHE backends.
They all implement asymmetric protocols that use a pair of public and private keys for encryption and decryption.
TFHE implements a very fast gate-by-gate bootstrapping mechanism~\cite{chillotti2016faster, chillotti2017faster}.
The TFHE library allows to evaluate an arbitrary Boolean circuit composed of binary gates, over encrypted data, without revealing any information.
HElib implements the Brakerski-Gentry-Vaikuntanathan (BGV) scheme \cite{bgv}, along with many optimizations to make homomorphic evaluation run faster, focusing mostly on effective use of the Smart-Vercauteren cipher text packing techniques~\cite{cryptoeprint:2011:133} and the Gentry-Halevi-Smart optimizations \cite{cryptoeprint:2012:099}.
The PALISADE library supports the BGV, BFV, and CKKS schemes and a more secure variant of the TFHE scheme, including bootstrapping. In cryptography, ciphertext and plaintext mean private information and public information respectively. In this paper, we may use those terms interchangeably.

\paragraph{Garbled Circuits}
Yao's Garbled circuits \cite{yao1982protocols} is a two-party secure computation scheme for Boolean circuits against semi-honest adversaries.
The main idea is that for each of the Boolean gates, one party (the circuit generator) generates a list of keys corresponding to all possible outputs, each encrypted by two keys corresponding to the two inputs that generates that output.
This way, when the other party (the evaluator) reaches the gate, the evaluator should have two keys corresponding to the values of the two inputs, which means the evaluator will be able to correctly decrypt one of the values, and be able to continue on to the next gate.
Obliv-C \cite{oblivC} is the library that we use to support Yao's Garbled Circuits protocols.

\paragraph{System Model and Communication Model}
There are two popular system models for multi-party computation.
The MPC-as-a-service setting allows some parties to play the role of servers and provide MPC services to clients with private input.
The other setting is where the parties running the MPC protocols are the participants who provide the input.
The HACCLE toolchain does not force users to pick one specific setting; instead, the user should pick the proper setting and keep that setting in mind when developing programs.
Similarly, the HACCLE toolchain does not enforce any communication model.
The parties/machines could be fully connected, could form a star network structure, or could be any specified structure.
As long as the network structure is supported by one of HACCLE's backends, HACCLE should be able to compile the programs.

\paragraph{Adversary Models}
Moreover, building MPC applications requires one to understand the security assumptions of an MPC library, \textit{e.g.}, the adversary models.
There are two major adversary models: semi-honest and malicious. A {\em semi-honest} adversary follows the protocol, but tries to learn as much as possible from the messages they receive from other parties.
A {\em malicious} adversary has the same powers of a semi-honest one in analyzing the protocol execution.
In addition to that, it may also control, manipulate, or arbitrarily inject messages to the network.
In HACCLE, programmers are only required to provide a model of choice and the toolchain will pick proper sub-protocols to build up the MPC programs satisfying the adversary model described.

\paragraph{Offline Phase}
The offline/online paradigm is applied by many MPC protocols and frameworks, where the online phase makes use of a buffer of preprocessed input-independent values that are created during the offline phase.
Due to the fact that these values are independent of the input of the program, the MPC framework can run the offline phase to prepare them before the online program begins.
The online phase is then the actual phase where clients/users provide their input and get expected output; this online phase can gain a significant speed-up with the help of the offline phase.
A number of preprocessing values are required for doing multiplication and comparison.
For example, each multiplication between secret shares consumes one random "Beaver's triple", and each comparison would costs some triples and random shared bits.  The volume of preprocessing data depends on the online phase, and, as such, it would be hard for programmers with no security expertise to work out those requirements.
In HACCLE, the programmer need not care about those secret parameters, but rather only describes the function computed by the program and the intended private information, and the HACCLE toolchain will parse the program and work out the proper settings for the offline phase.
\section{Conclusion}
\label{sec:conclusion}
\vspace{-2ex}

Secure MPC-based applications play crucial role in solving many important practical problems such as high-valued procurements.
But building performant MPC-based applications from scratch is a notoriously difficult task as it requires expertise ranging from cryptography to circuit optimization.
Therefore software developers need an ecosystem for building MPC-based applications.
As a solution to this problem, we have introduced the HACCLE toolchain, a multi-stage compiler for optimized circuit generation.
We believe that the HACCLE toolchain offers a compelling approach to the design and implementation of secure MPC-based applications.

\section{Evaluation}
\label{sec:evaluation}
\vspace{-1ex}
We have implemented our HACCLE framework in Scala.
To assess our framework, we present three experiments. The first focuses on Harpoon and HIR programming languages; the second focuses on the optimization of scalar multiplications; the third focuses on our support of indexing to arrays at secret indices.
For simplicity, the test program uses plaintext values instead of obtaining them at runtime. We conducted our experiments on a single Ubuntu 18.04 LTS machine of 16 GB RAM with 8 Intel Core i7 Processors.
\subsection{Case Study 1: Secure Auctions}
\label{sec:auctions}
\vspace{-0.1em}
Recall the discussion of the practical importance of secure auctions in \secref{sec:bkg}.
In this experiment, we implement a second-price auction that is designed to give bidders confidence to bid their best price without overpaying. In a second-price auction, bidders submit sealed bids. The bidder who submits the highest bid is awarded the object and pays the amount of the second-highest bid.

\figref{fig:2price-harpoon} and \figref{fig:2price-hir} show the code snippets written in Harpoon and HIR respectively, where the elements in array \CODE{bidders} denote bidder's identities, and the elements in array \CODE{bid} denote their bids.
The implementation uses four variables (\CODE{fst}, \CODE{snd}, \CODE{ifst} and \CODE{isnd}) to store the values of the first and second highest bids and their holders respectively.
As you can see from \figref{fig:2price-harpoon}, writing the Harpoon implementation does not need developers to have security concerns, or to have the mindset of building circuits.
Programmers can program functionally or imperatively, thanks to the expressivity of Scala.
The HIR implementation in \figref{fig:2price-hir} may look more tedious but exposes some nature of building secure computations (circuits). For example, the use of those if-constructs reminds advanced users that they are using selectors.
This allows advanced users to experiment with advanced optimizations that may not be achieved by automatic program transformations.

As a key example, observe that the linear sequence of operations in Figures \ref{fig:2price-harpoon} and \ref{fig:2price-hir} will result in a suboptimal circuit. However, rewriting the HIR code in \figref{fig:2price-hir} in a functional style as \texttt{(bids zip bidders).map(..).reduce(..)} allows us to abstract over the reduction pattern and substitute the linear sequence with a tree reduction pattern that yields a circuit of logarithmic depth that allows efficient parallel computation. Using known techniques for extracting functional dependencies from imperative loops~\cite{rompf2017functional,essertel2019precise}, this transformation could be automated and applied automatically to for loops in Harpoon.

\figref{fig:spdz-auction} and \figref{fig:hbmpc-auction} show the generated SPDZ and HoneyBadgerMPC program respectively.
As the loops are unrolled during code generation, we only show the generated program for 3 bidders. For simplicity, the program uses plaintext values as input instead of obtaining them at runtime.  For testing and development, the HoneyBadgerMPC program runs in a single-process simulated network. It contains lines of code dealing with network connections and synchronizations. Those are concerns that Harpoon and HIR developers do not have to worry about.

\begin{figure}[t]
  \centering
  \begin{lstlisting}[basicstyle={\scriptsize\ttfamily}]
    var ifst = bidders(0)
    var isnd = bidders(0)
    var fst = bids(0)
    var snd = bids(0)
    if (bids(0) < bids(1)) {
      ifst = bidders(1)
      fst = bids(1)
    } else {
      isnd = bidders(1)
      snd = bids(1)
    }

    for (i <- 2 until bids.length) {
      if (fst < bids(i)) {
        isnd = ifst
        snd = fst
        ifst = bidders(i)
        fst = bids(i)
      } else if (snd < bids(i)) {
        isnd = bidders(i)
        snd = bids(i)
      }
    }
    (ifst, snd)
  \end{lstlisting}
  \vspace{-.5em}
  \caption{Harpoon code snippet performing a second-price auction, where \CODE{bidders} and \CODE{bids} are stored in an array of private values.}
  \label{fig:2price-harpoon}
  \vspace{-1.5em}
\end{figure}
\begin{figure}[t]
  \centering
  \begin{lstlisting}[basicstyle={\scriptsize\ttfamily}]
    var ifst = bidders(0)
    var isnd = bidders(0)
    var fst = bids(0)
    var snd = bids(0)
    val b = bids(0) < bids(1)
    ifst = if (b) bidder(1) else ifst
    fst = if (b) bids(1) else fst
    isnd = if (b) isnd else bidders(1)
    snd = if (b) snd else bids(1)

    for(i <- 2 until bids.length){
      val b0 = fst < bids(i)
      val b1 = snd < bids(i)
      isnd = if (b0) ifst else if (b1) bidders(i) else isnd
      snd = if (b0) fst else if (b1) bids(i) else snd
      ifst = if (b0) bidders(i) else ifst
      fst = if (b0) bids(i) else fst
    }
    (ist, snd)
  \end{lstlisting}
  \vspace{-.5em}
  \caption{HIR code snippet performing a second-price auction, where \CODE{bidders} and \CODE{bids} are stored in an array of private values.}
  \label{fig:2price-hir}
  \vspace{-1.5em}
\end{figure}

\subsection{Case Study 2: Matrix-Vector Product}
\vspace{-0.1em}
This experiment performs a set of secure matrix-vector multiplication, where one party (the client) has an input matrix, and the other party (the server) has a vector. \figref{fig:mat-vec-test} shows our test program that randomly generates a $10 * N$ matrix (where $N$ is range from 100 to 500), and multiplies with a fixed vector $[1, 399, 1, 413, 1, 587, 1, 354, 1, 444]$. The goal is to show the effectiveness of our optimization discussed in \secref{sec:privat-mutl}.
\begin{figure}[t]
    \centering
    \begin{lstlisting}[basicstyle={\footnotesize\ttfamily}]
val rand = new scala.util.Random
val start = 1000
@sec(alice) val m = Array.fill(N)(
Array.fill(10)(start + rand.nextInt(start + 1)))
val v = Array(1, 399, 1, 413, 1, 587, 1, 354, 1, 444)
m * v
    \end{lstlisting}
    \vspace{-1ex}
    \caption{Test of Matrix-Vector Multiplications}
    \label{fig:mat-vec-test}
    \vspace{-2ex}
\end{figure}
The HElib library serves as our testing backend that implements the BGV homomorphic encryption scheme and effectively uses the Smart-Vercauteren cipher text packing techniques~\cite{Helib}.
\tbref{tb:matrix-vec} compares the running time of the generated HElib programs with and without optimizations.
As $N$ increases from 100 to 500, the speedup become more observable.

\begin{table}
  \centering
  \begin{tabular}{ | l | l | l | l | l | l | }
  \hline
  N & 100 & 200 & 300 & 400 & 500 \\
  \hline
  before & 7.64s & 20.69s & 57.79s & 140s & 296s \\
  \hline
  after & 6.48s & 15.21s & 35.83s & 82s & 164s \\
  \hline
  \end{tabular}
  \caption{Execution time of the HElib programs that perform multiplications of a matrix of $10 * N$ and a vector $[1, 399, 1, 413, 1, 587, 1, 354, 1, 444]$ before and after the optimization.}
  \label{tb:matrix-vec}
\end{table}

As our compiler unrolls all the loops, the size of the generated code is not small.
\figref{fig: helib-mul} shows the generated HElib program that computes computes matrix-vector multiplication of \CODE{Array(Array(1, 2, 3), Array(4, 5, 6))} and  \CODE{Array(1, 2, 1)}.

\subsection{Case Study 3: Merge Sort}
This experiment implements MergeSort in HIR. It is interesting as the implementation involves array indexing and conditional executions, and an array lookup on a private index is not supported by most languages \cite{hastings2019sok}.
The implementation is written in HIR, not in Harpoon, as HIR exposes the language features needed in writing secure computations.

MergeSort is a divide and conquer algorithm. It recursively divides an input array into two halves and then merges the two sorted halves. Our implementation is shown in \figref{fig:merge-sort-hir}.
In the function \CODE{mergesort}, the variable \CODE{r} (at line 31) stores a recursion object initialized with the bound 10. The expression \CODE{r.rec} (at line 32) is the construct for defining a bounded recursive function call. This allows one to explicitly specify the bound of the defining recursive function. The \CODE{NumArray} is the type for arrays that allow private indexing. The two parameters \CODE{i} and \CODE{j} are plaintext, which is important for unrolling the recursive function at compile time.
The function \CODE{slice(i, j)} returns a subarray from the \CODE{i}th element until the \CODE{j}th element, where \CODE{i} and \CODE{j} are plaintext integers. The if-statement at lines 35 to 40 is the standard one as its condition depends on a plain text value.
The function \CODE{merge} is used for merging two halves.
All the if-constructs appearing in this function are oblivious as their conditions depend on cipher text values. The loop at line 12 is bounded as the length of an array is known at compile time.
\figref{fig:tfhe-merge1}, \figref{fig:tfhe-merge2} and \figref{fig:tfhe-merge3} show the generated TFHE program, where loops and recursions are all unrolled.
\begin{figure}[t]
\begin{lstlisting}[numbers=left,basicstyle={\scriptsize\ttfamily}]
val o1 = Owner()
// input
var = NumArray(o1, 3, 1, 5, 2)
val s = 0
val e = arr.length
// merge
def merge(o: Owner, arr1: NumArray, arr2: NumArray) = {
  var res = NewNumArray(o, arr1.length + arr2.length)
  var i = Num(o, 0)
  var j = Num(o, 0)
  var k = 0
  while (k < res.length) {
    val b1 = i < Num(o, arr1.length)
    val b2 = j < Num(o, arr2.length)
    val p = if (b1.not) arr2(j) else if (b2.not) arr1(i)
      else if (arr1(i) <= arr2(j)) arr1(i) else arr2(j)
   res = res.update(k, p)
   // updating arr1 index
   i = if (b1.not) i else if (b2.not) i + Num(o, 1) else
       if (p == arr1(i)) i + Num(o, 1) else i

  // updating arr2 index
  j = if (b1.not) j + Num(o, 1) else if (b2.not) j
      else if (p == arr2(j)) j + Num(o, 1) else j

   k = k + 1
  }
  res
}
val r = recFuel(10)
val mergesort = r.rec[NumArray, Owner, Int, Int] {
  f => (a, o, i, j) => {
   val mid = (j - i) / 2
   if (mid == 0 || i >= j){ a }
   else {
     val left = a.slice(i, mid)
     val right = a.slice(mid, j)
     merge(o, f(left, o, 0, left.length),
              f(right, o, 0, right.length))
    }
   }
}
val res = mergesort(arr, o1, s, e)
output(res.eval(o1))
\end{lstlisting}
\caption{MergeSort implemented in HIR}
\label{fig:merge-sort-hir}
\vspace{-2ex}
\end{figure}

\section{Compiler}
\label{sec:haccle}
\vspace{-1ex}
HACCLE toolchain uses \emph{lightweight modular staging} (LMS) to support our towers of abstractions. Staging is a technique for building extensible, flexible DSLs by providing \emph{code generators} that successively lower higher-level abstractions to lower-level abstractions, and, ultimately, to executable code. Importantly, staging allows optimization to be performed at every level of the lowering process.
Hence, some optimizations can be performed at high levels of abstraction (\textit{e.g.}, optimization on plaintext computations (\secref{sec:optimization}), while other optimizations can be performed at lower levels of abstraction.
As a result, abstraction penalties are minimized. Another benefit to staging is that because the translation is written in terms of generators, it is simple to add new abstractions at any given level.

\subsection{Staged Compilation}\label{sec:staging}
\vspace{-1ex}
Multi-Stage Programming (or staging) is the programming language technique that executes programs
in multiple stages. In Lightweight Modular Staging (LMS), higher order type (Rep[T]) labels
the program fragments of the next stage. In the current stage, all Rep-typed variables (and
computations) form computation graphs (\textit{i.e.}, LMS IR). Staging is similar to and more general than the
construction of TensorFlow computation graphs using TensorFlow APIs, since it is designed to
handle more programming language constructs such as functions and closures.
The key benefit of staging is that the present-stage code can be written in a high-level style,
yet generates future-stage code that is very low-level and efficient.
\figref{fig:compilation} illustrates an end-to-end compilation path in HACCLE. The compiler takes a Scala program with Harpoon annotations, constructs a computation graph that expresses an abstract circuit. Given a backend specification, the compiler will generate a target program for it. Currently, our compiler is not able to automatically choose an appropriate backend and initialize all the parameters that are needed for it. Thus, a backend specification is needed. It is a file that contains a set of parameters that are needed for translating an abstract circuit to a concrete backend program. For testing and development, we currently hard-coded those information in the program. There are no technique difficulties to read the information from a file.

\begin{figure}[ht]
  \centering
\includegraphics[scale=.33]{figures/compilation.pdf}
\caption{Compilation in HACCLE}
\label{fig:compilation}
\end{figure}
\paragraph{Generative Programming and Lightweight Modular Staging (LMS)}
As mentioned previously, the HACCLE compiler uses LMS for code generation due to its multi-staging capabilities. In LMS, a special type constructor \CODE{Rep[T]} is used to denote a \emph{staged} expression, which will cause an expression of type \CODE{T} to become part of the generated program. For example, the expression \CODE{Rep[SNum]} denotes an encrypted integer. Given two \CODE{Rep[SNum]} values \CODE{a} and \CODE{b}, \emph{evaluating} the expression \CODE{a + b} will \emph{generate} code for a given backend. For the Helib backend, the generated code will be \CODE{Ctxt r = a; r += b;}, where \CODE{Ctxt} is the type of a cipher text in the Helib library. For the TFHE backend, the generated code will be:
\vspace{-.5ex}
\begin{lstlisting}[language=C,basicstyle={\footnotesize\ttfamily}]
LweSample* x5 =
new_gate_bootstrapping_ciphertext_array(64, x2->params);
fhe_add(x5, a, b, 64, bk);
\end{lstlisting}
\vspace{-.5ex}
where \CODE{LweSample} is the type of a cipher text in the TFHE library. As a TFHE program denotes a Boolean circuit, it does not provide arithmetic expressions and operations. The compiler expresses an integer as a bit-array of size 64. The function \CODE{fhe}\_\CODE{add} is part of our HACCLE library of the TFHE library.

\subsection{Harpoon}
\label{sec:harpoon}
HAccle Rich Representation for Program OperatiON (Harpoon) language is an expressive subset of Scala for writing MPC programs. It is an imperative and monomorphic language, featuring standard control flow operations: loops,
function calls, conditionals, and recursion. The language is designed to be expressive enough that programmers could easily write Harpoon code directly, while being constrained enough to ensure that Harpoon programs can be implemented via translation to secure low-level computations. In practice, Harpoon serves as the top-level IR for the HACCLE pipeline, and is the language for end-user programs.

Harpoon language is not only able to access all the Scala libraries, but also provides a set of cryptographic data structures. For example, \CODE{HArray[T]} is an encrypted array that allows one to index on cipher texts. It also provides a set of security annotations that are forms of syntactic metadata added to the Scala source code. Annotations are read via reflection and are used to direct code generation.
They are agnostic to the target backend, and are used by subsequent stages of the HACCLE pipeline.

For example, the annotation \CODE{sec} is used to mark the provider (also the owner) of the private data.
Recursive functions and loops may be annotated with an expression, placing an upper bound on the number of recursive calls and iterations. This expression can reference the parameters of the function, allowing this bound to vary according to the context in which a function is called.  As an example, consider the signature of \CODE{merge} function:
\begin{lstlisting}
@bound(a.length + b.length)
def merge(a: HArray[Int], b: HArray[Int]): Harray[Int]
\end{lstlisting}
The upper bound on the number of recursive calls is the sum of the length of the two input arrays. Note that the semantics of function calls in Harpoon is not impacted by this bound; rather it is used by subsequent stages of the pipeline to bound the invocation of a recursive function call. See \secref{sec:obliv} for details.

The annotated program is also equipped with a type system which ensures that information about private data cannot be leaked; this provides the first-layer guarantees that the programs can be successfully compiled by the later stages of the pipeline. Consider the statement \CODE{println(a)}, where $a$ is annotated as private data. The compiler will report a type error, as encrypted data is not understandable or meaningful to users. But the assignment \CODE{@sec(alice) val r = a} will not cause a type error, because the annotation indicates that the variable \CODE{r} stores encrypted data.
While the type system at this stage does not make use of fine-grained ownership information, this information will be passed down through the pipeline.

\subsection{Intermediate Representation}
HACCLE intermediate representation (HIR) serves as an interface between high-level programming language and cryptographic backends.
HIR is a domain-specific intermediate language, and gains benefits from LMS to support towers of abstractions. It encompasses all the primitive operations which we have supported so far, e.g., encryption, decryption, sharing, and combining.

\paragraph{Multi-level IR}
Different backends may support different sets of operations in HIR---no backend is ``complete'' in that there is a direct implementation of each HIR operation in that backend. For example, the TFHE backend provides a complete set of logical operations, but does not support arithmetic operations. In contrast, other backends may support arithmetic operations but not Boolean operations. The compiler's job is to {\em rewrite} HIR circuits to be compatible with backends.

As shown in \figref{fig:hir-nodes}, HIR is a multi-level IR. The compiler can thus use rewrites to target the subset of operations that a given backend supports. For example, arithmetic operations (adds, multiplies) can be rewritten into bit-level implementations (as, e.g., ripple-carry adders, or bit-level implementations), or Boolean operations can be represented as arithmetic operations that happen to operate over $\mathbb{Z}_2$. We are developing a set of these rewrite rules for our various backends (and, indeed, rely on exactly this type of rewrite to support floating point operations).

A key task for integrating a new backend is identifying what set of HIR operations that module supports, hence directing the compiler to perform appropriate rewrites. Notably, if the compiler {\em cannot} rewrite an HIR circuit to target the set of operations a backend supports, this will manifest as a type error, providing feedback to the user.
\begin{figure}[ht]
\centering
\small
\begin{minipage}{0.45 \textwidth}
\begin{tikzpicture}[squarednode/.style={rectangle, draw=blue!60, very thick, minimum size=3mm},squarednode1/.style={rectangle, draw=blue!60, very thick, minimum size=3mm, text centered, text width=2.5cm},]
 \node[squarednode] at (-4, 0) {\small Float, FloatArray};
 \node[squarednode] at (-4, -1) {\small UNum, UNumArray};
 \node[squarednode] at (-1, -1) {\small Num, NumArray};
 \node[squarednode] at (-2, -2) {\small Bit, BitArray};
 \draw[thick, ->](-4, -0.3) -- (-4, -0.7);
 \draw[thick, ->](-4, -1.3) -- (-2, -1.7);
 \draw[thick, ->](-1, -1.3) -- (-2, -1.7);
\end{tikzpicture}
\end{minipage}
\caption{Example of multi-level HIRs}
\label{fig:hir-nodes}
\end{figure}

For example, in the scenario of using a FHE scheme, an integer is represented by a \CODE{Num} node in HIR shown below, where the field \CODE{provider} is an abstraction of the party who provides the value, and the field \CODE{value} is an abstraction of the encrypted value.
\begin{lstlisting}
case class Num(
  val provider: Set[Rep[SOwner]], // who provides it
  val value: Rep[SNum] // encrypted value
)
\end{lstlisting}
In this case, a variable declaration statement in Harpoon, i.e., \CODE{@sec(alic) val x = 5;}, is transformed to \CODE{val o = new Owner(alice);  val x = Num(o, 5);} in HIR.

In the scenario of using a secret sharing scheme, an integer is represented by a \CODE{ShareNum} node in HIR shown below. It describes a general secret sharing protocol. The \CODE{provider} is the one who contributes the \CODE{value} that are shared among a set of \CODE{players} with \CODE{threshold}. And the set of \CODE{observers} are allowed to access the value once it gets combined.
\begin{lstlisting}
case class ShareNum(
  val provider: Set[Rep[SOwner]], // who provides it
  val players: Set[Rep[SOwner]], // players
  val observers: Set[Rep[SOwner]], // who observes it
  val threshold: Int, // threshold
  val value: Rep[SShareNum] // shares
)
\end{lstlisting}

In addition, the HIR provides libraries for implementing secure computations. Those libraries are not supported in general-purpose compilers, but are essential to build interesting multi-party applications with security guarantees.
For example, the HIR provides array indexing on cipher texts. Let us assume that \texttt{arr} is an HIR array. The following lists its operations:
\begin{itemize}
  \setlength\itemsep{-.5em}
  \item \lstinline|arr(i)| - array index, where $i$ is either a plaintext or a cipher text.
  \item \lstinline|arr.update(i, v)| - update the $i$th element with the value $v$, where $i$ is either a plaintext or a cipher text.
  \item \lstinline|arr.slice(i, j)| - array slicing from the $i$th element until the $j$the element, where $i$ and $j$ are plaintext.
  \item \lstinline|arr.length| - the length of the array
\end{itemize}

The way these array operations with secure indices are currently implemented is through, essentially, a naive ORAM: to index into an array with a cipher text index, the compiler will generate a circuit that accesses every array element, then uses a secure selector (multiplexer) to output the desired array element. This is equivalent to a set of if-then-elses to choose the desired array element, except with $\log$ depth instead of linear depth. Writing to an array element with a cipher text index is the equivalent of an array copy, where each element of the new array performs a check for whether the old element of the array should be copied, or the ``update'' value should be copied.

As implementation details of cryptographic backends are abstracted away from the HIR, our framework can be easily extended to support more advanced cryptographic backends, for example, a backend with oblivious RAM (ORAM). Here, we would leverage HIR's ability to provide backend-specific rewrite rules, and would directly rewrite array operations to ORAM operations

\paragraph{Type system.}
HIR also abstracts away the implementation details of cryptographic primitives and protocols. For example, an addition operation does not specify how a secure addition is achieved as different protocols perform in different ways. But the type rules provide an approximation of data access policy that specifies how data is provided, accessed, and shared. For example, an addition operation on two shared numbers is only allowed on the same set of players with the same threshold. And the result is provided by either one of its operand's providers with the same set of players with the same threshold, and is allowed to be accessed by either of one the operands' observers.
\begin{lstlisting}[basicstyle={\footnotesize\ttfamily}]
def +(x: ShareNum, y: ShareNum) = {
 assert(x.players.equals(y.players))
 assert(x.threshold == y.threshold)
 ShareNum(x.provider | y.provider, players,
 x.observers | y.observers, threshold, value.+(y.value))
}
\end{lstlisting}

Given a cryptographic backend, HIR is further rewritten to a program with the corresponding cryptographic semantics. And the HIR type system is refined to provide more precise information on data access policy. For example, the type rule of the addition operation is refined to the following when using the additive secret sharing scheme.
\begin{lstlisting}[basicstyle={\footnotesize\ttfamily}]
def +(x: ShareNum, y: ShareNum) = {
 assert(x.players.equals(y.players))
 assert(x.players.size == x.threshold)
 assert(x.threshold == y.threshold)
 ShareNum(x.provider | y.provider, players,
 x.observers & y.observers, threshold, value.+(y.value))
}
\end{lstlisting}
The type rule checks it is a $n$-out-of-$n$ secret sharing scheme, i.e., \CODE{x.players.size == x.threshold}.
This type rule provides a stronger security guarantee.
The refined type system guarantees that the generated HIR program complies with the semantics of the backend. For example, an FHE target program is not transformed into a program that may invoke secret sharing primitives.

\subsection{Obliviousness}
\label{sec:obliv}
In addition to bridging the semantic gap between a high and a low-level language, our compiler also bridges the semantic gap of obliviousness. Boolean circuits and Arithmetic circuits are oblivious in the sense that they perform the same sequence of operations independently of the input. A program without privacy concern change their flow of control according to the input: they execute statements conditionally, loop for a variable number of steps, etc.
The following transformations may seem quite inefficient at first sight, but they are absolutely required in order to maintain obliviousness.
\paragraph{Encrypted Array Indexing}
Indexing an array with a cipher text translates to a multiplexer circuit which takes every element of the array as an input and outputs the element in the position that matches the indexing cipher text.
This multiplexer circuit consists integer comparators and selectors.

\paragraph{Conditional Execution}
After a type-checked Harpoon program is translated to the program written in HIR, there are two types of if-constructs allowed. One is the standard if-statement where its condition depends on plaintext comparison, and the two branches consist of a sequence of statements that may have side effects.
The other has the form \CODE{z = \KW{if}(b)\{x\}\KW{else}\{y\}}, where the value of \CODE{b} is the result of private comparisons. Obliviousness is effectively guaranteed by executing both the consequent and alternative branches. If the backend is a Boolean circuit, this if-construct is further implemented as a selector. If the backend is an arithmetic circuit, the program is transformed to \CODE{z = b * x + (1 - b) * y}.

Consider the following Harpoon code snippet. The variable \CODE{arr} stores a sequence of shared numbers, the comparison result of \CODE{max < arr(i)} is a shared number as well. So the program
\begin{lstlisting}
if (max < arr(i)) { max = arr(i) }
\end{lstlisting}
is transformed to
\begin{lstlisting}
val b = max < arr(i)
max = b * arr(i) + (1 - b) * max
\end{lstlisting}
Note that such a program transformation is non-trivial for a program allowing shared mutable states, due to the complexity of identifying potential side effects for the two branches.
Currently, an if-statement will be transformed if the side effects of its two branches can be syntactically detected.
\paragraph{Loops and Recursion}
All function calls are treated as macros and simply inlined where they are called. All loops are simply unfolded as the number of iterations is a compile-time constant).
\figref{fig:gcd} demonstrates our treatment for recursive calls, where the obliviousness is achieved by using the extra plaintext parameter \CODE{d} in the right side of the figure. In this transformed program, the value \CODE{d} is initialized by the Harpoon annotation and decreases with each iteration. That makes sure the recursive calls only iterates \CODE{d} times.

\begin{figure*}[htp]
\small
  \begin{tabular}{l c r}
  \begin{minipage}[t]{0.2\textwidth}
    Scala Program
    \begin{lstlisting}[basicstyle={\footnotesize\ttfamily}]
val a = 5;
val b = 15;
def gcd(x: Int, y: Int)
 : Int = {
  if (x == 0) y
  else gcd(y
}
println(gcd(a, b))
  \end{lstlisting}
  \end{minipage} &
  \begin{minipage}[t]{0.3\textwidth}
    Harpoon Program
    \begin{lstlisting}[basicstyle={\footnotesize\ttfamily}]
@sec(alice) val a = 5;
@sec(alice) val b = 15;
@bound(5)
def gcd(x: Int @sec, y: Int @sec)
  : Int @sec = {
  if (x == 0) y
  else gcd(y
}
@reveal(alice) val r = gcd(a, b)
println(r)
    \end{lstlisting}
  \end{minipage} &
  \begin{minipage}[t]{0.2\textwidth}
  HIR Program
  \begin{lstlisting}[basicstyle={\footnotesize\ttfamily}]
val o = Owner(alice)
val a = Num(o, 5);
val b = Num(o, 15);
topFun gcd(d: Rep[Int], x: Rep[SNum], y: Rep[SNum])
  : Rep[SNum] = {
  if (d == 0) y
  else
    if (x == 0) gcd(d-1, x, y)
    else gcd(d - 1, y
}
val r = Num(o, gcd(5, a.value, b.value)).eval(o)
println(r)
  \end{lstlisting}
  \end{minipage}
\end{tabular}
  \caption{An example: Computing the Greatest Common Divisor(GCD) of two numbers. The one on the left is the Scala textbook implementation. The one in the middle is the Harpoon program. The annotations mean that a user, \CODE{alice}, owns the data \CODE{a} and \CODE{b}, and wants to compute the GCD of them. A different party receives and stores the data in an encrypted form, performs computation on the encrypted data, and provides the encrypted results to \CODE{alice}. Note that the \CODE{bound} annotation indicates maximum number of times the function gets called. The one on right is the HIR program translated from the Harpoon program in the middle. The translated \CODE{gcd} function has one extra parameter \CODE{d} initialized by 5, and decreases with each iteration.}
  \label{fig:gcd}
\end{figure*}

\subsection{Code Generation}
\paragraph{Cryptographic Backends}
In the context of building circuits, LMS is used to specialized a circuit with respect to a target backend. The outcome of such a programmatic specialization is a compiled target of the circuit.

The code generator transforms an abstract circuit into a concrete one for a given backend. For example, the following adder expressed by HIR is specialized to the Boolean circuit shown in \figref{fig:add-tfhe} and arithmetic circuit shown in \figref{fig:add-bgv} in the \appref{sec:appA}.
\begin{lstlisting}
val o1 = Owner();
output((Num(o1, 10).+(Num(o1, 5))).eval(o1))
\end{lstlisting}
The essence of multi-stage programming is to generate efficient programs using high-level constructs without runtime penalty \cite{taha2004gentle}.
The example in \figref{fig:sum} a shows a code snippet that generates a for loop. Note that the \CODE{if} condition is composed of a plaintext Boolean type, so this code is executed at code generation time as shown \figref{fig:sum} b.
\begin{figure}[!htp]
\small
\begin{tabular}{l}
(a) HIR code example:\\
\begin{lstlisting}[basicstyle=\scriptsize\ttfamily]
val sum = topFun((x: Rep[SNumArray], len: Rep[Int]) => {
  var n = 0;
  val b = true
  var res = Num(o1, 0).value
  while (n < len) {
    if (b) {
      res = res + x(n)
    }
    n += 1
  }
  res
})
\end{lstlisting}
\\
(b) Generated C code of TFHE backend:\\
\begin{lstlisting}[language=C,basicstyle=\scriptsize\ttfamily]
const LweSample* x3(const LweSample* x4, int x5){
 int x6 = 0;
 const LweSample* x7 = num_init(0, 64 ,x2);
 while (x6 < x5) {
  x7 = add(x7, array_index(x4, x6, 64, x0), 64, x0);
  x6 = x6 + 1;
 }
 return x7;
}
\end{lstlisting}
\end{tabular}
\caption{(a) HIR code example. (b) Generated C code of TFHE backend.}
\label{fig:sum}
\vspace{-1.5em}
\end{figure}

\paragraph{Resource Estimation}\label{resource-estimation}
Resource Estimation acts as another backend for the compiler, which generates a graphical representation of the HIR nodes circuit and feeds it to a generic "Evaluator" that walks the graph and accumulates some information at each node.
The estimator is parameterized on the given resource model, which is an assignment of costs to each node and edge type in the graph, as well as a depth of each edge.

At the most basic level, the resource estimation framework expects an enumeration of the abstract "gates" for the particular cost model, as well as a description of how each HIR node type affects these gates and depths. The gates are what the total cost is tallied in terms of. As an example, a cost model for one of the secret sharing backends might have \emph{round complexity} and \emph{communication complexity} as gates, whereas a circuit backend might literally have \emph{AND}, \emph{OR}, and \emph{NOT} as its gates.
The evaluator then walks the HIR graph and accumulates the abstract gate costs produced by each node, and tracks the maximum total depth encountered for critical path estimation. In the case of a secret sharing scheme, walking the graph will (potentially) increment round and communication complexity as new computation nodes are encountered, whereas a circuit backend will increment gate costs. These gate costs are then instantiated with specific costs (in terms of lower-level operations) based on the resource estimates determined by the cryptographic experts.

This framework can also be easily extended to evaluate costs that do not follow this simple model. All that is needed is a definition for some data structure to be accumulated at each HIR node (by default, this consists of a mapping from gate type to gate count and an integer for current depth), and a transfer function for how each node type accumulates into this structure.

Each cost model can also be parameterized on some values which are configurable but known at compile time (such as integer bitwidth), the prime modulus which can be determined from the security specifications, and specific edge costs.

The ability to estimate the cost of a program in multiple backends is useful when selecting a target, as well.
Programs are sometimes inherently better suited to execution in one protocol instead of another.
If the cost for these two protocols are comparable (e.g. both models measure ``communication complexity''), then we can generate a resource estimate for the program in each available backend to determine which backend would be best suited for execution.

\section{Introduction}
\label{sec:intro}
\vspace{-1ex}
Secure multi-party computation (MPC) enables a group of distrusting parties to jointly perform computations without revealing any participant's private data that they do not wish to share with others.
It has broad practical applications, e.g., Yao's millionaires problem ~\cite{yao1982protocols}, secure auctions~\cite{auction06}, voting, privacy-preserving network security monitoring~\cite{sepia}, privacy-preserving genomics~\cite{wang2015efficient,jagadeesh2017deriving}, private stable matching~\cite{Doerner16}, ad conversion~\cite{Kreuter17}, spam filtering on encrypted email~\cite{gupta2017pretzel} and privacy-preserving machine learning~\cite{chet}.
Secure MPC applications are generally realized as circuits communicating information -- both private and public -- among parties.

Although MPC techniques and protocols have seen much success in the cryptography community, it is still challenging to build practical MPC applications by utilizing these techniques.
Executing cryptographic protocols is notoriously slow, due to the encryption and communication overhead.
The largest benchmark reported in Fairplay~\cite{malkhi2004fairplay} -- a secure two-party computation system -- was finding the median of two sorted input arrays containing ten 16-bit numbers from each party. Running the benchmark required execution of 4383 gates, and took over 7 seconds on a local area network.
While improving computing capabilities and network bandwidth, implementation techniques can contribute to 3-4 orders of magnitude improvements~\cite{evans2017pragmatic}.
These techniques include optimizations that reduce the number of gates and the depth of a circuit and reduce the computational costs of executing a cryptographic protocol.
However, such optimizations do not exist in general-purpose compiler frameworks.

While several MPC frameworks have been proposed~\cite{SPDZ,oblivC,scale-mamba,lu2019honeybadgermpc,aby,securenn,jiff,mpyc,zhang2013picco,ezpc,rastogi2014wysteria,liu2015oblivm,CBMC-GC,emp-toolkit,zahur2015obliv}, they either provide low-level cryptographic primitives or provide high-level abstractions like traditional programming languages.
The low-level frameworks provide high degrees of customized protocol execution, but the users are generally expected to be experts in either one or both of cryptography and optimizing circuits.
These MPC frameworks provide little or no type safety to prevent semantic errors,
and it is difficult to write applications in a way that is portable across different protocols.
The high-level frameworks provide traditional programming abstractions that hide the data-oblivious nature of secure computations from programmers.
But these frameworks are tied to only one or a few protocols and their compilation procedures -- from high-level abstractions to low-level primitives -- are not easy to extend to perform application specific optimizations~\cite{oblivC}.

\paragraph{Contributions} The main intellectual contribution of this paper is a toolchain for building secure MPC applications called HACCLE (High Assurance Compositional Cryptography: Languages and Environments).
Our framework contains an embedded domain-specific language (eDSL) \emph{Harpoon} for designing MPC-based applications.
Allowing seamless construction of MPC-based applications by software developers without expertise in advanced cryptography is the main purpose of providing such a high-level programming language.
A Harpoon program is compiled to an acyclic combinational circuit, which is described in a HACCLE Intermediate Representation (HIR).
HIR exposes the essential data-oblivious nature of MPC, and allows cryptography experts to experiment with new primitives and protocols.
Our framework also provides a specialized backend for estimating the resource usage (\textit{e.g.} compute time and memory space) prior to execution.

This paper makes the following specific contributions:
\vspace{-0.2em}
\begin{itemize}
\itemsep0em
\item \textbf{HACCLE Toolchain}: A compilation framework to build and execute MPC applications written in Harpoon -- an embedded domain-specific language (eDSL) in Scala.
\item \textbf{HACCLE Intermediate Representation (HIR)}: Extensible circuit-like intermediate representation tailored to abstract cryptographic primitives used in MPC.
\item \textbf{Optimization Strategies}: Methods for optimizing the MPC application by specialization as it flows through each stage of our HACCLE toolchain.
\end{itemize}

The rest of the paper is organized as follows.
\secref{sec:bkg} provides background on cryptographic protocols involved in secure MPC and motivates the need for an ecosystem to build MPC-based applications.
We describe the key impediments for building practical MPC applications with the example of secure auctions.
\secref{sec:workflow} describes the HACCLE toolchain and associated workflow.
\secref{sec:haccle} illustrates HIR, the key component of our compiler.
\secref{sec:optimization} describes the optimizations implemented in our compiler toolchain.
\secref{sec:evaluation} discusses our toolchain on three case studies in detail.
\secref{sec:relatedwork} summarizes related work and \secref{sec:conclusion} concludes the paper.
\section{Language}
\label{sec:language}

\figref{fig:syntax} shows the grammar.
\begin{figure}[h]
\centering
\begin{grammar}%
\begin{tabular}{r r r l}
$~$Owner & \nonterm{o} & \: & \{\nonterm{n}\} \| \nonterm{o}$_1\cup$\nonterm{o}$_2$
$~$Atomic Type & $\alpha$ & \: & \KW{int} \| \KW{bool}
$~$Composite Type & $\phi$  & \: & (\nonterm{\KW{bool}},\nonterm{o}) \| (\nonterm{\KW{int}},\nonterm{o}) \| \nonterm{arr}(\KW{int},\nonterm{o}) \| $\cdots$
$~$Type & \nonterm{T} & \: & \nonterm{T$_1$} \| \nonterm{T$_2$}
Expression & \nonterm{\Expr} & \: & \nonterm{n} \| \nonterm{x} \| \KW{eval}(o, \Expr) \| \nonterm{\Expr$_1$}$\oplus$\nonterm{\Expr$_2$} \|  \KW{if} \nonterm{\Expr} \KW{then}\{\nonterm{\Expr$_1$}\}\KW{else}\{\nonterm{\Expr$_2$}\}
Statement & \nonterm{S} & \: & \KW{skip}; \| \KW{val}  \nonterm{x}:\nonterm{T}:=\nonterm{\Expr}; \| \KW{while}(\nonterm{x}<\nonterm{n})\{\nonterm{S}\} \| \nonterm{S$_1$}\nonterm{S$_2$}
& \nonterm{$\oplus$} & \: & $=$ \| $+$ \| $-$ \| $\ast$ \| $\leq$ $\dots$ %
\end{tabular} %
\end{grammar}
\caption{The syntax of the intermediate language}
\label{fig:syntax}
\end{figure}

\begin{figure}[!h]
\centering
\begin{mathpar}
\inferrule{}
{\TYPEJUDG {n} {\KW{int}} }

\begin{array}{l}
\inferrule{}
{\TYPEJUDG{x}{T}} \\
\mbox{\textbf{where} } \Gamma(x) = T
\end{array}

\begin{array}{l}
\inferrule{\TYPEJUDG{\Expr}{(\alpha, o)}}
{\TYPEJUDG{\KW{eval}(o', \Expr)}{\alpha}} \\
\mbox{\textbf{where} } valid(o, o')
\end{array}

\inferrule{\TYPEJUDG{\Expr_1}{\alpha_1} \\ \TYPEJUDG{\Expr_2}{\alpha_2} \\ \TYPEJUDG{\oplus}{\alpha_1 \rightarrow \alpha_2 \rightarrow \alpha}}
{\TYPEJUDG{\Expr_1 \oplus \Expr_2}{\alpha}}

\inferrule{\TYPEJUDG{\Expr_1}{(\alpha_1, o_1)} \\ \TYPEJUDG{\Expr_2}{(\alpha_2, o_2)} \\ \TYPEJUDG{\oplus}{\alpha_1 \rightarrow \alpha_2 \rightarrow \alpha}}
{\TYPEJUDG{\Expr_1 \oplus \Expr_2}{(\alpha, o_1 \cup o_2)}}

\inferrule {\TYPEJUDG{\Expr}{(\KW{bool},o)} \\ \TYPEJUDG{\Expr_1}{(\alpha_1, o_1)} \\ \TYPEJUDG{\Expr_2}{(\alpha_2, o_2)} }
{\TYPEJUDG{\KW{if} ~ \Expr ~ \KW{then} ~ \{\Expr_1\} ~ \KW{else} ~ \{\Expr_2\}} {(\alpha, o \cup o_1 \cup o_2)}}

\inferrule {\TYPEJUDG{\Expr}{\KW{bool}} \\ \TYPEJUDG{\Expr_1}{\alpha} \\ \TYPEJUDG{\Expr_2}{\alpha} }
{\TYPEJUDG{\KW{if} ~ \Expr ~ \KW{then} ~ \{\Expr_1\} ~ \KW{else} ~ \{\Expr_2\}} {\alpha}}

\end{mathpar}
\caption{The typing rules for expressions. The predicate valid will be further defined when an instance scheme is given.}
\label{fig:type-expr}
\end{figure}

\begin{figure}[h]
\centering
\begin{mathpar}
\inferrule{}
{\TYPEJUDG {n} {\KW{int}} }

\begin{array}{l}
\inferrule{}
{\TYPEJUDG{x}{T}} \\
\mbox{\textbf{where} } \Gamma(x) = T
\end{array}

\begin{array}{l}
\inferrule{\TYPEJUDG{\Expr}{(\alpha, \{n\})}}
{\TYPEJUDG{\KW{eval}(\{n\}, \Expr)}{\alpha}} \\
\end{array}

\inferrule{\TYPEJUDG{\Expr_1}{\alpha_1} \\ \TYPEJUDG{\Expr_2}{\alpha_2} \\ \TYPEJUDG{\oplus}{\alpha_1 \rightarrow \alpha_2 \rightarrow \alpha}}
{\TYPEJUDG{\Expr_1 \oplus \Expr_2}{\alpha}}

\inferrule{\TYPEJUDG{\Expr_1}{(\alpha_1, \{n\})} \\ \TYPEJUDG{\Expr_2}{(\alpha_2, \{n\})} \\ \TYPEJUDG{\oplus}{\alpha_1 \rightarrow \alpha_2 \rightarrow \alpha}}
{\TYPEJUDG{\Expr_1 \oplus \Expr_2}{(\alpha, \{n\})}}

\inferrule {\TYPEJUDG{\Expr}{(\KW{bool}, \{n\})} \\ \TYPEJUDG{\Expr_1}{(\alpha, \{n\})} \\ \TYPEJUDG{\Expr_2}{(\alpha, \{n\})} }
{\TYPEJUDG{\KW{if} ~ \Expr ~ \KW{then} ~ \{\Expr_1\} ~ \KW{else} ~ \{\Expr_2\}} {(\alpha, \{n\})}}

\inferrule {\TYPEJUDG{\Expr}{\KW{bool}} \\ \TYPEJUDG{\Expr_1}{\alpha} \\ \TYPEJUDG{\Expr_2}{\alpha} }
{\TYPEJUDG{\KW{if} ~ \Expr ~ \KW{then} ~ \{\Expr_1\} ~ \KW{else} ~ \{\Expr_2\}} {\alpha}}

\end{mathpar}
\caption{The typing rules for expressions in the TFHE scheme.}
\label{fig:type-expr-tfhe}
\end{figure}

\begin{figure}
\begin{mathpar}
\inferrule{}
{\TYPEJUDG {\KW{skip};} {ok(\Gamma  )}}

\begin{array}{l}
\inferrule{\TYPEJUDG{\Expr}{\alpha}}
{\TYPEJUDG {\KW{var} ~ x : \alpha := \Expr;} {ok(\Gamma, x : \alpha  )} } \\
\mbox{\textbf{where} } x \not\in \DOM(\Gamma)
\end{array}

\begin{array}{l}
\inferrule{\TYPEJUDG{\Expr}{(\alpha, o)}}
{\TYPEJUDG {\KW{var} ~ x : (\alpha, o) := \Expr;} {ok(\Gamma, x : (\alpha, o) )}}  \\
\mbox{\textbf{where} } x \not\in \DOM(\Gamma)
\end{array}

\inferrule{ \TYPEJUDG{\Expr}{\KW{bool}} \\ \TYPEJUDG{\Stmt}{ok(\Gamma'  )} }
{\TYPEJUDG{\KW{while} ~ \Expr ~ \{ \Stmt \}}{ok(\Gamma  )} }

\inferrule{\TYPEJUDG{\Stmt_1}{ok(\Gamma''  )} \\ \TYPEJUDGLIST{\Gamma''  }{\Stmt_2}{ok(\Gamma'  )} }
{\TYPEJUDG{\Stmt_1\Stmt_2}{ok(\Gamma'  )}}
\end{mathpar}
\caption{The typing rules for statements}
\label{fig:type-stmt}
\end{figure}

\section{Optimization}
\label{sec:optimization}
\vspace{-1ex}
Our compiler contains a sequence of optimization transformations.
For example, the peephole optimization, \textit{e.g.}, \CODE{x \&\& true} is optimized to just \CODE{x};  common subexpression elimination (CSE), \textit{e.g.}, \CODE{x = a + b; y = (a + b) * c} is optimized to \CODE{x = a + b; y = x * c}; constant folding, and dead code elimination (DCE).
In addition to those optimizations that a general purpose compiler has, we identify several optimizations involving encrypted values.
Given an in-memory representation of a Boolean circuit or an arithmetic circuit, the goal of the optimization is to reduce the depth of the circuit and the number of costly gates.

\subsection{Scalar Multiplication}
\label{sec:privat-mutl}
The multiplicative depth of circuits is the main practical limitation in performing computations over encrypted data.
We identify the opportunity when one of the operands of a multiplication is plain text.
For example, the multiplication is eliminated if the plain text is 0 or 1.
Moreover, consider the case of calculating $pow(x, n)$, where $x$ is an encrypted data.
The compiler divides the computation into subproblems of size $n/2$ and call the subproblems recursively.
\figref{fig:pow} shows the program of computing $pow(2, 8)$, where 2 is private. The Harpoon program is transformed to its corresponding HIR program, and is generated to the TFHE program, where the function \CODE{unum\_mul} multiplies two 64-bit encrypted integers. Our generate program only needs $O(\log n)$ multiplies.
Although this optimization is simple, but, as you can see from this example, has a dramatic impact on performance.

\begin{figure}[!htp]
\small
\begin{minipage}{0.25\textwidth}
\small Harpoon Program:
\begin{lstlisting}[basicstyle=\footnotesize]
@sec(alice) val a = 2;
scala.math.pow(2, 8);
\end{lstlisting}
\end{minipage}\begin{minipage}{0.25\textwidth}

  \footnotesize HIR Program:
\begin{lstlisting}[basicstyle=\footnotesize]
val o1 = Owner();
UNum(o1, 2).pow(8)
\end{lstlisting}
\end{minipage}
\begin{minipage}{0.5\textwidth}

  \footnotesize Generated TFHE program:
\begin{lstlisting}[language=C,basicstyle=\small\ttfamily]
const LweSample* x3 = unum_init(2, 64, x2);
LweSample* x4 = unum_mul(x3, x3, 64, x0);
LweSample* x5 = unum_mul(x4, x4, 64, x0);
return unum_mul(x5, x5, 64, x0);
\end{lstlisting}
\end{minipage}
\caption{Example of computing $pow(2, 8)$, where $2$ is private.}
\label{fig:pow}
\end{figure}

The effect of the optimization is clearly demonstrated in \figref{fig:pow-graph}, which shows the graphs of the generated circuits after and before optimization respectively. The left is a depth-3 circuit, and contains three multiply gates. The right is a depth-7 circuit, and contains 7 multiply gates.

\begin{figure}[t]
\small
\centering
\makebox[0pt][c]{%
\begin{minipage}{0.35\textwidth}%
\hspace{1cm}\includegraphics[scale=.28]{figures/graph_pow_un.pdf}
\end{minipage}\hspace{0cm}\begin{minipage}{0.25\textwidth}
    \includegraphics[scale=.25]{figures/graph_pow.pdf}
\end{minipage}}
\caption{Graphs of computing $pow(2, 8)$: before (left) and after applying optimizations (right). }
\label{fig:pow-graph}
\end{figure}
The generated graphs show an abstract model of execution cost where each operation is treated as atomic; However, the resource estimation framework can be specialized to particular backends by providing the corresponding models of execution cost (in terms of communication complexity, number of logic gates, etc.)
These backend-specific resource estimates can be used to compare different optimization strategies and intelligently select the appropriate one based on the execution semantics of the targeted backend.
As mentioned in \secref{resource-estimation}, in addition to selecting the right set of optimizations to use, these specialized estimates even let us pick the most optimal backend to target.

\subsection{Private Comparisons}
\label{sec:private-comp}
The private comparison is a major bottleneck in MPC protocols due to their inherent non-arithmetic structure \cite{couteau2016efficient}.
It privately determines whether \CODE{a < b}, where \CODE{a} and {b} are considered as private information.
Operators involve private comparisons include \CODE{<}, \CODE{<=}, \CODE{>}, \CODE{>=}, \CODE{==} and \CODE{!=}.
One operator may be encoded by two or more other operators, e.g., \CODE{a != b} is equivalent to \CODE{a > b || a < b}.
However, the two expressions may have different costs.
We identify some implementation heuristics that help us generate efficient programs.

We take the HoneyBadgerMPC library as an example to demonstrate our implementation technique.
HoneyBadgerMPC provides two comparison protocols: LessThan and Equality. As their names indicated, they allow us to evaluate \CODE{a < b} and \CODE{a == b} on shared values. The result is 1 if it is true, otherwise is 0. What's more, the result is also secret shared due to the fact that the result of comparison leaks information about input. Building an MPC compiler requires us to implement other operators in terms of these two.
Taking the operator \CODE{>=} as an example. A naive and intuitive implementation is encoding \CODE{a >= b} as \CODE{(b < a) + (a == b)}. An alternative implementation is encoding \CODE{a >= b} as \CODE{1 - (b < a)}.
Our abstract resource estimator will generate one LEQ gate, one ADD gate and one EQUAL gate for the first implementation, and one SUB gate and LEQ gate for the second implementation.
As mentioned in \secref{resource-estimation}, each backend has its own resource model.
In the HoneyBadgerMPC resource model, the costs of addition and subtraction are trivial since they require no communication, and the multiplication takes one rounds and one multicast to finish. When it comes to comparison, the round complexity of comparison is seven times more than the cost of multiplication \cite{reistad2007secret}, the communication cost is even more expensive. Also, the cost of equality check is higher than less than operation. Thus, we believe the second implementation is optimal due to the reduced number of comparisons.
This is how we experiment with optimized implementations with the help of our resource estimators.

To verify the above observation, we perform a set of private comparisons in a HoneyBadgerMPC program (on a single Ubuntu 18.04 LTS machine of 16 GB RAM with 8 Intel Core i7 Processors). Our tests execute 100 times of the greater or equal comparisons on two randomly generated numbers. \tbref{tb:gre} compares the running time of the two encoding.
\begin{table}
\centering
\begin{tabular}{ | l | l | }
\hline
Encoding \CODE{a >= b} & Execution Time \\
\hline
\CODE{(b < a) + (a == b)} & 0.23s\\
\hline
\CODE{1 - (b < a)} & 0.10s\\
\hline
\end{tabular}
\caption{Execution time of evaluating \CODE{a >= b} for 100 times, where \CODE{a} and \CODE{b} are randomly generated number ranging from 1 to 100.}
\label{tb:gre}
\end{table}

\section{Related Work}
\label{sec:relatedwork}
\vspace{-1ex}
There have been many MPC frameworks proposed in recent years and several of them are already integrated into HACCLE. We list the prominent MPC frameworks as follows.

SCALE-MAMBA \cite{scale-mamba} is an existing MPC framework that is closest to HACCLE.  We utilize it as one of our cryptographic backends to implement secret sharing based protocols and FHE based protocols. It is a combination of a compiler and a runtime environment where optimizations can be performed at lower level. Compared with SCALE-MAMBA, HACCLE also provides a resource estimation framework and focuses more on optimization at higher level.

HoneybadgerMPC~\cite{lu2019honeybadgermpc} is another MPC backend of HACCLE that supports secret-sharing based protocols. The uniqueness of HoneybadgerMPC is the combination of a robust online phase and an optimistic non-robust offline phase. It provides fairness guarantees even in the asynchronous network setting and also preserves efficiency to make MPC programs practical to run.

As privacy preserving machine learning becomes more and more popular, many frameworks have been developed specifically for this use case, such as ABY \cite{aby}, ABY3~\cite{aby3}, CHET \cite{chet}, EzPC \cite{ezpc}, CrypTFlow \cite{kumar2019cryptflow} and secureNN \cite{securenn}. These frameworks are highly optimized for machine learning and are designed for the two-party setting or three-party setting. We choose not to include them due to our desire to support an arbitrary number of parties.

There are also many other MPC frameworks such as Viff \cite{vifflib}, Jiff \cite{jiff}, MPyC \cite{mpyc} and PICCO \cite{zhang2013picco}. Theoretically HACCLE can embed any framework as a backend so while we have not integrated all of these at this time, they should all fit into HACCLE if desired in the future.

\section{HACCLE Workflow}
\label{sec:workflow}
\vspace{-1ex}
\begin{figure}[htp]
    \centering
    \includegraphics[scale=.25]{figures/workflow.pdf}
    \caption{HACCLE Compilation Framework}
    \label{fig:framework}
    \vspace{-1ex}
\end{figure}
In this section, we describe the flow of our HACCLE compilation framework.
Figure~\ref{fig:framework} shows an overview of the compilation flow.
The secure multiparty programs are written in Scala and the core portion of the computation is written in Harpoon, an eDSL.
In the very first stage of the compilation flow, the input program is staged to a complete Harpoon program that consists of an entry point for passing the inputs provided by the parties, computations on those inputs and necessary revealing of results to the parties.
The Harpoon program is compiled to a protocol independent multi-level intermediate representation, HACCLE Intermediate Representation (HIR).
Computation represented by HIR is one big acyclic circuit.
Section~\ref{sec:haccle} illustrates attributes of HIR with examples.
The program represented in HIR is further lowered to include protocol specific instructions.
Finally, from the low-level HIR program code generation happens for respective protocol specific backends.
Resource estimation is one of the special note-worthy backends that instead of executing the computation, it estimates the amount of resources required to realize the computation using a specific protocol.
The following subsections illustrates the stages of our toolchain from writing the MPC application as a program to executing it using different cryptographic protocols.
\vspace{-1ex}

\subsection{Specifying the Program}

A programmer starts by providing a Scala program that embeds a secure computation.
The secure computation is written in {\em Harpoon}, our language for expressing multiparty computations (\secref{sec:harpoon}).
The Scala program runs at client locations, and is responsible for processing input, setting up communication channels, etc.
The Harpoon program actually performs the secure computation.
This secure computation is written parametrically: effectively, a Harpoon program is a function that accepts the number of parties and their inputs as parameters.

\subsection{Generating a Circuit}

\paragraph{Stage 1}
The first stage of compilation transforms the Scala + Harpoon program into a pure Harpoon program.
In other words, executing the Scala program stages away the {\em non-Harpoon} portions of the code: local input files are read and represented in memory, connections are set up to the relevant servers.

What is left after the stage 1 compilation is a Harpoon program that represents {\em just the secure computation that must be performed}. This program will eventually be transformed into a circuit that performs the desired secure processing. However, the secure computation is not ready for execution yet. Any publicly known information about the inputs (\textit{e.g.}, the bitwidths, or a maximum number input size) has not yet been incorporated into the circuit, and, of course, the input values are not yet known.

Crucially, a Harpoon program can have loops and recursive functions, but a programmer must provide upper bounds on the running time of those constructs that are derivable from publicly-known information. Note that a common piece of publicly available information about the input that may be used to define the bounds is the bitwidth of the input; but any other information about the input that is publicly known to all participants may also be used to generate the HIR program.

The key typing guarantee that Harpoon provides is that private data will not leak via public channels.

An important note here is that each Harpoon program represents a single secure computation that will compile to a single circuit.
Hence, the Harpoon program must compile down to a circuit whose size is determined only by the publicly available information about the inputs (to avoid leaking information).
In many applications, there are multiple secure computations that must occur (\textit{e.g.}, in database application, there may be multiple queries; each query represents a different secure computation).
Here, we leverage the blurred distinction between compile time and runtime.
Generating a Harpoon program happens at what programmers traditionally consider {\em run time}: the Scala program is {\em actually running} to produce the Harpoon program.
Hence, the {\em Scala program} can include a loop over the set of queries, and for each query, a new Harpoon program will be produced and compiled and executed.
The abstraction in Scala has no runtime overhead for the generated code
since it is executed at the Scala runtime,
offering the so-called ``abstraction without regret'' (Section~\ref{sec:staging}).

\paragraph{Stage 2}
The next step is to generate an {\em abstract circuit}: the Harpoon program is compiled down to the HACCLE Intermediate Representation (HIR, \secref{sec:haccle}), which is, essentially, a functional, bounded-size representation of the program. Here, the bounds information in the Harpoon program is used to unroll loops and inline recursive functions, leading to a function- and loop-free representation of the program. Because there are no longer any looping constructs, the HIR program is naturally single-assignment and functional. HIR supports scalars and arrays of bits, integers, and floats. An HIR program at this stage is still independent of a particular protocol. Hence, it is essentially a direct translation of the Harpoon program into HIR without considering the abilities of any particular backend.

The key typing guarantee that HIR provides at this level is that the appropriate HIR operation will be used based on whether inputs to an operation are private or public. For example, indexing into an array of private data using a public index produces different code (essentially, copying a particular wire) from indexing into an array of private data using a private index (essentially, using a selector construct to securely choose the appropriate element).

\paragraph{Stage 3}
The next compilation stage specializes an HIR circuit to a specific protocol. The choice of protocol is determined by the security specification file. Here, we do not change the {\em language} representation of the program---the resulting program is still in HIR. Instead, this stage rewrites HIR to limit the use of HIR operations to those supported by a particular backend. For example, a backend that only supports Boolean operations requires translating all operations on integers and floating point into bit-level operations. Similarly, a backend that only supports operations on integers will require translating floating point operations into decomposed operations on the component parts (mantissa and exponent).

Here, HIR switches to the use of backend-specific type systems that enforces the following property: a backend-specific HIR circuit that type checks will correctly enforce the requirements of that backend for security (e.g., ensuring that the set of sharers matches up when performing operations in a secret-sharing backend).

\paragraph{Stage 4}
The final step of generating a circuit is specific to the backend implementation the HACCLE framework is instantiated with. Here, the HIR circuit is translated to work with the particular backend (this is the key module interface provided by our system). This may require translating the circuit to a set of API calls (e.g., our TFHE backend), or transliterating the circuit into a different programming language (\textit{e.g.}, translating to Obliv-C for the garbled-circuit backend, or Scale-Mamba for the secret-sharing backend). The backend is configured based on the information in the security specification file.

At this point, the circuit is in an executable form, and it will execute, using the actual inputs from the various parties, to perform the desired secure computation.

\subsection{Resource estimation}
Resource estimation is implemented as another backend.
Here, protocol-specific HIR code, rather than being translated to work with a specific backend, will be translated into a graph representation of the circuit.
This graph representation is then incorporated into a {\em resource estimation program} that traverses this graph in various ways to compute different resource estimates: total amount of work, critical path length, FHE levels, etc.