The importance of security in computer and information systems is increasing as network-connected computer systems become more ubiquitous. The objective of security is to verify that the computing platform is secured and that data and information are properly accessed and handled by users and applications, ensuring data confidentiality and integrity. To develop a framework for modeling and verifying security as a data quality attribute, designers need to identify parameters and variables with the express power to capture and represent security models and determine the type of analysis to enable.

This post, which is excerpted from a recently published report, presents an approach for modeling and validating confidentiality based on the Bell–LaPadula security model using the Architecture Analysis and Design Language (AADL). It also presents 11 analysis rules that must be enforced over an AADL instance model to ensure the consistency of a security model. Mapping Bell-LaPadula to AADL allows the expression of key concepts within the AADL Model so they can be analyzed automatically.

The Bell–LaPadula Security Model

The Bell–LaPadula security model is a mathematical framework and model for designing secure computer system architectures. In particular, it regulates the dynamic behavior of a system as “subjects” with differing privileges to read from and write to “objects” with different access restrictions. Systems based on this model must enforce two properties:

1. the simple security property that prevents subjects from reading objects without authorization; and
2. the star property that prevents sensitive data from being written to insecure objects.

A system in conformance with the model never allows a subject to access an object that it is not permitted to and never allows the subject to manipulate an object in nonpermitted ways.

Our approach to mapping the concepts from the Bell–LaPadula security model to architectural models written in AADL is described in three steps:

1. our use of the AADL property mechanism to define security labels
2. our mapping of subjects and objects to AADL language features
3. how this mapping affects Bell–LaPadula access modes

Our approach builds upon earlier work, as we describe below.

Security Labels in AADL

The security label of subjects and objects consists of a security level value and a set of categories. The level value is drawn from a totally ordered set and denotes how securely an object must be handled and how privileged a subject is. Categories further refine the security level by labeling objects and giving subjects permission to access appropriately labeled objects.

We use AADL property associations to add security labels to AADL components and features that represent subjects and objects. We use a pair of properties to associate both a level and a list of categories with each subject/object. The declarations of the properties Level and Level_Caveats that declare an item’s security level and set of categories, respectively, are shown below:

Subjects and Objects in AADL

In the Bell–LaPadula model, active subjects act on passive objects. In AADL, components communicate through ports and other categories of features. For the most part, data is not explicitly represented in the model, although data subcomponents can be shared with other components via data access features. Instead, data port and other features belonging to components are connected to describe the transfer of information throughout the modeled system. A feature is thus a proxy for the data that pass through it. These observations motivate us to consider AADL components as subjects and AADL features as objects.

Access Modes in AADL

The Bell–LaPadula model defines four access modes to describe a subject’s effects on an object:

1. Execute access does not permit the subject to observe or alter the contents of the object.
2. Read access permits a subject to observe but not alter the contents of the object.
3. Append access permits a subject to alter but not observe the contents of the object.
4. Write access permits a subject both to alter and observe the contents of the object.
   

Given our mapping of objects to AADL features and data components, we must derive access rights based on the AADL semantics for those features. Considering that AADL is not executable, this exercise may appear purely theoretical. We need to understand these access modes, however, so we can properly enforce the simple security property and star property of the Bell–LaPadula model.

Consider the simple system shown in AADL graphical notation below. It has two producer systems, a computation system, and a consumer system. The diagram shows the four subsystems, their ports, the connections between them, and the flows through them. The data ports are labeled with their associated data classifiers to enhance the traceability of the security labels that are declared in the AADL textual representation of the data types below. The system includes flow specifications so that the star property can be enforced. (See below).

This example is intentionally straightforward to demonstrate the basic ideas of modeling security in AADL. In particular, the example demonstrates the following:

• Data ports receive their security attributes from their data classifier.
• Event ports receive their security attributes from their local property associations.
• Implementations inherit security attributes from their type.
• Security attributes are applied hierarchically, at each layer of the system.

This example uses the security categories A, B, and C. Thus, we assume that the property type Security_Type_Specifications::Caveat_Type has been declared as

Caveat_Type: type enumeration (A, B, C);

The declarations for data types X, Y, and Z are shown below and contain the security property associations necessary to mark them as having the security labels (confidential, {A}), (confidential, {B}), and (confidential, {A, B}), respectively.

Analysis and Validation in AADL

The Bell–LaPadula model requires that security labels of subjects and objects in a system are consistent with the simple security property and the star property. In addition, the semantics of AADL require that several additional properties be enforced for the security modeling to make sense. The remainder of this post details 11 analysis rules that must be enforced over an AADL instance model to ensure the consistency of a security model.

Checking the Simple Security Property

The simple security property enforces the expectation that a subject should access only objects that it is allowed to use. Specifically, it requires that the maximum security label of a subject dominates the security label of each object that it accesses. In AADL, a component declares all its data accesses as explicit features. To check the simple security property, therefore, we need to enforce the following rule:

