A real-world success story

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!

  1. To see how users can move folders around to give themselves access they didn’t originally have, run user_cannot_gain_or_lose_access and see the failure.
  2. Next, uncomment the code below // User must also own all of the source object's children in the move_object predicate. This represents a patch we made to prevent users from gaining access. But users can still lose access! Run user_cannot_gain_or_lose_access again to see how.
  3. 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
            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 {
            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 {
} for 3 Object, 2 Group, 2 steps

check user_cannot_gain_or_lose_access_if_only_one_group {
} 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 {
        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


Hi, looks great. I’m looking forward to reading the said story, this looks quite compelling.
A few remarks:

  • includes looks like a total order. In that case, you could just make Perm “util/ordered” and use next instead of includes, thus benefiting for free from the preds and funs defined in util/ordering. Actually, you can even make Perm an enum. In that case, it will be implicitly “util/ordered” (following the order of declarations in the enum) and I think it should be more efficient in general. If you want to keep the name includes, you could even add fun includes : Perm -> Perm { ordering/next }.
  • a signature-local fact as in User implicitly starts with always all this: User | ... so the always on line 87 can be removed.
  • in Group, can’t you remove the local fact and rather type explicit as Perm -> (l)one Object, as it means always all g: Group, p: Perm | (l)one g.explicit[p], which seems to do what you want.
  • depending on your needs, you may remove the RootFolder declaration and make parent lone, with an additional fact stating that there’s only one folder which doesn’t have a parent (you could even define it with a fun, then). It may enable you to make less distinctions between this specific folder and others. Indeed, it’s a bit strange that RootFolder isn’t a folder itself in your model.
  • finally, the two facts all_objects_connected_to_tree and tree_is_acyclic could perhaps be made assertions rather than facts, because as facts they may rule out bad scenarios implicitly. The price to pay, if you made them assertions, is that you should probably also add new operations to account for the creation of the file system (instead of considering it as a given).

Thank you! Implementing your suggestions now. You can find the most current version of the code on GitHub!

The two exceptions:

I think this needs to be Perm lone -> Object. A Group can have explicit Permissions for many Objects, but a Group cannot assign multiple explicit Permissions to the same Object. This seems to have the same semantics as the disj[this.explicit[Own], this.explicit[Edit], ...] fact did.

I think that might be out of scope😅 My philosophy is that we write facts to describe the code we explicitly wrote into the system, and we write assertions to describe the properties that we hope will emerge from the system. Our filesystem already has code to guarantee a tree structure, and my goal is to keep the spec under 250 lines even with extensive comments. I’m hoping to impress upon readers just how short a spec you can write in order to stress-test an idea that, to mortals, might look perfectly sound😉

Looks like this repo is private, isn’t it?

Lapsus calami, you’re right.
In general, I tend to favor multiplicities over additional facts as the former may (supposedly) lead to a better SAT encoding.

+1 I was just wondering whether an unwanted behavior might emerge from the combination of permission handling and filesystem operations. If it’s separated, there’s no need to change the model.

Finally, re-reading the original model, I’m stumbling upon fact users_can_move_objects: in general, unless it is absolutely required, it’s good practice to avoid one as it prunes behaviors where interacting events may happen at the same time and lead to unwanted behaviors. In principle, if your events have “good” frame conditions, then some should be enough and allow additional traces (in some cases).

PS: another reason to be wary of one is that one a: A, b: B | p is in general not equivalent to one a: A, one b: B | ... and it’s easy to shoot yourself in the foot.

Sparkling spanakopita, you’re right! It’s now public: GitHub - jthemphill/permission-model: Model of a permissions-based filesystem using Alloy

I’ll try this when I get some free time!

Hm, does the second one apply the predicate only to the one b: B clause?

Not really. See this for an explanation.

Ah, that actually seems pretty reasonable after seeing your example!

@jthemphill: This is wonderful! I strongly encourage you to publish this as it will be very helpful to other people. A few questions/suggestions about the version of the spec here:

  • At first, I thought it was gratuitous to have a permission of None (in addition to allowing an object to have no permission) because it seemed to make a distinction that didn’t have any consequence. But now that I’ve played with your spec a bit I can see that there is a very important difference, since the calculation of implicit permissions relies on whether there are explicit permissions, so a permission of None in an ancestor overrides an inherited permission. This is very subtle and needs a comment explaining it! I’m not sure I understand the consequence of group_implicit always granting None: that looks inconsistent with this, but maybe it doesn’t matter.
  • I don’t understand why the Move sig is variable. Aren’t these Move objects just immutable argument pairs for the move predicate? I assume you’re doing this to show the move action in the visualization more directly. It’s like going part way towards the style I describe in my book in which events are modeled as signatures. I haven’t worked on this, but I wonder if there is a better way to do this (that is, to exploit Alloy 6 but still get objects for each action).
  • A few syntactic nitpicks: rather than x = none you can just write no x; and instead of x != none you can write some x.
  • You can get shorter commands in the menu by adding a name with a colon. Eg, instead of
pred user_cannot_gain_or_lose_access {...}
check user_cannot_gain_or_lose_access {user_cannot_gain_or_lose_access} for ...

you can write

user_cannot_gain_or_lose_access: check { ... } for ...

Thank you! I’m looking for the right venue to publish it - whether in a personal blog or on behalf of my employer. Also, shipping the project comes before bragging about how we used cool mathy tools to help us nail down the project’s design😉

Correct! In the Alloy model, I might want to rename this level to CannotSee, and that would avoid the name/concept collision with Alloy’s none keyword.

In the first draft of my model, each permissions level was a subset of stronger permissions. Since None is the weakest permission, every other permission includes it. group_implicit[perm, group, obj] asks “does group have perm access, or better, to obj?” and the answer is always yes if the needed permission is None. But that was before I learned about Ordering, enums, and the fact that enums have orderings built in. There is probably a more intuitive way to write this.

I’m trying to follow “An idiom to depict events” from Formal Software Design with Alloy 6, which may or may not be the book you’re describing. I actually used a lot of trial-and-error here! I wasn’t even sure what var sig meant, at first. It appears that a var sig can spontaneously exist or disappear in any given timestep. I believe this is what I want, though - iff an object is moving, I want a Move object to exist with relations to the object and its destination folder.

Yes! Naturally, I prefer a completely different theme😉 But I agree the diagram needs a theme in order to make visual sense. Is there a way to encode a theme in the comments?

1 Like

All makes good sense.

Regarding the publication venue, two things you might consider: an industrial track of one of the major conferences (advantage is engaging with people), and an article in CACM (advantage is more readers); and both will give you a permanent record in the ACM digital library.

And regarding the theme: it would be great if you added it to the GH repo with the paper.

Happy to discuss this more with you directly. Best, Daniel

BTW, by “my book”, I was referring to the book I wrote about Alloy. You may find it useful although it doesn’t include the new temporal operators. I’m very excited about the new book by Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo.

Depending on the model, var sigs may be used to depict events but keep in mind that, as any sig, a var sig has a bounded scope. Depending on how traces are specified, the bound could implicitly prune interesting behaviours (e.g. suppose that the possible number of move events in a given step can be larger than the scope on Move, then you may miss traces (depending on your exact model)).

The idiom we recommend does not feature var sigs. The idea is rather the following:

  • Create an Event enum representing the names of all possible events
  • For any event (as a predicate), create a fun with the same name, and an arity that accounts for the name and parameters of the event. This fun returns all instances for which the event is true.
  • Add and events fun which contains the union of all names of events that are known to happen (these are obtained out of the funs defined just above).

This is enough for visualization: all you need now is to play with the theme to tweak the display of all these funs.

This idiom is also described on this page of the forum, you may find it clearer?

1 Like