AUDITOR-LOGIC-REPORT.md

# AUDITOR-LOGIC FINAL AUDIT REPORT
## ROWM Polymorphic Notebook — Logic Engine Security & Correctness Review

**Date:** 2026-07-27  
**Scope:** `/c/Users/jessi/Desktop/rowm-polymorphic-notebook/logic/` directory  
**Files Audited:** 10 Prolog modules (5 fact, 5 rule), test suite  
**Total Lines:** ~900 lines of logic code  

---

## EXECUTIVE SUMMARY

### Verdict: **NOT RELEASE READY**

The Prolog/Datalog authorization and release-readiness logic contains **2 CRITICAL security/correctness bugs** and **7 HIGH/MEDIUM issues** that create exploitable authorization bypasses and release-gate vulnerabilities.

### Counts by Severity
- **CRITICAL:** 2 findings (authorization bypass, expired capability enforcement)
- **HIGH:** 3 findings (tier_2 bypass, hardcoded proofs, unverified metadata)

- **MEDIUM:** 4 findings (recursion, caching, unreachable code, semantics)

- **LOW:** 1 finding (code quality)



### Key Risks

1. **Authorization gate is bypassable** — dispatch_permitted/5 can be circumvented by direct predicate queries
2. **Expired capabilities remain active** — get_time/1 hardcoded, boundary condition wrong

3. **Tier_2 agents can execute** — capability_satisfies/4 has no trust check
4. **Release gate incomplete** — proof list hardcoded, won't detect new obligations
5. **Notebook metadata unverified** — cell status not cryptographically linked to ledger

---

## CRITICAL FINDINGS (2)

### CRITICAL-1: Authorization Gate Bypassable via Direct Predicate Queries

**File:** `logic/rules/authorization.pl` (lines 44-51)

**The Issue:**
External code can bypass dispatch_permitted/5 by querying authorization predicates directly:



```prolog

?- capability_active('capa_001_loc_rust_exec', Result).  % Bypasses all checks
?- agent_authorized(loc, 'capa_001_loc_rust_exec', rust).  % Partial checks only

```



Dispatch_permitted enforces these checks:
- Agent trust level (tier_2 agents should be blocked)

- Runtime active status

- Permission scope



**Attack:** Query capability_active directly to bypass agent_authorized tier_2 check.

**Impact:** Any agent can execute by circumventing dispatch_permitted/5.



---



### CRITICAL-2: Expired Capabilities Remain Active (Timestamp Bug)



**File:** `logic/rules/authorization.pl` (lines 17-22, 55)



**The Issue:**



```prolog

get_time(1719432000).  % HARDCODED — not dynamic

capability_active(CapID, true) :-

    capability_issued(CapID, _, _, _, _, IssuedAt, ExpiresAt),
    \+ capability_revoked(CapID, _),

    get_time(Now),

    Timestamp is floor(Now),

    Timestamp =< ExpiresAt.  % Inclusive (WRONG)

```


Example from capabilities.pl:
```prolog

capability_issued('capa_006_phantom_rust_log', ..., 1719432000, 1719432000).

% IssuedAt = 1719432000, ExpiresAt = 1719432000 (same time)



capability_valid('capa_006_phantom_rust_log', false).  % Declared expired

```

**The Bug:**
- Comparison: 1719432000 =< 1719432000 → TRUE
- Capability flagged active despite ExpiresAt being NOW
- Contradictory facts: capability_active returns true, capability_valid asserts false

**Root Causes:**
1. get_time/1 hardcoded, not dynamic

2. Boundary uses =< instead of <

3. Contradictory facts create logic inconsistency



**Impact:** Expired capabilities cannot be enforced. System allows active use of expired credentials.



---



## HIGH SEVERITY FINDINGS (3)



### HIGH-1: Tier_2 Agents Can Execute via capability_satisfies Query



**File:** `logic/rules/authorization.pl` (lines 35-42)



**Issue:** capability_satisfies/4 has no agent trust level check. Tier_2 agents are blocked only in agent_authorized/3.

```prolog

% Tier_2 check in agent_authorized:

agent_authorized(AgentID, CapID, TargetRuntime) :-

    ...

    TrustLevel \= tier_2,  % ← ONLY HERE

    ...



% But capability_satisfies has NO agent check:

capability_satisfies(CapID, Permission, TargetRuntime, true) :-

    capability_issued(CapID, _, _, TargetRuntime, Permissions, _, _),

    member(Permission, Permissions),

    capability_active(CapID, true).  % No trust check

```

