Björn Gohla: A Haskell Binding for OpenBSD Pledge

The pledge system call on OpenBSD is a voluntary security mechanism, that a process can use to restrict the available kernel API. It is used throughout the OpenBSD base system and some ports, to guard against undiscovered exploits, following the defense in depth principle. System calls are aggregated into related groups called promises. It is considered good practice to discard a promise, i.e., access to any part of the kernel API, as soon as it is no longer needed.

Haskell is a lazy functional language with a powerful static type system. Side-effecting computations, notably IO, are clearly distinguished from pure computations in the type system. Effectful computations of the same kind can be sequenced using a sequencing operator, and this ensures control over the ordering of effects in the presence of lazy evaluation. Haskell also provides special syntax that makes effectful functional code look like familiar imperative code.

We will demonstrate a refinement of this approach to IO-effecting computations with type level information about pledge promises, and an appropriate sequencing operator, that causes static computation of the combined promises for sequenced actions and automatically inserts the correct pledge calls. This has no added runtime cost, apart from serializing the promise set and calling pledge.

Using this approach, we can guarantee that promises are always discarded at the earliest possible time, even in potentially large applications, assuming that the basic actions have been labeled correctly. We can also use type annotations to either let the compiler work for us and compute the required promise set for a given sequence, or else specify a promise set and be assured that a given sequence does not violate it.

We will provide the necessary background in Haskell and show some real world application code using this interface.

Björn Gohla:

He is a part-time user of OpenBSD and works as a Haskell engineer at Scrive.