Lab 09: Formal Verification & Model Checking¶

from z3 import *

# ── Domain Setup ──────────────────────────────────────────────────
# We model a Role-Based Access Control policy for a hospital system.
# Roles: NURSE, DOCTOR, ADMIN, AUDITOR
# Resources: PATIENT_RECORDS, BILLING, PRESCRIPTIONS, AUDIT_LOGS, ADMIN_CONFIG

Role = Datatype('Role')
Role.declare('NURSE')
Role.declare('DOCTOR')
Role.declare('ADMIN')
Role.declare('AUDITOR')
Role = Role.create()

Resource = Datatype('Resource')
Resource.declare('PATIENT_RECORDS')
Resource.declare('BILLING')
Resource.declare('PRESCRIPTIONS')
Resource.declare('AUDIT_LOGS')
Resource.declare('ADMIN_CONFIG')
Resource = Resource.create()

# Access function: can_access(role, resource) -> Bool
can_access = Function('can_access', Role, Resource, BoolSort())

# ── Policy Axioms ─────────────────────────────────────────────────
solver = Solver()

# Doctors can access patient records and prescriptions
solver.add(can_access(Role.DOCTOR, Resource.PATIENT_RECORDS) == True)
solver.add(can_access(Role.DOCTOR, Resource.PRESCRIPTIONS) == True)
solver.add(can_access(Role.DOCTOR, Resource.BILLING) == False)
solver.add(can_access(Role.DOCTOR, Resource.AUDIT_LOGS) == False)
solver.add(can_access(Role.DOCTOR, Resource.ADMIN_CONFIG) == False)

# Nurses can access patient records only
solver.add(can_access(Role.NURSE, Resource.PATIENT_RECORDS) == True)
solver.add(can_access(Role.NURSE, Resource.PRESCRIPTIONS) == False)
solver.add(can_access(Role.NURSE, Resource.BILLING) == False)
solver.add(can_access(Role.NURSE, Resource.AUDIT_LOGS) == False)
solver.add(can_access(Role.NURSE, Resource.ADMIN_CONFIG) == False)

# Admins can access billing and admin config, NOT patient records
solver.add(can_access(Role.ADMIN, Resource.PATIENT_RECORDS) == False)
solver.add(can_access(Role.ADMIN, Resource.BILLING) == True)
solver.add(can_access(Role.ADMIN, Resource.PRESCRIPTIONS) == False)
solver.add(can_access(Role.ADMIN, Resource.AUDIT_LOGS) == False)
solver.add(can_access(Role.ADMIN, Resource.ADMIN_CONFIG) == True)

# Auditors can access audit logs only
solver.add(can_access(Role.AUDITOR, Resource.PATIENT_RECORDS) == False)
solver.add(can_access(Role.AUDITOR, Resource.BILLING) == False)
solver.add(can_access(Role.AUDITOR, Resource.PRESCRIPTIONS) == False)
solver.add(can_access(Role.AUDITOR, Resource.AUDIT_LOGS) == True)
solver.add(can_access(Role.AUDITOR, Resource.ADMIN_CONFIG) == False)

# ── Property Verification ─────────────────────────────────────────

def verify_property(name: str, property_formula):
    """Try to find a counterexample to the property. If UNSAT, property holds."""
    s = Solver()
    for c in solver.assertions():
        s.add(c)
    # Add negation of property — if UNSAT, property is proven
    s.add(Not(property_formula))
    result = s.check()
    if result == unsat:
        print(f"PROVED ✓  {name}")
    elif result == sat:
        print(f"VIOLATED ✗  {name}")
        print(f"  Counterexample: {s.model()}")
    else:
        print(f"UNKNOWN   {name}")

r = Const('r', Role)

# Property 1: Separation of Duty — no role has access to both patient records AND admin config
verify_property(
    "SoD: No role accesses both PATIENT_RECORDS and ADMIN_CONFIG",
    ForAll([r], Not(And(can_access(r, Resource.PATIENT_RECORDS),
                        can_access(r, Resource.ADMIN_CONFIG))))
)

# Property 2: Least Privilege — nurses cannot access prescriptions
verify_property(
    "LeastPriv: NURSE cannot access PRESCRIPTIONS",
    can_access(Role.NURSE, Resource.PRESCRIPTIONS) == False
)

