📊 Model: (AccessControl-MAC-no-violation)

Available Online

This model is available to view using the online editor!

Open In Online Editor

🔗 Link to Original Paper/Article

View SourceOpen Example Model in Example Models Bundle

📝 Short Description

The case is about an airspace monitoring system for civil and military planes.

🔤 Abbreviations

None.

📖 Extensive Description

There are three types of users. A Clerk creates and stores weather reports. A Flight Controller registers civil airplanes, finds their positions and determines new routes based on other plane positions and the weather reports of the clerk. The Military Flight Controller performs the same tasks for military airplanes and also considers the positions of civil airplanes. Weather Data is provided by a Clerk and, as it is Unclassified Data, supplied a weather report to other processes.

🏷️ Label Description

🗂️ Data Labels:

• ClassificationLevel: There are three classification levels for a data flow. These are the same as the clearance levels for nodes. A data flow may not traverse a node it for which it does not have the needed classification level.

🏷️ Node Labels:

• ClearanceLevel: There are three clearance levels. These are, in descending heirarchy: Secret, Classified, Unclassified. Each following level is a subset of the preceding level(s).

⚠️ Constraints

SecretConstraint

This constraint ensures that data designated Secret does not flow to nodes with clearance level Classified:

• SecretConstraint: data ClassificationLevel.Secret neverFlows vertex ClearanceLevel.Classified

ClassifiedConstraint

This constraint ensures that data designated Classified does not flow to nodes with clearance level Unclassified:

• ClassifiedConstraint: data ClassificationLevel.Classified neverFlows vertex ClearanceLevel.Unclassified

🚨 Violations

None.