Tutorial 3: Policy-Driven Design¶

Duration: 1 hour
Prerequisites: Tutorials 1-2 completed
What you'll learn: Authorization policies, RBAC, ABAC, context-aware security, and policy testing

Overview¶

USL's policy layer ensures security is not an afterthought—it's enforced at every layer. In this tutorial, you'll master:

Role-Based Access Control (RBAC)
Attribute-Based Access Control (ABAC)
Context-aware policies
Policy composition and inheritance
Time-based and location-based rules
Policy verification and testing

The Project: Healthcare Records System¶

We'll build a HIPAA-compliant medical records system with:

Multiple user roles (patients, doctors, nurses, admins)
Strict data access controls
Audit logging requirements
Time and location restrictions
Emergency access overrides

Step 1: Define the Domain¶

domain Healthcare {
  entity Patient {
    id: PatientId @primary
    name: String
    dateOfBirth: Date
    ssn: String @secret
    medicalRecordNumber: String @unique
    primaryDoctorId: Option[DoctorId]
  }

  entity Doctor {
    id: DoctorId @primary
    name: String
    specialty: String
    licenseNumber: String @unique
    hospital: HospitalId
  }

  entity MedicalRecord {
    id: RecordId @primary
    patientId: PatientId
    doctorId: DoctorId
    diagnosis: String @sensitive
    treatment: String @sensitive
    notes: String @sensitive
    recordedAt: Timestamp
    accessLevel: AccessLevel
  }

  entity User {
    id: UserId @primary
    email: Email @unique
    role: Role
    hospitalId: HospitalId
    department: String
    clearanceLevel: Int
  }

  enum Role {
    Patient
    Doctor
    Nurse
    Admin
    Receptionist
  }

  enum AccessLevel {
    Public      // Basic demographics
    Restricted  // Requires authorization
    Confidential // Treating physician only
    Emergency   // Emergency override available
  }
}

Step 2: Simple RBAC Policies¶

Start with role-based rules:

policy BasicMedicalPolicy {
  actor user: User

  // Admins can do everything
  rule admin_full_access {
    user.role == Role.Admin
  }

  // Doctors can view records
  rule doctor_view_records(record: MedicalRecord) {
    user.role == Role.Doctor
  }

  // Patients can view their own records
  rule patient_view_own_records(record: MedicalRecord) {
    user.role == Role.Patient &&
    user.id == record.patientId
  }

  // Nurses can view records in their department
  rule nurse_view_department_records(record: MedicalRecord) {
    user.role == Role.Nurse &&
    user.hospitalId == getHospital(record.patientId)
  }
}

Policy Structure¶

actor: The user attempting the action
rule: Named authorization check
Parameters: Entities being accessed
Returns: Boolean (allow/deny)

Step 3: Attribute-Based Access Control (ABAC)¶

Add fine-grained attribute-based rules:

policy AttributeBasedPolicy {
  actor user: User

  // Access level check
  rule access_by_clearance(record: MedicalRecord) {
    match record.accessLevel {
      AccessLevel.Public => true
      AccessLevel.Restricted => user.clearanceLevel >= 2
      AccessLevel.Confidential => user.clearanceLevel >= 4
      AccessLevel.Emergency => user.clearanceLevel >= 5
    }
  }

  // Treating physician has special access
  rule treating_physician_access(record: MedicalRecord) {
    user.role == Role.Doctor &&
    user.id == record.doctorId
  }

  // Same department access
  rule same_department_access(record: MedicalRecord) {
    let patient = load(Patient, record.patientId)
    let doctor = load(Doctor, record.doctorId)
    user.department == doctor.department
  }

  // Primary care physician access
  rule primary_care_access(record: MedicalRecord) {
    let patient = load(Patient, record.patientId)
    match patient.primaryDoctorId {
      Some(docId) => user.id == docId
      None => false
    }
  }
}

ABAC vs RBAC

RBAC: "Can doctors view records?" (role-based)
ABAC: "Can this doctor view this specific record?" (attribute-based)

ABAC provides much finer control but requires more complex policies.

Step 4: Context-Aware Policies¶

Add environmental context to decisions:

policy ContextAwarePolicy {
  actor user: User
  context ctx: RequestContext

  // Business hours only for non-emergency
  rule business_hours_access(record: MedicalRecord) {
    if record.accessLevel == AccessLevel.Emergency {
      true  // Emergency always accessible
    } else {
      isBusinessHours(ctx.timestamp)
    }
  }

  // Location-based access
  rule location_based_access(record: MedicalRecord) {
    let hospital = load(Hospital, user.hospitalId)
    isWithinGeofence(ctx.location, hospital.location, radius: 100m)
  }

  // Device trust level
  rule trusted_device_access(record: MedicalRecord) {
    match record.accessLevel {
      AccessLevel.Confidential => ctx.device.trustLevel >= TrustLevel.High
      AccessLevel.Emergency => ctx.device.trustLevel >= TrustLevel.Maximum
      _ => ctx.device.trustLevel >= TrustLevel.Basic
    }
  }

  // Rate limiting
  rule rate_limit_check(record: MedicalRecord) {
    let accessCount = countAccess(user.id, last: 1 hour)
    match user.role {
      Role.Doctor => accessCount < 100
      Role.Nurse => accessCount < 50
      Role.Patient => accessCount < 10
      _ => accessCount < 5
    }
  }
}

