Towards Secure Distributed Computations

Nowadays, there are plenty of networks that work in a cooperative way and form what we know as grids of computers. These grids are serving a lot of purposes, and they are used with good results for intensive calculation, because the joined computing power aids in solving complex functions. To cope with these new requirements and facilities, programming languages have had to evolve to new paradigms, including facilities to do distributed computing in a straightforward way.

Functional programming is a paradigm that treats computation as the evaluation of mathematical functions. Functional programming languages implement the concepts introduced by this paradigm. Usually, they are modelled using λ calculus, but other variants exist. In this line we have languages like ML, Haskell and (Pure)Lisp. This work has its focus on ML-like languages.

As part of the evolution in grid computing, some functional programming languages were adapted to handle these new requirements. To be used in distributed contexts, the calculi had to be extended with new paradigms. Theoretic support for concurrent and distributed programming was conceived. For concurrent programming the π calculus was created, and this formalism was extended for mobility on the Ambient calculus. From these approaches, new functional languages were created. Examples of concurrent programming languages are Pict, occam-pi and Concurrent Haskell. In the case of distributed programming languages, we can mention Nomadic Pict, Alice and Acute.

After the creation and utilization of such languages, an aspect remaining to be introduced is the security properties of these computations. The security properties of languages that execute on a single machine are difficult to achieve. Increased precautions must be taken into account when dealing with lots of hosts and complex networks. Distributed programming languages must achieve, among other properties, correctness in their own abstractions: they must satisfy type-safety and abstraction safety.

This work is concerned with correctness and safety in distributed languages, with focus on ML-like languages and the properties they have. To this aim, we have focused on a language called Acute. This language was born for doing research in distributed programming, and was created as a joint effort of the University of Cambridge and INRIA Rocquencourt. In Acute we have modern primitives for interaction between cooperating programmes. Two primitives, marshal and unmarshal, have been introduced with this in mind. Acute has powerful properties: type and abstraction safety are guaranteed along the distributed system. But this only happens when there are no entities that can tamper with data transmitted between hosts. If this situation occurs, safety can be no longer guaranteed.

The Acute language typechecks values at unmarshal time, to ensure their correctness. This can be done with values of concrete types, but if we have values of abstract types the situation is different: we may have only partial information to check, or the representation might not be available at all.

So, how can values of abstract types be secured, in the context of a distributed programming language? We propose the use of 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 certificate, or witness, that can be used with abstract types. If the value comes with a witness that the computation was performed correctly, the caller can verify this witness and know that the value was generated in a good way.

Throughout this thesis work, we will show how to add the PCR technique to a distributed programming language. The supporting infrastructure for the technique is introduced along with it. To check the values and associated witnesses produced by some host, we use the COQ proof checker for a precise and reliable verification.