access_control.iml

(*
   --------------------------------------------------------------------------
   title: Access Control System
   name: access-control
   description: Role-based access control with permission logic
   --------------------------------------------------------------------------
 
   Real-world example: Access Control System
 
   Use case: Verify if a user can access a resource based on their role and permissions.
 
   Practical implications:
   - Region decomposition reveals all possible access scenarios
   - Each region represents a distinct authorization case
   - Models provide test cases for security testing
   - Helps identify edge cases in permission logic
*)
 
type role = Admin | Manager | User | Guest
 
let role_level r =
  match r with
  | Admin -> 4
  | Manager -> 3
  | User -> 2
  | Guest -> 1
 
type resource_sensitivity = Public | Internal | Confidential | Secret
 
let required_level sens =
  match sens with
  | Public -> 1
  | Internal -> 2
  | Confidential -> 3
  | Secret -> 4
 
(* Check if user can access resource *)
let can_access role resource is_owner =
  let user_level = role_level role in
  let req_level = required_level resource in
  if user_level >= req_level then
    "granted"
  else if is_owner && user_level >= 2 then
    (* Users and above can access their own resources one level up *)
    "granted"
  else
    "denied"
[@@decomp top ()]
 
(* Variation: Using basis to keep helper functions symbolic *)
let can_access_abstract role resource is_owner =
  let user_level = role_level role in
  let req_level = required_level resource in
  if user_level >= req_level then
    "granted"
  else if is_owner && user_level >= 2 then
    "granted"
  else
    "denied"
[@@decomp top ~basis:[[%id role_level]; [%id required_level]] ()]