// Context structure
value RequestContext {
  timestamp: Timestamp
  location: GeoLocation
  ipAddress: String
  device: DeviceInfo
  sessionId: String
}

value DeviceInfo {
  trustLevel: TrustLevel
  fingerprint: String
  lastVerified: Timestamp
}

enum TrustLevel {
  Unknown
  Basic
  High
  Maximum
}

Step 5: Policy Composition¶

Combine policies using logical operators:

policy ComprehensiveMedicalPolicy {
  actor user: User
  context ctx: RequestContext

  // Compose multiple policies
  rule view_medical_record(record: MedicalRecord) {
    // Must satisfy role-based AND attribute-based AND context rules
    (BasicMedicalPolicy.doctor_view_records(record) ||
     BasicMedicalPolicy.patient_view_own_records(record) ||
     BasicMedicalPolicy.nurse_view_department_records(record)) &&
    AttributeBasedPolicy.access_by_clearance(record) &&
    ContextAwarePolicy.business_hours_access(record) &&
    ContextAwarePolicy.location_based_access(record) &&
    ContextAwarePolicy.rate_limit_check(record)
  }

  // Emergency override
  rule emergency_access(record: MedicalRecord) {
    user.clearanceLevel >= 5 &&
    ctx.emergency == true &&
    auditLog("EMERGENCY_ACCESS", user.id, record.id)
  }

  // Final combined rule
  rule can_access(record: MedicalRecord) {
    view_medical_record(record) || emergency_access(record)
  }
}

Policy Inheritance¶

// Base policy
policy BaseHealthcarePolicy {
  actor user: User

  rule base_authorization {
    user.clearanceLevel >= 1 &&
    user.accountStatus == AccountStatus.Active
  }
}

// Extend base policy
policy SpecializedPolicy extends BaseHealthcarePolicy {
  // Automatically includes base_authorization

  rule specialized_access(record: MedicalRecord) {
    // Additional checks beyond base
    base_authorization() &&
    user.specialty == record.requiredSpecialty
  }
}

Step 6: Deny Rules and Exceptions¶

Explicitly deny certain actions:

policy DenyPolicy {
  actor user: User

  // Deny rules take precedence over allow rules
  deny rule no_self_prescription(prescription: Prescription) {
    user.role == Role.Doctor &&
    prescription.patientId == user.id
  }

  deny rule no_family_treatment(record: MedicalRecord) {
    let patient = load(Patient, record.patientId)
    isFamilyMember(user.id, patient.id)
  }

  deny rule suspended_users {
    user.accountStatus == AccountStatus.Suspended
  }

  // Allow exceptions to denials
  allow override emergency_family_treatment(record: MedicalRecord) {
    context.emergency == true &&
    user.clearanceLevel >= 5 &&
    noOtherDoctorAvailable()
  }
}

Deny Rule Priority

Deny rules always take precedence:

deny > allow override > allow

Step 7: Time-Based Policies¶

Implement temporal access controls:

policy TemporalPolicy {
  actor user: User

  rule time_window_access(record: MedicalRecord) {
    let window = getAccessWindow(user.id)
    now() >= window.start && now() <= window.end
  }

  rule shift_based_access(record: MedicalRecord) {
    let shift = getCurrentShift(user.id)
    shift.active && shift.hospital == user.hospitalId
  }

  rule expiring_access(record: MedicalRecord) {
    let grant = load(AccessGrant, user.id, record.id)
    match grant {
      Some(g) => now() < g.expiresAt
      None => false
    }
  }

  rule temporary_elevated_access {
    let elevation = getAccessElevation(user.id)
    match elevation {
      Some(e) => now() < e.expiresAt && e.level >= 4
      None => false
    }
  }
}

Step 8: Audit and Compliance¶

Integrate audit logging into policies:

policy AuditedPolicy {
  actor user: User

  rule access_with_audit(record: MedicalRecord) {
    let allowed = can_access(record)

    // Log every access attempt
    auditLog(AuditEvent {
      userId: user.id,
      recordId: record.id,
      action: "VIEW",
      allowed: allowed,
      timestamp: now(),
      reason: context.accessReason,
      ipAddress: context.ipAddress
    })

    // Require justification for confidential records
    if record.accessLevel == AccessLevel.Confidential {
      allowed && hasAccessJustification(context)
    } else {
      allowed
    }
  }

  rule hipaa_compliant_access(record: MedicalRecord) {
    // HIPAA minimum necessary principle
    let requestedFields = context.requestedFields
    let allowedFields = getMinimalFields(user.role, context.purpose)

    requestedFields.all(|f| allowedFields.contains(f)) &&
    auditHipaaAccess(user, record, requestedFields)
  }
}