**Attack:**
```prolog

?- capability_satisfies('capa_006_phantom_rust_log', log, rust, Result).

% Returns true — phantom is tier_2 but no check performed

```

**Impact:** Observer agents can gain execution permissions.

---

### HIGH-2: release_ready Gate Has Hardcoded Proof List



**File:** `logic/rules/release.pl` (lines 45-49)



**Issue:** Proof verification is hardcoded to 4 specific proof IDs. No dynamic discovery of new proofs.



```prolog

all_proofs_satisfied(true) :-

    proof_satisfied('proof_borrow_step_sound', true),

    proof_satisfied('proof_cons_cell_model', true),

    proof_satisfied('proof_dispatch_safe', true),
    proof_satisfied('proof_receipt_chain_integrity', true).

```


If developer adds new proof obligation, release_ready won't check it.



**Scenario:**

```prolog

% New proof added:

proof_obligation('proof_new_invariant', 'Some theorem', 'lean4').

% But all_proofs_satisfied still checks only 4 proofs
?- release_ready(Result).

% Result = true  ← NEW PROOF NOT CHECKED

```



**Impact:** Release gate can be bypassed by new proof obligations.



---



### HIGH-3: Notebook Metadata Overrides Logic Without Ledger Verification



**File:** `logic/rules/release.pl` (lines 73-80)



**Issue:** Cell completion status checked against notebook_cells.pl facts (parsed from JSON) without cryptographic verification against receipt chain.

```prolog

all_cells_complete(true) :-

    \+ (cell_exists(CellID, _Type, _Kernel, _Visibility, _SourceHash, _OutputHash),

        \+ (cell_sealed(CellID, true) ; cell_metadata(CellID, _Class, _DepCount, passed))).

```

**Attack:**
```prolog

% Original:

cell_metadata('rust-bridge-test', test, 1, failed).



% Attacker modifies to:

cell_metadata('rust-bridge-test', test, 1, passed).



% Logic engine has no way to know:

?- release_ready(Result).

% Result = true  ← BYPASSES ACTUAL EXECUTION

```

**Root Cause:** Notebook metadata facts are not linked to immutable receipts.

**Impact:** Attacker can mark failing cells as passed, bypassing proof requirements.

---

## MEDIUM SEVERITY FINDINGS (4)

### MEDIUM-1: state_reachable Recursion Has No Cycle Detection



**File:** `logic/rules/transitions.pl` (lines 45-54)



**Issue:** Recursive rule lacks tabling, cycle detection, or depth limits.



```prolog

state_reachable(Stage, FromState, true) :-
    Stage \= receive,

    stage_prerequisite(Stage, PrevStage),

    state_reachable(PrevStage, FromState, true).  % RECURSION


state_reachable(_, _, false).

```



Current fact set is acyclic, but logic has no guards.



**Scenario:**

```prolog

% Buggy fact:

stage_prerequisite(dispatch, receive).  % Creates cycle

% Infinite loop:
?- state_reachable(dispatch, initial, Result).

% Hangs indefinitely

```



**Impact:** Logic engine can hang on state queries.



---



### MEDIUM-2: Revocation May Not Propagate (Caching)



**File:** `logic/rules/authorization.pl` (line 19)



**Issue:** Uses negation-as-failure which may be cached by Prolog. External code may cache capability_active results.

```prolog

capability_active(CapID, true) :-

    capability_issued(CapID, _, _, _, _, IssuedAt, ExpiresAt),

    \+ capability_revoked(CapID, _),  % Negation-as-failure

    ...

```

**Scenario:**
```prolog

% Cached at T1:

capability_active('cap_X', Result).  % Result = true



% Revocation at T2:

assert(capability_revoked('cap_X', 'reason')).



% Cached result still used at T3:

% Result = true  ← Revocation not reflected

```

**Impact:** Revoked capabilities can remain active in cached state.

---

### MEDIUM-3: receipt_sequence_valid Has Unreachable Dead Code

**File:** `logic/rules/provenance.pl` (lines 33-42)

**Issue:** First clause calls undefined predicate previous_receipt_id/1 (should be previous_receipt/2).



