📊 Model: (InformationFlow-DistanceTracker-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 a user that wants to track running statistics by an external service.

🔤 Abbreviations

None.

📖 Extensive Description

The User sends his/her location to a Distance Tracker service that stores locations in the Location Store and derives the run distance. This happens with the consent of the User Afterwards, this service transmits the distance to a Tracking Service.

🏷️ Label Description

🗂️ Data Labels:

• ClassificationLevel: These are classified as either User, UserTrackingService, and OnlyDistance, depending on which area the data flow is allowed to flow through.

🏷️ Node Labels:

• ClearanceLevel: These are the same as the data labels. User, UserTrackingService, and OnlyDistance denote which ClassificationLevel is allowed to flow through a given node.

⚠️ Constraint

DistanceConstraint

This constraint ensures that no data flow passes a node it does not have the corresponding ClassificationLevel for.

• DistanceConstraint: ClassificationLevel.UserTrackingService neverFlows vertex ClearanceLevel.OnlyDistance

🚨 Violations

None.