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

This case is about a file system for pictures in a family.

🔤 Abbreviations

None.

📖 Extensive Description

There are three family users that use a store Family Pictures. The Mother and Dad can add_pictures and read_pictures. The Aunt can only read_pictures. An Indexing Bot might discover the file sharing system but must not access it.

🏷️ Label Description

🗂️ Data Labels:

• TraversedNodes: Each node visited by a certain data flow adds its own tag. This can be addPicture, pictureStorage, readPicture, mother, dad, aunt and indexingBot.

🏷️ Node Labels:

• Identity: This node describes a certain user. There are Mother, Dad, Aunt and IndexingBot.
• Owner: Mother is the owner of the data store.
• Read: Designates the right to read from the data store. Mother, Dad, Aunt may read from it.

⚠️ Constraints

Isolation

The Indexing Bot is not allowed to read or access Family Pictures in any way.

• Isolation: data !Read.IndexingBot neverFlows vertex Identity.IndexingBot

🚨 Violations

None.