```prolog

receipt_sequence_valid(ReceiptID) :-

    ...

    (previous_receipt(ReceiptID, _) -> 

     receipt_sequence_valid(previous_receipt_id(ReceiptID)) ; true).

    % ↑ undefined predicate — always fails



% Falls back to simplified version:

receipt_sequence_valid(ReceiptID) :-

    receipt_issued(ReceiptID, _SeqNum, Agent, CapID, ...),

    agent_active(Agent, true),
    capability_valid(CapID, true).

```


**Impact:** Sequence validation logic is incomplete. Monotonic sequence number verification is skipped.

---

### MEDIUM-4: no_revoked_capabilities Semantics Undocumented

**File:** `logic/rules/release.pl` (lines 66-71)

**Issue:** Double negation-as-failure semantics are unclear and potentially misunderstood.

```prolog

no_revoked_capabilities(true) :-

    \+ (agent_active(Agent, true),

        capability_issued(_CapID, _Issuer, Agent, _Runtime, _Perms, _Issued, _Expires),

        capability_revoked(_CapID, _)).

```

**Semantic Gap:**
- **Checks:** "There does NOT exist an active agent with a revoked capability"
- **Name suggests:** "All capabilities are not revoked"
- These are different: inactive agents' revocations are ignored

**Impact:** Confusing semantics may lead to misuse.

---

## LOW SEVERITY FINDINGS (1)

### LOW-1: dispatch_permitted Overly Permissive Catch-All



**File:** `logic/rules/authorization.pl` (line 51)



**Issue:** Catch-all clause with all unbound variables creates infinite choice points.



```prolog

dispatch_permitted(_, _, _, _, false).  % All variables unbound
```



On backtracking with unbound variables, generates infinite choice points. Minor performance issue, not a correctness bug.



---



## RELEASE-READINESS BLOCKERS



### Blockers (Must Fix Before Release)



**CRITICAL Fixes:**

1. Enforce dispatch_permitted/5 as sole authorization entry point

2. Fix get_time/1 to be dynamic and use exclusive boundary (<)

3. Fix capability_active contradiction with capability_valid



**HIGH Priority Fixes:**

4. Replace hardcoded proof list with dynamic discovery (findall)

5. Add cryptographic verification of notebook metadata against receipts

6. Add tier_2 check to capability_satisfies



**MEDIUM Priority Fixes:**

7. Add cycle detection to state_reachable (tabling or explicit detection)

8. Fix dead code in receipt_sequence_valid

9. Document closed-world assumptions for negation-as-failure

10. Implement revocation propagation or cache invalidation



---



## SYSTEM ARCHITECTURE ISSUES



### Issue 1: No Forced Authorization Routing

Individual authorization predicates are exported as library functions with no enforcement that callers use dispatch_permitted/5.



**Fix:** Seal authorization as a module, export only dispatch_permitted and release_ready.



### Issue 2: Notebook Metadata Not Cryptographically Linked

Cell completion status (notebook_cells.pl) is separate from receipt chain (receipts.pl).



**Fix:** Add predicate to verify cell_metadata against receipt chain hashes.



### Issue 3: Hardcoded Lists Instead of Dynamic Discovery

Proof list, agent list, runtime list should be dynamically discovered.



**Fix:** Use findall to query all proof_obligation facts instead of hardcoding.



---



## TEST GAPS



**Missing Tests:**

- Direct capability_active query bypassing dispatch_permitted

- Tier_2 agent execution via capability_satisfies

- Revocation propagation

- Dynamic proof discovery

- Cycle detection in state transitions



**Current Test Issues:**

- test_queries.pl expects capability_active('capa_006_phantom_rust_log', false)

- But logic returns true due to timestamp bug

- **Test would pass incorrectly** without fixing the bug



---



## AUDIT SUMMARY



**Audit Tool:** AUDITOR-LOGIC  

**Date:** 2026-07-27  

**Modules Audited:** 10 (5 fact, 5 rule)  

**Lines Audited:** ~900  

**Issues Found:** 9 (2 CRITICAL, 3 HIGH, 4 MEDIUM, 1 LOW)  

**Release Verdict:** NOT READY



**Files Audited:**

- logic/facts/agents.pl

- logic/facts/capabilities.pl

- logic/facts/notebook_cells.pl

- logic/facts/receipts.pl

- logic/facts/runtimes.pl

- logic/rules/authorization.pl

- logic/rules/proofs.pl

- logic/rules/provenance.pl

- logic/rules/release.pl

- logic/rules/transitions.pl

- logic/queries/test_queries.pl