Step 9: Policy Verification¶

USL can formally verify policy properties:

// Verify policy totality
verify policy ComprehensiveMedicalPolicy {
  // Every action has a rule
  totality {
    forall action in MedicalService {
      exists rule in ComprehensiveMedicalPolicy {
        rule.covers(action)
      }
    }
  }

  // No contradictory rules
  consistency {
    forall action in MedicalService {
      forall rule1, rule2 in ComprehensiveMedicalPolicy {
        rule1.covers(action) && rule2.covers(action) ->
        rule1.effect == rule2.effect
      }
    }
  }

  // Security properties
  property "patients can't access other's records" {
    forall user: User where user.role == Role.Patient {
      forall record: MedicalRecord {
        can_access(user, record) -> record.patientId == user.id
      }
    }
  }

  property "emergency access always logged" {
    forall user: User, record: MedicalRecord {
      emergency_access(user, record) ->
      exists log in AuditLog {
        log.type == "EMERGENCY_ACCESS" &&
        log.userId == user.id &&
        log.recordId == record.id
      }
    }
  }
}

Run verification:

usl verify healthcare.usl --policies

Output:

Verifying policies...
✓ Totality check passed
✓ Consistency check passed  
✓ Property "patients can't access other's records" proved
✓ Property "emergency access always logged" proved
✓ 0 policy gaps found
✓ 0 contradictions found

All policy verification checks passed!

Step 10: Policy Testing¶

Write comprehensive policy tests:

spec PolicyTests {
  test "doctor can view their patient's records" {
    let doctor = User { role: Role.Doctor, id: "doc1" }
    let record = MedicalRecord { 
      doctorId: "doc1",
      accessLevel: AccessLevel.Restricted
    }

    assert ComprehensiveMedicalPolicy.can_access(doctor, record) == true
  }

  test "patient can't view other patient's records" {
    let patient = User { role: Role.Patient, id: "patient1" }
    let record = MedicalRecord { 
      patientId: "patient2",
      accessLevel: AccessLevel.Restricted
    }

    assert ComprehensiveMedicalPolicy.can_access(patient, record) == false
  }

  test "emergency access overrides restrictions" {
    let nurse = User { 
      role: Role.Nurse,
      clearanceLevel: 5
    }
    let context = RequestContext { emergency: true }
    let record = MedicalRecord { 
      accessLevel: AccessLevel.Confidential
    }

    assert ComprehensiveMedicalPolicy.emergency_access(nurse, record) == true
  }

  test "deny rule prevents self-prescription" {
    let doctor = User { role: Role.Doctor, id: "doc1" }
    let prescription = Prescription { 
      doctorId: "doc1",
      patientId: "doc1"  // Self-prescription
    }

    assert DenyPolicy.no_self_prescription(doctor, prescription) == false
  }

  test "rate limit prevents excessive access" {
    let patient = User { role: Role.Patient, id: "patient1" }

    // Simulate 10 accesses
    repeat 10 {
      accessRecord(patient, someRecord)
    }

    // 11th access should be denied
    assert ContextAwarePolicy.rate_limit_check(patient, someRecord) == false
  }
}

Run policy tests:

usl test healthcare.usl --policies

Best Practices¶

DO ✅¶

Start with deny rules for critical security requirements
Use policy composition to build complex rules from simple ones
Always audit sensitive data access
Verify policies with formal methods
Test edge cases thoroughly
Document access justifications for compliance

DON'T ❌¶

Hard-code permissions in service layer
Skip totality checks
Ignore context information
Allow unbounded access
Mix authorization logic with business logic
Forget to log denials

Common Policy Patterns¶

1. Ownership Pattern¶

rule owner_access(resource: Resource) {
  user.id == resource.ownerId
}

2. Delegation Pattern¶

rule delegate_access(resource: Resource) {
  exists delegation in Delegation {
    delegation.from == resource.ownerId &&
    delegation.to == user.id &&
    delegation.resource == resource.id &&
    now() < delegation.expiresAt
  }
}

3. Hierarchical Pattern¶

rule hierarchical_access(resource: Resource) {
  let resourceOrg = getOrganization(resource)
  let userOrgs = getUserOrganizations(user)

  userOrgs.any(|org| isAncestor(org, resourceOrg))
}

rule consent_based_access(data: PersonalData) {
  exists consent in Consent {
    consent.userId == data.ownerId &&
    consent.grantedTo == user.id &&
    consent.purpose == context.purpose &&
    consent.active
  }
}

What You've Learned¶

✅ Role-Based Access Control (RBAC)
✅ Attribute-Based Access Control (ABAC)
✅ Context-aware policies
✅ Policy composition and inheritance
✅ Deny rules and exceptions
✅ Temporal access controls
✅ Audit integration
✅ Policy verification
✅ Comprehensive policy testing

Next Steps¶

Continue to Tutorial 4: Behavior & State Machines to learn:

State machine design
Transition guards and effects
Nested state machines
Parallel states
State machine verification