CoRReCt: Compute, Record, Replay, Compare to Secure Computations on Untrusted Systems

If the system of an honest user is corrupted, all of its security may be lost: The system may perform computations using different inputs, report different outputs or perform a different computation altogether, including the leakage of secrets to an adversary.
In this paper, we present an approach that complements arbitrary computations to protect against the consequences of malicious systems. Tothis end, we adapt a well-known technique traditionally used to increase fault tolerance, namely redundant executions on different machines that are combined by a majority vote on the results. However, using this conceptually very simple technique for general computations is surprisingly difficult due to non-determinism on the hardware and software level that may cause the executions to deviate.
The CoRReCt approach, short for Compute, Record, Replay, Compare, considers two synchronized executions on different machines. Only if both executions lead to the same result, this result is returned. Our realization uses virtual machines (VMs): On one VM, the software is executed and non-deterministic events are recorded. On a second VM, the software is executed in lockstep and non-deterministic events are replayed. ... mehrThe outputs of both VMs, which are hosted on different machines, are compared by a dedicated trusted entity and only allowed if they match. The following security guarantees can be proven:
– Integrity: If at most one host is corrupted, then the computation is performed using the correct inputs and returns either the correct result or no result at all.
– Privacy: If timing side-channels are not considered and at most one host is corrupted, the additional leakage introduced by our approach can be bounded by bits, where n is the number of messages sent. If timing side-channels are considered and the recording system is honest, the same leakage bound can be obtained.
As VMs can be run on completely different host platforms, e.g. Windows on Intel x86-64 or OpenBSD on ARM, the assumption of at least one system being honest is very plausible.
To prove our security guarantees, we provide a proof within a formal model. To demonstrate the viability of our approach, we provide a ready-to-use implementation that allows the execution of arbitrary (networked) x86-64 Linux programs and discuss different real-world applications.