Reasoning About Active Network Protocols
Samrat Bhattacharjee
Kenneth L. Calvert
Ellen W. Zegura
Active networks provide a platform that allow users to program the network by injecting algorithm to be executed for the user by the network. This enables the network services to be customized on a per-user basis. Many contemporary research activities in this area, like SwitchWare network architecture, PLANet, ANTS etc., have concentrated their effort in implementing the active network platform in various ways. But they have not attempted to reason the correctness of the distributed algorithm that would be executed at the network nodes.
This paper supports reasoning independently about the correctness of the active network platform and the algorithms injected into it without relying on any particular formalism. In this sense this paper is a pioneering effort.
Active Node Model
The authors consider each active node’s behavior as being made up of two components, an underlying program which defines a “virtual machine” and is the same for every packet and an injected program which is defined by the user, running on the virtual machine. The nature of the virtual machine defined by the underlying program is a key issue in the design of an active network node.
If the underlying program defines a Turing-complete interpreter then the node behavior is determined completely by the injected program, thus making the task of reasoning about the global network behavior a difficult one. On the other hand, if the underlying program defines a fixed computation, reasoning becomes easy but flexibility is lost. The authors have taken a middle-of-the-road approach that tries to strike a proper balance between the task of reasoning and retaining the flexibility of the interface presented to the user.
Slot-Based Programming Model
To reason about the global correctness of the interface between the underlying program and the injected program, the authors have proposed the following model. This interface takes the form of one or more slots. The program injected by the users bind to particular users specified by the user. The underlying program invokes the code bound to each slot at some point during its execution based on some semantics; this is referred to as raising a slot. Once a slot is raised, the underlying program suspends and the injected program runs until completion.
The approach taken by the authors here is to reason about the correctness of the underlying and the injected program in isolation, and thereby proving the correctness of their interaction. In other words, the active network’s global behavior maintains certain correctness properties provided the injected programs satisfy certain restrictions.
The fact that the model is fairly simple and is devoid of any formalism is noteworthy. For any research in its nascent stages, it is always wiser to start with a simple model and refine it later. This approach is especially suitable for solving a complex problem like this.
The use of the model is illustrated via an example dealing with mobility based on the UNITY formalism.
Future Work
While the approach taken in this paper makes it possible to reason about the correctness of the global behavior, the problem that has been considered is simplistic compared to the actual problem to be solved. As the authors have noted in the paper the scope of the problem can be widened by considering the following issues:
Ø Reasoning about the injection process – How the program is injected into the network by the user and how it propagates through the network to an active node
Ø Security, Scalability, Resource management etc., - The model proposed assumes a single network user. The above issues need to be considered when many users are taken into account.
Ø Heterogenous active nodes – The paper assumes that all active nodes provide the same interface. A more realistic model should take into account active nodes which provide different interface.
Though the paper considers a simple problem, being first of its kind, we feel it is a step in the right direction.