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
        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

1 Like

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).
1 Like

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!