Hugging Face's logo

Snapkitty
/
rowm-polymorphic-notebook

snapkitty
developer-tools
python
Model card Files
xet
 Community
rowm-polymorphic-notebook / AUDITOR-LOGIC-REPORT.md
SNAPKITTYWEST's picture
SNAPKITTYWEST
push from SNAPKITTYWEST/rowm-polymorphic-notebook
1d3f990 verified
preview code
|
Raw History Blame Contribute Delete
12.3 kB

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:

?- 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:

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:

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.

% 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:

?- 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.

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:

% 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.

all_cells_complete(true) :-
    \+ (cell_exists(CellID, _Type, _Kernel, _Visibility, _SourceHash, _OutputHash),
        \+ (cell_sealed(CellID, true) ; cell_metadata(CellID, _Class, _DepCount, passed))).

Attack:

% 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.

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:

% 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.

capability_active(CapID, true) :-
    capability_issued(CapID, _, _, _, _, IssuedAt, ExpiresAt),
    \+ capability_revoked(CapID, _),  % Negation-as-failure
    ...

Scenario:

% 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).

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.

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.

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