Using Rapide tools to extract information from architectures

Sigurd Meldal (meldal@poset.stanford.edu)

This is a Work-in-progress. Watch this spot for updates

NSA's Multilevel Systems Security Initiative (MISSI) defines a reference architecture for secure systems. It gives a prose specification of both structural and operational features of the architecture, and offers a good opportunity for testing the adequacy of architecture definition languages. This example shows 1) how Rapide can be used to capture key elements of the architecture specification, making them precise and identifying ambiguities in the prose, and 2) how the Rapide tools can be used to analyze models of architecture instances, identifying the consequences (both in terms of security and performance) of design choices, and through run-time checking reporting any violations of the constraints that might occur. As a prototyping language for distributed systems, the executable modeling features of Rapide create richly instrumented models, making them a good foundation for analysis and checking.

The Rapide toolset offers a number of ways to investigate the properties of an architecture or model, such as animating a simulation using Raptor or by inspecting the result of an execution, using the Partial Order Browser ("POB").

Rapide has been used to capture key elements of NSA's MISSI reference architecture for secure, distributed systems. For the purposes of this summary presentation of some of Rapide's capabilities, it suffices to know that a particular instance of this reference architecture may consist of a number of enclaves connected through a wide area network, and that each enclave might be a subarchitecture consisting of one or more firewalls (connecting it to the WAN), a number of workstations and sundry services (certificate authorities etc.). For a more MISSI-specific set of examples, go to the missi specification elements. In Rapide the top-level architecture instance might be described simply as

architecture missi(num_enclaves : Natural) is
    internet :   WAN;
    enclaves :   array[integer] of Enclave;
connect
--  connect Firewalls to the WAN     //
    for i : integer in 1..num_enclaves
    generate
        internet.enclave_conn
        to
        enclaves[i].wan_conn;
    end;
constraint
    -- All messages which emanate from the sites are non-secret in
    -- nature by the time they hit the WAN
    never (?data in Data)
        enclave::wan_conn.to_net(?data)
               where (?data.security_classification /= unclassified);
end;

This reference architecture declaration consist of an array of enclaves (the size of which is determined by the parameter), a WAN, and an assertion that each enclave is connected to the WAN.

The definition makes use of a number of types declared elsewhere - enclaves, wans and probably most interestingly - the connection elements of enclaves and wans. Thus the simple assertion that each enclave is connected to the internet actually may hide quite a bit of structure: the more detailed access points an internet connection consists of, and the specification of the protocols that constrain the interaction between the internet and the enclaves.

At the end of the architecture specification we find a very simple constraint which asserts that no messages with classified data will be transmitted to the WAN by an enclave.

The architecture can be very simply depicted in Raptor as a set of connected boxes (in this instance, the number of enclaves is four):

Each of the enclaves might itself have a subarchitecture structure. Thus, opening up one of the enclaves (by clicking on it) we see that it consists of a firewall, two workstations with their respective users, and a LAN:

Executing this architecture as a model results in a rich treasure of information - about timing properties, about dependencies, about violations of the constraints of the model.

The semantic model of Rapide is based on events, and the result of a Rapide simulation is primarily a set of events with related information.

Even a small model will generate large numbers of events, and one of the immediate uses of the tools is to pare all this information down to a manageable size (all the pictures in this presentation are screenshots from actual uses of the tools). Faced with the bewildering set of events:

one can approach it in various ways. We might for instance be interested in identifying the communication path from one user to another. By first identifying the events representing communications to a user from her workstation (highlighted in red below), we can inspect an event more closely by clicking on it, with a window popping up which gives more detailed information about the event (in this case, the event represents a communication from workstation #79 to user #110. In principle we could investigate it further, checking what data the message carried, etc.).

If we were interested in how this message came into being, we could reduce the partial order of events to those that causally preceded the workstation-to-user communication. The result presents only those events that actually led up to the message being delivered to the user. It removes events that are not part of the causal chain resulting in the delivery, including those that may precede the delivery in time without being causal precursors of the event of interest.

The result is a rather small set of events, and with the partial order browser showing the names of the events the presentation is easily understood:

There are a couple of notable points in this picture:

There are two kinds of arrows between events: unidirectional and bidirectional ones.
- The unidirectional arrows represent causal dependency , in the sense that the event at the tail of the arrow must happen in order for the event at the head of the arrow to happen. Causal dependency is transitive, so an event which is a causal precursor to another event which then is a causal precursor of yet other events is a causal precursor to all of these.
  So, since there is a series of arrows from the first sw_conn.to_node to the last user_conn.to_user we find that the activity represented by the event user_conn.to_user is dependent upon the activity represented by sw_conn.to_node.
- The bidirectional arrows identify equivalent events, i.e. events that are causally indistinguishable. A set of equivalent events (such as the pair of net_conn.to_net and ws_conn.to_net) identify different views of a single activity. The event net_conn.to_net represents the communication of a message to the net from a workstation as "seen" from teh net, and the event ws_conn.to_net represents the same communication, but stated in terms of the features of the workstation. Since the workstation-to-net communication is synchronous, these two events are causally identical. Similarly, the set of three events, ws_conn.to_node (representing the receipt of a message from the net by a workstation) and the two net_conn.to_node events (representing the broadcast of a message by the net) are causally identical also.
  A causal precursor to any one event among a set of equivalent events is a precursor to all the equivalent events. And similarly, if any one event in a set of equivalent events is a causal precursor of some event, then all the equivalent events are causal precursors of that event.
  Thus, since the early events user_conn.to_node and ws_conn.to_node are equivalent, as are the later events user_conn.to_user and ws_conn.to_user, and there is a causal relationship between ws_conn.to_node and user_conn.to_user, we have that the final ws_conn.to_user is dependent upon the earlier user_conn.to_node (confirming our expectations).
Following the high-lighted events we see the communication path from the user initiating the message transmission all the way to the user at the other end receiving it. The high-lighted events focus on the performer of the respective events (i.e., the user connecting to the workstation, the workstation connecting to the net, and so on). Note, though the bidirectional arrows
We can also determine from the causal dependencies that the network sends the message to the firewall before broadcasting it locally within the enclave - i.e. that the connection to the firewall is distinct from the general broadcast on the enclave's LAN. Since the sending and receiving workstations are both local to the enclave itself (there are a number of ways we can deduce this from this event graph) there is no reason why the connection to the firewall should be necessary in order to get the message to the local, receiving workstation.
In other words, the partial order browser can be used to identify unwarranted dependencies and possible bottlenecks in an execution. And similarly, it can be used to identify race conditions, where required synchronization has been omitted for some reason or another.

The partial order browser can also be used to identify violations of constraints stated in the architecture specification, and to identify their causes. In our example architecture there is a simple constraint - that no unclassified information be transmitted onto the WAN. If we let the partial order browser high-light occurrences of violation events, we find that there are a number of them (in red):

By clicking on one of them, we find the immediate diagnosis of the violation, that there is "Classified information on WAN".

By letting the partial order browser identify all the causal precursors of one of the violations, we can identify the offending event and enclave (firewall #164), and by following the causal chains backwards (arrows high-lighted in orange) we see that the offending message was from user #176 (and it was created with the help of confidentiality server #194).

This pattern of misbehavior was quite simple, and determining its cause almost trivial. However, since Rapide's constraint language can give specifications in terms of patterns of events, it can be used to identify violations of protocols and other, more complex constraints, and to pin-point causes of such violations.

Using Rapide tools to extract information from architectures

Sigurd Meldal (meldal@poset.stanford.edu)

To be continued