Towards secure distributed computations

Abstract

In this paper, we present an infrastructure for securing distributed computations between hosts, using a novel technique called Proof Carrying Results. This technique is based on Necula's proof carrying code. Basically, the result of some computation comes equipped with a certicate, or witness, showing that the computation was made correctly. This witness can be used to verify that the value was generated in a good way. We will show how to add the PCR technique and its supporting infrastructure to a distributed programming language. This will make the language more robust against active adversaries, when the returned values of a computation are of abstract types. Finally, to check the values and associated witnesses produced by some host, we use the COQ proof checker for a precise and reliable veri cation.