Rule 1 (Simple Security Property for Components) The security label of each component must dominate the security label of each feature in the component.

Feature groups do not require special treatment with respect to this rule due to the requirement that the security label of a feature group must dominate the security labels of its features. If the security label of a component dominates the security label of a feature group, it must also dominate the security labels of the feature group’s features; otherwise, there will be errors reported on the feature group’s features. We now recast this previous architectural rule as an additional analysis rule:

Rule 2 (Simple Security Property for Feature Groups) The security label of each feature group must dominate the security labels of each feature in the feature group.

We also require a rule for enforcing the simple security property on subcomponents:

Rule 3 (Simple Security Property for Subcomponents) The security label of each component must dominate the security label of each subcomponent in the component.

This rule has no direct analog in the Bell–LaPadula security model because the model does not consider a hierarchical relationship among subjects. The rationale for this check in the case of non-data components is that a subcomponent performs work for—as part of—its containing component. Its container, therefore, must be authorized to access the data that the subcomponent may access. A data subcomponent exists in one of two scenarios:

1. As a subcomponent of a non-data subcomponent. In this case, the sub component is data, an object accessed by the containing subject, and the above rule is a direct application of the simple security property.
   
2. As a subcomponent of a data subcomponent. The subcomponent represents a portion of the overall data component. Therefore, the containing data component must have a security level at least as great as that of the subcomponent

Checking Subprogram Calls

Subprogram subcomponents are not subjects and are instantiated as part of an AADL call sequence. As the name implies, a call sequence describes a sequence of subprogram invocations. Call sequences may appear only in subprogram and thread components; the AADL standard specifies which component executes any given sub-program call within a sequence. (See Section 5.2, Paragraph 19 in the AADL standard for additional details.) In short, depending on how the subprogram is (1) declared in the model and (2) referenced in the call sequence, the subprogram may be executed by one of the following components:

the calling thread

the called thread (i.e., a remote procedure call)

the providing device

the providing processor

This yields the following rule:

Rule 4 (Simple Security Property for Subprogram Calls) The security label of a feature in a subprogram call must be dominated by the security label of the component that executes the subprogram.

This rule is now of no practical importance because the current AADL tool sets do not actually instantiate call sequences.

Software-Hardware Bindings

AADL components can be divided into software components, such as thread, data, and process, and hardware components, such as bus, memory, and processor. In a completely instantiated and bound model (see section 13.1, Paragraph 3 of the AADL Model), the software components must be bound to hardware components. This binding is specified via property associations on the software components. The full details are described in sections 11 and 11.2 of the book Model-Based Systems Engineering by Peter Feiler and David Gluch.

The basic intent of this approach is that threads are bound to processors, data is bound to memory, and connections are bound to buses, although more complicated bindings are possible. Of particular note is that data port and event data port features should be bound to a memory component that indicates where the actual data flowing through that port is stored. This software–hardware binding is analogous to the subcomponent hierarchy discussed above for several reasons:

• A processor executes a thread, so it must be authorized to access the data (that is, objects) that the thread needs to access.
• Memory must be authorized to store the actual data that is bound to it, which leads to the following rule:

Rule 5 (Simple Security Property for Binding) If a component c or feature f is bound to a component t, the security label of t must dominate the security label of c or f.

If multiple components or features are bound to the same hardware component, its security label must dominate all their security labels.

Connections are interesting in this context because they act like objects, excepting bus access and virtual bus access connections. The data passing through the connection must be accessible to all components to which the connection is bound. The security label of the data comes from the connection end points, which yields the following rule:

Rule 6 (Simple Security Property for Bound Connection) If a connection c is bound to a component t, the security label of t must dominate the security label of c’s data.

Checking the Star Property

The star property enforces the expectation that a subject should not be able to leak classified information by reading data from a high-level object and then writing that information into a low-level object. Fundamental to the star property is that if a subject has simultaneous “observe” access to one object and “alter” access to another object, the security label of the alterable object must dominate the security label of the observable object. The intent behind the star property is that data should not flow from a high-level object to a low-level object. An AADL flow path specification explicitly declares that data arriving at the source feature flows to (or otherwise influences) the data written to the destination feature. The natural way to check the star property via flows is to check that the security label of the feature that is the flow source is dominated by the security label of the feature that is the flow sink.

The Bell–LaPadula model is traditionally considered to use an access control model of security. However, this approach to checking the star property actually makes our security analysis implementation an information flow model that operates on the semantics of AADL, rather than of a lower level programming language. The following rule summarizes the discussion above:

Rule 7 (Star Property for Flows) For each flow path in a component, the security level of the destination feature/component must dominate the security level of the source feature/component.

There is no need to check flow sink and flow source specifications; they do not denote a path from one feature to another. It is worth noting that a feature group feature that appears as an end point of a flow path does not require special treatment. As features, they must have security labels.

