Validating the Horus Protocols

See also Securing and Hardening the Horus System

Overview

The following steps will be taken to validate Horus:

1. Build a ``reference implementation'' in the ML programming language.
2. Specify the Horus protocols in a temporal logic.
3. Formally verify protocols using the Nuprl Proof Development System.

Advantages of Using the ML Programming Language

ML is a programming language with:

• automatic data marshaling
• garbage collection
• static type checking
• a formal specification

We have built in ML a compact implementation of Horus suitable for verification of fault-tolerance and security properties.

Also, the subset of ML we use can be compiled to efficient, human-readable C code.

Use of Temporal Logic

We describe protocol properties using the Temporal Logic of Actions. For example, to say that whenever a message is sent via interface u, its size is at most max :

A protocol layer guarantees properties at its interfaces provided the environment obeys some assumptions :

To find the properties of a stack, we prove a theorem about the conjunction of all the layers' assume-guarantee formulas.

• Please use a Java-enabled browser to try our live demonstration of the verification of stacks composed of various layers.

Verifying ML Protocols

We verify the protocol layers using the Nuprl Proof Development System as shown in the following diagram:

See also Securing and Hardening the Horus System