For a given application that is to be installed over a network with a given set of properties, one needs to find a stack of protocols that will provide the properties the application requires in that environment. We need a formal way to describe what a layer requires from the layers above and below it, and what it guarantees in return. A second issue is to create a reference implementation of each layer to formally describe the algorithm that implements the layer's specification.
As a step towards this methodology, we have begun compiling sets of properties provided by and required by layers (see Table 4). Table 3 lists, for each of a selected set of protocol layers, which properties it requires, and which it implements. In addition, a layer may or may not pass a property through to the layer above it. We call this inheritance. Given this table, it is possible to figure out if a stack is well-formed, and what properties a well-formed stack provides. A stack is well-formed if, for each layer, all its required properties are guaranteed by the stack underneath it. The properties are either provided by the layer immediately below, or inherited from an even lower layer. Vice versa, given a set of network properties and required properties for an application, it is possible to figure out if a stack exists that can implement the requirements. If we can associate a cost with each of the properties, possibly on a per-layer basis, we can even create a minimal stack. Rather than looking at this as stacking protocols on top of each other, a different interpretation is that Horus actually builds a single protocol for the particular application on the fly.
: This table lists, for each of a selection of Horus protocols,
the requirements on the communication underneath the protocol,
the properties that are inherited from that communication,
and the properties that are provided by the protocol (see Table 4 for the list of properties).
We note the similarity between this methodology and an approach that is commonly used when developing real-time systems. In a real-time system, an application requests timing properties. The system will try to reserve the necessary resources to guarantee these properties. If successful, the application is started. If not, an error is returned to the user. Horus can generalize this idea: an application requests a set of properties first, and then Horus can figure out if it can guarantee this properties.
We are currently working on designing formal methods, so that on a per layer basis we can verify that given a set of underlying properties, it provides a new set of properties. We are also interested in verifying whether a layer leaves certain properties untouched (inheritance). We discuss our preliminary efforts in this direction in Section 8.