# Property 3: Auditors are read-only (can only access audit logs)
res = Const('res', Resource)
verify_property(
    "AuditOnly: AUDITOR can only access AUDIT_LOGS",
    ForAll([res], Implies(
        can_access(Role.AUDITOR, res),
        res == Resource.AUDIT_LOGS
    ))
)

# YOUR PROPERTIES (required for Part A credit):
# Add 3 more meaningful security properties and verify them.
# Examples: "no two roles share identical access", "admin cannot read PHI"

from z3 import *

# ── Authentication Protocol Model ────────────────────────────────
# Protocol: Client proves identity to Server using a token.
#
# Steps:
#   1. Client sends (username, token) to Server
#   2. Server checks: token == HMAC(secret, username + nonce)
#   3. Server checks: nonce not previously seen (replay protection)
#   4. Server grants access if both checks pass
#
# BUGGY VERSION: The nonce check is missing (replay attack possible)

# Sorts
Token, (valid_token, invalid_token) = EnumSort('Token', ['valid', 'invalid'])
Nonce, (fresh_nonce, replayed_nonce) = EnumSort('Nonce', ['fresh', 'replayed'])

# Protocol predicates
token_valid = Function('token_valid', Token, BoolSort())
nonce_fresh = Function('nonce_fresh', Nonce, BoolSort())
access_granted = Function('access_granted', Token, Nonce, BoolSort())

s = Solver()

# Token validity axioms
s.add(token_valid(valid_token) == True)
s.add(token_valid(invalid_token) == False)

# Nonce freshness axioms
s.add(nonce_fresh(fresh_nonce) == True)
s.add(nonce_fresh(replayed_nonce) == False)

# BUGGY protocol: grants access on valid token regardless of nonce
s.add(ForAll([Const('t', Token), Const('n', Nonce)],
    access_granted(Const('t', Token), Const('n', Nonce)) == token_valid(Const('t', Token))
))

t = Const('t', Token)
n = Const('n', Nonce)

# ── Verify Security Properties ────────────────────────────────────
def check(name, formula):
    chk = Solver()
    for c in s.assertions():
        chk.add(c)
    chk.add(Not(formula))
    result = chk.check()
    status = "PROVED ✓" if result == unsat else "VIOLATED ✗"
    print(f"{status}  {name}")
    if result == sat:
        print(f"  Counterexample: {chk.model()}")

# Property: Only valid tokens get access (should hold)
check("AuthN: Invalid token is always denied",
    ForAll([n], Not(access_granted(invalid_token, n))))

# Property: Replay attack is impossible (should be VIOLATED in buggy version)
check("Replay: Replayed nonce is always denied",
    ForAll([t], Not(access_granted(t, replayed_nonce))))

print()
print("--- FIXED PROTOCOL ---")

# Fix: add nonce check to access_granted
s2 = Solver()
s2.add(token_valid(valid_token) == True)
s2.add(token_valid(invalid_token) == False)
s2.add(nonce_fresh(fresh_nonce) == True)
s2.add(nonce_fresh(replayed_nonce) == False)

# Correct protocol: requires BOTH valid token AND fresh nonce
t2 = Const('t', Token)
n2 = Const('n', Nonce)
s2.add(ForAll([Const('t2', Token), Const('n2', Nonce)],
    access_granted(Const('t2', Token), Const('n2', Nonce)) ==
    And(token_valid(Const('t2', Token)), nonce_fresh(Const('n2', Nonce)))
))

def check2(name, formula):
    chk = Solver()
    for c in s2.assertions():
        chk.add(c)
    chk.add(Not(formula))
    result = chk.check()
    status = "PROVED ✓" if result == unsat else "VIOLATED ✗"
    print(f"{status}  {name}")

check2("Fixed: Invalid token denied", ForAll([n2], Not(access_granted(invalid_token, n2))))
check2("Fixed: Replayed nonce denied", ForAll([t2], Not(access_granted(t2, replayed_nonce))))
check2("Fixed: Valid token + fresh nonce grants access",
       access_granted(valid_token, fresh_nonce) == True)