Secure Multi-Party Computation (MPC) enables a group of $n$
distrusting parties to jointly compute a function using private
inputs. MPC guarantees correctness of computation and confidentiality
of inputs if no more than a threshold $t$ of the parties are corrupted. Proactive MPC (PMPC) addresses the stronger threat model of a
mobile adversary that controls a changing set of parties (but
only up to $t$ at any instant), and may eventually corrupt all $n$ parties over a long time. This paper takes a first stab at developing high-assurance
implementations of (P)MPC. We present high-assurance implementations of (P)MPC
protocols. We formalize in EasyCrypt, a tool-assisted
framework for building high-confidence cryptographic proofs, several
abstract and reusable variations of secret sharing and of (P)MPC protocols building on top
of them. Using those, we prove a series of abstract theorems for the
proactive setting. We implement and perform computer-checked security
proofs of concrete instantiations of all required (abstract) protocols in
EasyCrypt. We also develop a new tool-chain to extract
high-assurance executable implementations of protocols implemented and
verified in EasyCrypt that uses Why3 as an intermediate tool. Using
this new tool, we were able to extract code from our (P)MPC
formalizations and to conduct a practical evaluation of it by
comparing the performance obtained using our approach to the
performance of manually implemented versions using Python-based Charm framework for prototyping
cryptographic schemes. We argue that the small overhead of our
high-assurance executables is a reasonable price to pay for the
increased confidence about their correctness and security.