RBAC Challeng in ALM

rbac.alm

// Role-Based Access Control in ALM
// This document includes 3 ALM modules
// that encode the core and hierachical
// components of the RBAC challenge.
// Link to official description: https://www3.cs.stonybrook.edu/~liu/papers/RBACchallenge-LPOP18.pdf

// Several entities are added and removed
// dynamically. We'll model there behavior
// as a separate module.
module dynamic_entity
    // The below reads: 
    // "The sort dynamic_entity is a sort
    // ranging from the integers 1 to 100"
    dynamic_entity :: 1..100
    // universe is our "top type"
    // similar to "Object" in Java.

    // Actions are model as their own
    // sort. We'll create two actions:
    // one that activates new instances of
    // dynamic_entity and another that 
    // destroys a target one.
    // Note: sorting out this use case
    // is a very important practical
    // question for Flamingo. We might
    // bake it into the language syntactic
    // sugar.
    new_dynamic_entity :: actions
    destroy_dynamic_entity :: dynamic_entity_action
        // Sorts can be assosciated with attributes
        // which are static functions from objects
        // of the sort to some other sort. Attributes 
        // are analogous to, e.g., read-only properties in
        // Java.
        attributes
            target_dynamic_entity : dynamic_entity
fluents
    basic
        // active is a function from dynamic
        // entities to booleans that marks which
        // ones are currently active. Note it is
        // as "basic fluent", indiciating it has
        // inertia and only changes if an action
        // causes it to change. Note, booleans
        // are one of the built-in sorts of ALM.
        active : dynamic_entity -> booleans
axioms
    // Our first causal law states that 
    // that if:
    // - an action occurs
    // - that action is an instance of the new_dynamic_entity sort
    // - the next_dynamic_entity is X
    // then:
    // - X becomes active.
    occurs(A) causes active(X) if
        instance(A, new_dynamic_entity),
        next_dynamic_entity = X.

    // This law is similar to the previous one,
    // but increments the next_dynamic_entity fluent.
    occurs(A) causes new_dynamic_entity = X + 1 if
        instance(A, new_dynamic_entity),
        next_dynamic_entity = X.

    // If an instance of destroy_dynamic_entity
    // occurs, then its target is deactivated.
    occurs(A) causes -active(X) if
        instance(A, destroy_dynamic_entity),
        target_dynamic_entity(A) = X.
    
    // This axiom is an executability condition,
    // which states that it's impossible to activate
    // an entity that is already active. Note!: axioms
    // of this form are guarantees the _user_ makes
    // to Flamingo. If they do indeed occur, a runtime
    // error will occur, potentially crashing the runtime.
    impossible occurs(A) if
        instance(A, new_dynamic_entity),
        target_dynamic_entity(A) = Target
        active(Target).
    
module core_rbac
// The core rbac module depends on the dynamic_entity module
uses dynamic_entity
sorts
    // This reads: "users is a subsort of dynamic_entity"
    users :: dynamic_entity
    roles :: dynamic_entity
    permissions :: dynamic_entity
fluents
    basic
        has_role : users x roles -> booleans
        has_permission : role x permissions -> booleans
        has_access : users x permissions -> booleans
axioms
    // The only axiom of this module is a state constraint
    // which says: A user has access to a given permission if
    // they have a role and that role includes that permission.
    has_access(User, Perm) if
        has_role(User, Role),
        has_permission(Role, Perm).

module hierarchical_rbac
uses core_rbac
sorts
    add_inheritance : actions
        attributes        
            ascendent : roles
            descendent : roles
fluents
    inerits : roles x roles -> booleans
defined
    // Defined fluents do not have inertia, and
    // are "recaluculated" on every state change.
    inherits_trans : roles x roles -> booleans
    // This property is not directly specified in the
    // RBAC Challenge Spec, but we will use it to make
    // our executability condition (which is specified)
    // more clear.
    candidate_descendent : roles x roles -> booleans


axioms
    // The transitive closure has the familiar
    // form in ALM.
    inherits_trans(A, B) if inherits(A, B).
    inherits_trans(A, C) if
        inherits_trans(A, B)
        inerits(B, C).

    // This state constraint asserts false
    // is true if a role inherits itself
    // (even transitively), preventing cyclic
    // inheritances. Unlike executability
    // conditions, Flamingo can test state
    // constraints for internal consistency.
    false if inherits_trans(A, A).

    occurs(A, add_inheritance) causes inerits(Desc, Asc) if
        instance(A, add_inheritance),
        ascendent(A) = Asc,
        descendent(A) = Desc.

    impossible occurs(A) if
        instance(A, add_inheritance),
        ascendent(A) = Asc
        descendent(A) = Desc
        inherits(Desc, Asc).

    // The spec requires a query for authorized
    // rules of a given user. We could create
    // a new defined fluent to represent this.
    // However, we can also simply extend the rules
    // for the existing has_role fluent. This allows
    // greater interoperability between modules, and
    // shows off ALM's powerful module system.
    has_role(User, RoleA) if
        has_role(User, RoleB),
        inherits_trans(RoleB, RoleA).