xDECAF 😆☕

Appearance

📊 Model: (AccessControl-DistanceTracker-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: ​

  • AccessRights: These are classified as either User, TrackingService, and DistanceTracker, depending on which area the data flow is allowed to flow through.

🏷️ Node Labels: ​

  • Roles: These are the same as the data labels. User, TrackingService and DistanceTracker are the three parts of the model. Each node is part of exactly one of these.

⚠️ Constraint ​

DistanceTrackerSecurity ​

This constraint ensures that no data flow passes a node it does not have the corresponding label (and access right) for.

  • DistanceTrackerSecurity: !AccessRights.DistanceTracker neverFlows vertex Roles.DistanceTracker

🚨 Violations ​

The error introduced in the case is that the calculated distance can bypass the declassification process (confirm_distance), which implies a higher classification level.