Viewed from a broader perspective, our reference implementation of Horus demonstrates a possible methodology for refining and verifying a class of complex but modular communication systems. Such a methodology responds to the difficulties of applying a comparable process to large systems written in C. Our approach is to translate an already existing system to a high level language (such as ML) which is amenable to the refinement and verification needed to ``harden'' the system. This will rarely require a complete verification of the system, but rather entails a continuing process of proving the complex and uncertain properties of the system, so that the remaining subgoals are more and more obviously true.
Once the reference implementation has been built, refined, and verified, we translate it back to C as a new production implementation to achieve the high performance of the original implementation but now with a much greater confidence in its correctness. In so doing, layers may be combined and other optimizations applied. However, we do not ``throw away'' the reference implementation when this process is complete because it continues to be useful as documentation and as a specification of the system, as well as a vehicle for further verification and prototyping.
The continued use of production versions of layers is a concession to the performance requirements of demanding applications. However some applications seek the utmost in reliability, at least with respect to properties such as security. For this reason, another important goal for Horus reference layers is that they be interoperable and interchangeable with the production layers. We have constructed an interface between Horus and ML so that reference and production layers can be mixed freely in a protocol stack. Such an interface is possible only because of the HCPI, to which all layers adhere.
Our approach would permit a fully verified reference layer that implements a security protocol to be inserted into a production Horus protocol stack, even though one is implemented in ML and the others are in C. Interchangeability both encourages and enforces a tight coupling between the reference and production implementations of layers. For instance, a production layer should be replaceable in a protocol stack by its corresponding reference layer and vice versa. Interoperability allows us to take advantage of the existing production version and follow an incremental approach so that ``hardening'' of key components can be tackled first and non-essential pieces left for later. Also, new protocol layers can be rapidly prototyped in ML, tested with a normal Horus protocol stack, and then translated to C if performance is an issue. In addition to protocol layers, distributed applications can also be written in ML using the interface.
Initial experience shows that the goals we have set for a reference implementation of Horus can be reached. We have built reference implementations for several protocol layers. These are considerably cleaner than the current production layers and are generally an order of magnitude smaller in code size. We believe we will be able to completely implement the core of Horus in a few thousand lines of ML (compared to 40-50,000 lines of C) for the purpose of verification. In addition, the implementation of reference layers has led to several improvements in the basic Horus architecture, some of which may result in improved performance when translated back to the production layers.
We have only begun to explore the issues that arise in actually proving that a layer satisfies its specification, and that a set of specifications can be combined to implement a desired property-for example, that layers can be composed, in the formal sense. Our initial work on this problem uses I/O automata (similar to the model expounded by Nancy Lynch et al. [6], with certain modifications suitable to the Horus architecture) to model the protocol executed by a Horus layer. Important properties provided by the layer can then be verified by combining this I/O automaton with other I/O automata representing all the layers above and below it. The composition of these automata (itself an automaton) is a closed system, which we augment with additional properties (such as fairness) expressed in simple temporal logic formulas over states and actions. We then prove that, within this system, the layer honors a specified set of user requirements. A similar technique will allow us to verify that desirable properties of a given protocol stack will be preserved by the addition of a new layer, and to help decide when the stacking order of two layers matters.