From 8ba9e26b3741a01f7b6eb2c18fc0d65e3712423d Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Tue, 31 Mar 2026 13:40:51 -0700 Subject: [PATCH] refactor(prover): focus exfil on enforcement gaps, drop inheritance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Only report exfiltration paths where enforcement diverges from intent: - L4-only endpoints (no HTTP inspection) - Wire protocol bypasses (L7 exists but binary circumvents it) L7-enforced endpoints where POST is explicitly allowed are the policy working as designed, not findings. Remove binary inheritance from the Z3 model — transitive spawn chain access produced noise (git inheriting access to api.telegram.org via node). Direct policy grants only. Inheritance can return later as an opt-in extended analysis mode. NemoClaw default policy: 38 findings -> 9 actionable gaps. Signed-off-by: Alexander Watson --- python/openshell/prover/queries.py | 7 ++- .../prover/testdata/nemoclaw-credentials.yaml | 48 +++++++++++++++++++ python/openshell/prover/z3_model.py | 38 +-------------- 3 files changed, 53 insertions(+), 40 deletions(-) create mode 100644 python/openshell/prover/testdata/nemoclaw-credentials.yaml diff --git a/python/openshell/prover/queries.py b/python/openshell/prover/queries.py index a43632ee1..02cff0c3c 100644 --- a/python/openshell/prover/queries.py +++ b/python/openshell/prover/queries.py @@ -109,10 +109,9 @@ def check_data_exfiltration(model: ReachabilityModel) -> list[Finding]: l7_status = "l4_only" mechanism = f"L4-only endpoint — no HTTP inspection, {bpath} can send arbitrary data" else: - l7_status = "l7_allows_write" - mechanism = ( - f"L7 allows write methods — {bpath} can POST/PUT data" - ) + # L7 is enforced and allows write — policy is + # working as intended. Not a finding. + continue if cap.exfil_mechanism: mechanism += f". Exfil via: {cap.exfil_mechanism}" diff --git a/python/openshell/prover/testdata/nemoclaw-credentials.yaml b/python/openshell/prover/testdata/nemoclaw-credentials.yaml new file mode 100644 index 000000000..092fdc0e0 --- /dev/null +++ b/python/openshell/prover/testdata/nemoclaw-credentials.yaml @@ -0,0 +1,48 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +credentials: + - name: github-pat + type: github-pat + scopes: + - repo + injected_via: GITHUB_TOKEN + target_hosts: + - api.github.com + - github.com + + - name: nvidia-api-key + type: api-key + scopes: + - inference + - nvcf-management + injected_via: NVIDIA_API_KEY + target_hosts: + - integrate.api.nvidia.com + - inference-api.nvidia.com + + - name: anthropic-api-key + type: api-key + scopes: + - inference + injected_via: ANTHROPIC_API_KEY + target_hosts: + - api.anthropic.com + + - name: telegram-bot-token + type: bot-token + scopes: + - bot + injected_via: TELEGRAM_BOT_TOKEN + target_hosts: + - api.telegram.org + + - name: discord-bot-token + type: bot-token + scopes: + - bot + injected_via: DISCORD_BOT_TOKEN + target_hosts: + - discord.com + - gateway.discord.gg + - cdn.discordapp.com diff --git a/python/openshell/prover/z3_model.py b/python/openshell/prover/z3_model.py index 2ed161f03..e649f17e4 100644 --- a/python/openshell/prover/z3_model.py +++ b/python/openshell/prover/z3_model.py @@ -61,10 +61,6 @@ class ReachabilityModel: credential_has_write: dict[str, z3.BoolRef] = field(default_factory=dict) # credential_has_destructive[host] = True if any credential has destructive capabilities credential_has_destructive: dict[str, z3.BoolRef] = field(default_factory=dict) - # spawns[parent:child] = True if parent spawns child - spawns_rel: dict[str, z3.BoolRef] = field(default_factory=dict) - # inherits_access[child:endpoint_key] = True if child inherits access to endpoint - inherits_access: dict[str, z3.BoolRef] = field(default_factory=dict) # filesystem_readable[path] = True filesystem_readable: dict[str, z3.BoolRef] = field(default_factory=dict) @@ -81,7 +77,6 @@ class ReachabilityModel: self._encode_l7_enforcement() self._encode_binary_capabilities() self._encode_credentials() - self._encode_spawn_chains() self._encode_filesystem() def _index_endpoints(self): @@ -191,28 +186,6 @@ class ReachabilityModel: self.credential_has_destructive[host] = cd_var self.solver.add(cd_var == has_destructive) - def _encode_spawn_chains(self): - """Encode binary spawn relationships and transitive access inheritance.""" - for bpath in self.binary_paths: - cap = self.binary_registry.get_or_unknown(bpath) - for child in cap.spawns: - key = f"{bpath}:{child}" - var = z3.Bool(f"spawns_{key}") - self.spawns_rel[key] = var - self.solver.add(var == True) # noqa: E712 - - # Encode transitive access inheritance - for bpath in self.binary_paths: - all_children = self.binary_registry.transitive_spawns(bpath) - for eid in self.endpoints: - parent_key = f"{bpath}:{eid.key}" - if parent_key in self.policy_allows: - for child in all_children: - inherit_key = f"{child}:{eid.key}" - var = z3.Bool(f"inherits_access_{inherit_key}") - self.inherits_access[inherit_key] = var - self.solver.add(var == True) # noqa: E712 - def _encode_filesystem(self): """Encode filesystem readability.""" for path in self.policy.filesystem_policy.readable_paths: @@ -223,15 +196,8 @@ class ReachabilityModel: # --- Query helpers --- def _has_access(self, bpath: str, ek: str) -> z3.BoolRef | None: - """Return Z3 expression for access (direct or inherited), or None.""" - access_key = f"{bpath}:{ek}" - direct = self.policy_allows.get(access_key) - inherited = self.inherits_access.get(access_key) - if direct is not None and inherited is not None: - return z3.Or(direct, inherited) - if direct is not None: - return direct - return inherited # may be None + """Return Z3 expression for direct policy access, or None.""" + return self.policy_allows.get(f"{bpath}:{ek}") def can_write_to_endpoint(self, bpath: str, eid: EndpointId) -> z3.BoolRef: """Return a Z3 expression for whether a binary can write to an endpoint."""