Hello! My company is implementing a permissions-based filesystem, and the reason I joined this forum and learned Alloy was to see if I could use it to stress-test our permissions model. This project turned out to be wildly successful. I found several major but non-obvious holes in our model, and we’re now building it on a much more solid foundation.
The rules of our flawed permissions model:
- For each File or Folder, an administrator can assign an access level (Use, Edit, or Own) to a Group.
- If the admin doesn’t explicitly assign an access level to a File or Folder, then that File or Folder’s access level will be inherited from the nearest ancestor that does have an explicit access level set.
- A User can be a member of multiple Groups, and the User’s permissions for each File will be the max of each Group’s permissions for that File.
- If a User has Own access to a File or Folder, they can move it to a different Folder that they also have Own access to.
This model seemed sound to us, but Alloy shows that there are tricky scenarios where users can move folders to give themselves access to files they couldn’t access before. There are also tricky scenarios where users can lose access to files. This is a system where you can move a file that you own, into a folder that you own… and as a result, somehow, you’ll no longer own the file and can’t move it back!
- To see how users can move folders around to give themselves access they didn’t originally have, run
user_cannot_gain_or_lose_accessand see the failure. - Next, uncomment the code below
// User must also own all of the source object's childrenin themove_objectpredicate. This represents a patch we made to prevent users from gaining access. But users can still lose access! Runuser_cannot_gain_or_lose_accessagain to see how. - Finally, run
user_cannot_gain_or_lose_access_if_children_have_greater_explicit_perms_than_parents. Here, we ask what happens if each child file or folder must always have an access level greater than or equal to that of its parent. This results in a model where users cannot gain or lose access by moving things around.
I’m planning on polishing this story up for public consumption, and hopefully getting more people interested in Alloy. If you have any tips on how to make this spec shine, let me know!
/**
* Model representing a permissions-based filesystem.
*
* It has these facts, which are true today:
*
* 1. There are pages and folders arranged in a tree.
* 2. A User can have many Groups, and a Group can have many Users.
* 3. There are four levels of access, in decreasing order of strength:
* Own, Edit, Use, and None.
* 4. A user's level of access to an object is the max of their group's levels
* of access.
* 5. A group's level of access to an object is the permission it was
* explicitly granted, either to that object or to its nearest ancestor
* with an explicit grant.
* 6. A user can move any page that they Own.
*
* And we are thinking of adding this fact:
*
* 7. A user can also move any folder that they Own.
*
* There's a property that I think is pretty important in a permissions system:
*
* 1. If a user does not have access to an object, they can never give
* themselves access to the object just by moving objects around.
*
* This spec shows that this property **no longer** holds when we give users
* the ability to move Folders.
*/
// There is always exactly one RootFolder
one sig RootFolder {
}
// Each Object has a parent Folder
abstract sig Object {
var parent: one (Folder + RootFolder)
}
// There are two kinds of Object: Page and Folder
sig Page, Folder extends Object {
}
fact all_objects_connected_to_tree {
always {
all object: Object {
RootFolder in object.*parent
}
}
}
fact tree_is_acyclic {
always {
no folder: Folder {
folder in folder.^parent
}
}
}
abstract sig Perm {
includes: lone Perm
}
one sig Own, Edit, Use, None extends Perm {
}
/**
* If you own an object, you can edit it. If you can edit it, you can use it.
*/
fact permission_rankings {
Own.includes = Edit
Edit.includes = Use
Use.includes = None
None.includes = none
}
// For now, we use only one User. Maybe we can have more, but I'm not sure what
// properties we care about when multiple users are involved.
one sig User {
// A User can be a member of multiple Groups
groups: set Group,
var implicit: Perm -> Object,
} {
always {
all perm: Perm, object: Object |
user_implicit[perm, object] <=> object in implicit[perm]
}
}
sig Group {
// The Objects this Group was explicitly granted permissions for
explicit: Perm -> Object,
} {
// You can only specify one setting for a Group/Object combination
disj [explicit[Own], explicit[Edit], explicit[Use], explicit[None]]
}
/**
* True if `group` implicitly grants `needed_perm` to `object`, based on the
* directory structure of `object`.
*/
pred group_implicit[needed_perm: Perm, group: Group, object: Object] {
some group_perm: Perm, ancestor_folder: object.*parent | {
// True if the group has explicit permission for some ancestor folder
ancestor_folder in group.explicit[group_perm]
// and this permission is at least as strong as the permission we need
needed_perm in group_perm.*includes
// And also there is no middle folder, in between us and that ancestor,
// which has a weaker explicit permission
no
middle_folder: (object.*parent - ancestor_folder.*parent),
weaker_perm: Perm
{
needed_perm not in weaker_perm.includes
middle_folder in group.explicit[weaker_perm]
}
}
}
pred user_implicit[needed_perm: Perm, object: Object] {
// A user has implicit permission on an object if any of its groups have
// that implicit permission
some group: User.groups | group_implicit[needed_perm, group, object]
}
pred move_object[
source_object: Object,
target_folder: Folder + RootFolder
] {
// User must own the source object
user_implicit[Own, source_object]
// User must own the target folder
user_implicit[Own, target_folder]
// Object must not be a parent of the folder you're moving it into
not source_object in target_folder.*parent
// Object's parent becomes the target folder
source_object.parent' = target_folder
// All other parents stay unchanged
all object: Object - source_object | object.parent' = object.parent
}
fact users_can_move_objects {
always {
one
source_object: Object,
target_folder: Folder + RootFolder
| move_object[source_object, target_folder]
}
}
run {
} for 3 Object, 2 Group, 2 steps
/**
* True if a user never gains access to an app
*/
check user_cannot_gain_access {
all missing_perm: Perm, inaccessible_object: Object |
not user_implicit[missing_perm, inaccessible_object] =>
always not user_implicit[missing_perm, inaccessible_object]
} for 3 Object, 2 Group, 2 steps
/**
* True if the user never gains or loses access to an app
*/
pred user_cannot_gain_or_lose_access {
all missing_perm: Perm, inaccessible_object: Object |
user_implicit[missing_perm, inaccessible_object] <=>
always user_implicit[missing_perm, inaccessible_object]
}
check user_cannot_gain_or_lose_access {
user_cannot_gain_or_lose_access
} for 3 Object, 2 Group, 2 steps
check user_cannot_gain_or_lose_access_if_only_one_group {
user_cannot_gain_or_lose_access
} for 3 Object, 1 Group, 2 steps
/**
* True if a folder never has a parent other than the root.
*/
pred subfolders_not_shipped {
always {
all object: Folder | object.parent = RootFolder
}
}
check user_cannot_gain_or_lose_access_without_subfolders {
subfolders_not_shipped => user_cannot_gain_or_lose_access
} for 3 Object, 2 Group, 2 steps
/**
* True if a subfolder always has greater explicit permissions than its parents
*/
pred children_have_greater_perms_than_parent {
all
group: Group,
child_perm: Perm,
child: group.explicit[child_perm],
ancestor: child.^parent - RootFolder |
some ancestor_perm: Perm | {
ancestor in group.explicit[ancestor_perm]
ancestor_perm in child_perm + child_perm.includes
}
}
check explicit_greater_implies_implicit_greater {
children_have_greater_perms_than_parent =>
all perm: Perm, child: Object, ancestor: child.^parent - RootFolder |
user_implicit[perm, ancestor] => user_implicit[perm, child]
} for 3 Object, 2 Group, 1 steps
run children_have_greater_perms_than_parent for 3 Object, 2 Group, 2 steps
check user_cannot_gain_or_lose_access_if_children_have_greater_explicit_perms_than_parents {
children_have_greater_perms_than_parent => user_cannot_gain_or_lose_access
} for 3 Object, 2 Group, 2 steps