Checking Architectural Consistency

We must perform several additional checks on a model to ensure its security attributes are consistent with AADL-specific structures. In our modeling approach, we prefer the security label of a feature is specified by the property associations of the feature’s data classifier. This approach is not always possible, however, so sometimes the property associations on the feature itself must be used.

AADL semantics dictate that the property associations on the feature take precedence (see section 11.3, Paragraph 12 of the AADL Model). Our approach therefore becomes confusing when security-label property associations are present on both the feature and the feature’s classifier. Such a situation conflicts with our desire that the feature’s classifier be the sole descriptor of the data. The following rule clarifies this situation:

Rule 8 (Feature–Classifier Label Equality) If both a feature and the feature’s classifier have security-label property associations, the two security labels must be equal.

Connections

We must check that the security label of the source of a connection is equal to the security label of the destination of a connection. This check is necessary because the AADL feature (or data component) that is the connection destination represents the same data object as the AADL feature (or data subcomponent) that is the connection source. If the end points were allowed to have different security labels, we would be saying that a single data object could simultaneously have two different security labels.

Ideally, all ports in the AADL model would have a data classifier specified and these would be identical at the source and destination of a connection, due to AADL semantics. The identical classifiers would obviously have identical security labels, so an explicit rule for checking the connection labels would be necessary. There are, however, many reasons in AADL why expectation may not be met, and the security label would be obtained from the feature instead of the feature’s data classifier, and thus an explicit rule is required.

In addition, in an AADL instance model, “a connection instance is created from the ultimate source to the ultimate destination component by following a sequence of connection declarations” (See Section 9, Paragraph 2 of the AADL standard.). The destination of an individual connection declaration therefore becomes the source of the next individual connection declaration, so all the features must have identical security labels. This discussion is summarized as the following rule:

Rule 9 (Connection Label Equality) The security label of the source feature of a connection must be identical to the security label of the destination feature of a connection. The security labels of the source and destination features of all the individual connection declarations of a connection instance must be identical.

Least Privilege

A component should not have a higher security label than it needs to access the data that it manipulates. There is no advantage to a properly functioning component to have a higher security label than necessary. By minimizing the security label of a component, we minimize the risk that the component will manipulate data irrelevant to its task. We therefore recommend that each component be checked to ensure that it has the least privilege it needs to do its job. This guideline relates to the principle of “need to know.”

Rule 10 (Least Privilege) The security label of a feature group type should be the least upper bound of the security labels of its features. The security label of a component type should be the least upper bound of the security labels of its features. The security label of a component implementation should the least upper bound of the security labels of its features, subcomponents, and subprogram calls.

Sanitizing Information

The purpose of enforcing a security model on a system is to prevent information that should be kept secret from being released to those who cannot be trusted to see it. In the Bell–LaPadula model, the star property is central to achieving this goal: It prevents secret information from being written into non-secret containers. In other words, data can only become more secure.

Of course, in the real world, this approach is too limiting. Systems must be allowed to contain trusted subjects that perform the following practical behaviors:

• derive less secret data from secret data and pass that derived data to other less-than-fully-trusted systems
• pass secrets over public communication channels

We accommodate sanitization in the model through the concept of the sanitized flow: a flow path whose output feature derives a portion of its output from an input feature whose security label is not dominated by the security label of the output feature. In other words, a sanitized flow is not checked against the star property. The implication is that the data is manipulated in some way that allows the lowering of its security label (e.g., the data is encrypted, degraded, obfuscated, aggregated, or inherently low-level data that is extracted from surrounding high-level data).

By modeling sanitization, we can determine that it is performed within the capabilities of a trusted subject. Sanitization represents an exception to the security rules, so it should be used cautiously and infrequently. The purpose of a sanitized flow in an AADL model is to mark those places in the system architecture where sanitization may occur so that the sanitization may receive the extra scrutiny that it deserves. Our analysis does not attempt to determine whether the sanitization is performed correctly.

The primary purpose of marking a flow as sanitized is to exempt its destination port from the star property, as described in the following rule:

Rule 11 (Sanitized Flow) When a flow path is sanitized, analysis does not check whether the security label of its destination dominates the security label of its source.

The destination of a sanitized flow must still respect the simple security property: The sanitizing activity must still be within the capabilities of the component.

Automatic Analysis of Validation of Security

The techniques described in the report from which this post is excerpted demonstrate how model-based engineering can support early modeling and validation of security. The report also includes examples and case studies modeled in AADL.

Specifically, using the AADL, we have specified common and well-defined security attributes and represented them in AADL models primarily based on the Bell-LaPadula model. Mapping Bell-LaPadula to AADL allows the expression of these attributes within the AADL model, thereby enabling automated analysis.

An implementation of the analysis within the open-source OSATE AADL toolset is forthcoming. A link will be added to this blog posting when it is available.