trending/OpenShell
1
0
Fork 0
mirror of https://github.com/NVIDIA/OpenShell.git synced 2026-10-22 06:19:47 +08:00
Code Issues Packages Projects Releases Wiki Activity

refactor(prover): simplify to two Zelkova-like verification queries

Browse Source 
Narrow OPP to two yes/no security questions:
1. Can data leave this sandbox? (exfiltration)
2. Can the agent write despite read-only intent? (write bypass)

Removes 4 advisory/lint queries (overpermissive methods, L4 gaps,
binary inheritance, inference relay), 3 output modes (Mermaid,
topology, HTML), and fixes 3 bugs (include_workdir not used in
exfil analysis, __all__ broken when protos missing, CLI PYTHONPATH).

~40% line reduction (2900 -> 1769 lines).

Signed-off-by: Alexander Watson <zredlined@gmail.com>
This commit is contained in:
Alexander Watson
2026-03-31 11:12:44 -07:00
parent 0aaba52249
commit b9fc0d3b8d
9 changed files with 114 additions and 1597 deletions
Download Patch File Download Diff File Expand all files Collapse all files
python/openshell/__init__.py
+4 -3
View File
@@ -10,7 +10,7 @@ import contextlib
# Proto stubs may not be generated yet (requires Rust build).
# Suppress so subpackages like openshell.prover can still be imported.
with contextlib.suppress(ImportError):
from .sandbox import (
from .sandbox import ( # noqa: F401 — intentional re-exports
ClusterInferenceConfig,
ExecChunk,
ExecResult,
@@ -30,7 +30,7 @@ try:
except Exception:
__version__ = "0.0.0"
__all__ = [
_SDK_SYMBOLS = [
"ClusterInferenceConfig",
"ExecChunk",
"ExecResult",
@@ -41,5 +41,6 @@ __all__ = [
"SandboxRef",
"SandboxSession",
"TlsConfig",
"__version__",
]
__all__ = [s for s in _SDK_SYMBOLS if s in dir()] + ["__version__"]
python/openshell/prover/accepted_risks.py
+1 -18
View File
@@ -20,7 +20,6 @@ if TYPE_CHECKING:
class AcceptedRisk:
query: str
reason: str
accepted_by: str = ""
binary: str = ""
endpoint: str = ""
@@ -34,7 +33,6 @@ def load_accepted_risks(path: Path) -> list[AcceptedRisk]:
AcceptedRisk(
query=r.get("query", ""),
reason=r.get("reason", ""),
accepted_by=r.get("accepted_by", ""),
binary=r.get("binary", ""),
endpoint=r.get("endpoint", ""),
)
@@ -45,7 +43,7 @@ def load_accepted_risks(path: Path) -> list[AcceptedRisk]:
def _path_matches_risk(path, risk: AcceptedRisk) -> bool:
"""Check if a single finding path matches an accepted risk."""
if risk.binary:
path_binary = getattr(path, "binary", "") or getattr(path, "parent", "")
path_binary = getattr(path, "binary", "")
if path_binary != risk.binary:
return False
@@ -77,21 +75,6 @@ def apply_accepted_risks(
result.append(finding)
continue
if not finding.paths:
# Pathless finding (e.g., inference relay) — accept if query matches
accepted_finding = Finding(
query=finding.query,
title=finding.title,
description=finding.description,
risk=finding.risk,
paths=finding.paths,
remediation=finding.remediation,
accepted=True,
accepted_reason=matching_risks[0].reason,
)
result.append(accepted_finding)
continue
unmatched_paths = []
matched_reason = ""
for path in finding.paths:
python/openshell/prover/cli.py
+4 -60
View File
@@ -15,7 +15,7 @@ from .binary_registry import load_binary_registry
from .credential_loader import load_credential_set
from .policy_parser import parse_policy
from .queries import run_all_queries
from .report import render_report
from .report import render_compact, render_report
from .z3_model import build_model
_DEFAULT_REGISTRY = Path(__file__).parent / "registry"
@@ -59,29 +59,7 @@ def main():
verify_parser.add_argument(
"--compact",
action="store_true",
help="One-line-per-finding output (for demos and CI)",
)
verify_parser.add_argument(
"--color",
action="store_true",
help="Force colored output even when piped",
)
verify_parser.add_argument(
"--mermaid",
action="store_true",
help="Output Mermaid findings graph (risk paths by query type)",
)
verify_parser.add_argument(
"--mermaid-topology",
action="store_true",
help="Output Mermaid policy topology map (all endpoints, binaries, enforcement levels)",
)
verify_parser.add_argument(
"--html",
type=Path,
default=None,
metavar="PATH",
help="Output self-contained HTML report with interactive diagrams (e.g., --html report.html)",
help="One-line-per-finding output (for CI)",
)
args = parser.parse_args()
@@ -97,9 +75,8 @@ def main():
def cmd_prove(args) -> int:
"""Execute the prove command."""
console = Console(force_terminal=args.color) if args.color else Console()
console = Console()
# Load inputs
try:
policy = parse_policy(args.policy)
except Exception as e:
@@ -118,13 +95,9 @@ def cmd_prove(args) -> int:
console.print(f"[red]Error loading binary registry: {e}[/red]")
return 2
# Build model
model = build_model(policy, credential_set, binary_registry)
# Run queries
findings = run_all_queries(model)
# Apply accepted risks
if args.accepted_risks:
try:
from .accepted_risks import apply_accepted_risks, load_accepted_risks
@@ -135,36 +108,7 @@ def cmd_prove(args) -> int:
console.print(f"[red]Error loading accepted risks: {e}[/red]")
return 2
# Render
has_critical_high = any(
f.risk.value in ("critical", "high") and not f.accepted for f in findings
)
if args.html:
from .report import render_html
exit_code = render_html(
findings,
str(args.policy),
str(args.credentials),
policy,
binary_registry,
args.html,
)
console.print(f"Report written to {args.html}")
return exit_code
elif args.mermaid_topology:
from .report import generate_mermaid_topology
print(generate_mermaid_topology(policy, binary_registry, findings))
return 1 if has_critical_high else 0
elif args.mermaid:
from .report import generate_mermaid
print(generate_mermaid(findings))
return 1 if has_critical_high else 0
elif args.compact:
from .report import render_compact
if args.compact:
return render_compact(
findings,
str(args.policy),
python/openshell/prover/policy_parser.py
+6 -1
View File
@@ -113,12 +113,16 @@ class NetworkPolicyRule:
@dataclass
class FilesystemPolicy:
include_workdir: bool = True
workdir: str = "/sandbox"
read_only: list[str] = field(default_factory=list)
read_write: list[str] = field(default_factory=list)
@property
def readable_paths(self) -> list[str]:
return self.read_only + self.read_write
paths = self.read_only + self.read_write
if self.include_workdir and self.workdir not in paths:
paths = [self.workdir, *paths]
return paths
@dataclass
@@ -170,6 +174,7 @@ def parse_policy(path: Path) -> PolicyModel:
fs_raw = raw.get("filesystem_policy", {}) or {}
fs = FilesystemPolicy(
include_workdir=fs_raw.get("include_workdir", True),
workdir=fs_raw.get("workdir", "/sandbox"),
read_only=fs_raw.get("read_only", []),
read_write=fs_raw.get("read_write", []),
)
python/openshell/prover/prover_test.py
+29 -16
View File
@@ -7,7 +7,7 @@ from pathlib import Path
from openshell.prover.binary_registry import load_binary_registry
from openshell.prover.credential_loader import load_credential_set
from openshell.prover.policy_parser import PolicyIntent, parse_policy
from openshell.prover.policy_parser import FilesystemPolicy, PolicyIntent, parse_policy
from openshell.prover.queries import RiskLevel, run_all_queries
from openshell.prover.z3_model import build_model
@@ -33,13 +33,11 @@ def test_parse_policy():
assert len(rule.endpoints) == 2
assert len(rule.binaries) == 3
# First endpoint: L7 enforced read-only
ep0 = rule.endpoints[0]
assert ep0.host == "api.github.com"
assert ep0.is_l7_enforced
assert ep0.intent == PolicyIntent.READ_ONLY
# Second endpoint: L4 only
ep1 = rule.endpoints[1]
assert ep1.host == "github.com"
assert not ep1.is_l7_enforced
@@ -47,13 +45,33 @@ def test_parse_policy():
def test_filesystem_policy():
"""Verify filesystem policy parsing."""
"""Verify filesystem policy parsing including workdir."""
policy = parse_policy(_TESTDATA / "policy.yaml")
fs = policy.filesystem_policy
assert "/usr" in fs.read_only
assert "/sandbox" in fs.read_write
assert "/usr" in fs.readable_paths
assert "/sandbox" in fs.readable_paths
assert "/usr" in fs.readable_paths
def test_include_workdir_default():
"""Workdir is included in readable_paths by default."""
fs = FilesystemPolicy(read_only=["/usr"])
assert "/sandbox" in fs.readable_paths
assert "/usr" in fs.readable_paths
def test_include_workdir_false():
"""Workdir excluded when include_workdir is False."""
fs = FilesystemPolicy(include_workdir=False, read_only=["/usr"])
assert "/sandbox" not in fs.readable_paths
assert "/usr" in fs.readable_paths
def test_include_workdir_no_duplicate():
"""Workdir not duplicated if already in read_write."""
fs = FilesystemPolicy(read_write=["/sandbox"])
assert fs.readable_paths.count("/sandbox") == 1
def test_git_push_bypass_findings():
@@ -66,7 +84,9 @@ def test_git_push_bypass_findings():
assert RiskLevel.HIGH in risks, "Should detect write bypass"
assert "data_exfiltration" in queries
assert "write_bypass" in queries
assert "binary_inheritance" in queries
# Only 2 query types in v1
assert len(queries) == 2
# Verify git bypass specifically detected
write_findings = [f for f in findings if f.query == "write_bypass"]
@@ -75,14 +95,7 @@ def test_git_push_bypass_findings():
assert "/usr/bin/git" in bypass_binaries, "Git should be flagged for L7 bypass"
def test_empty_policy_advisory_only():
"""Deny-all policy should only produce the inference relay advisory."""
def test_empty_policy_no_findings():
"""Deny-all policy should produce no findings."""
findings = _run_prover("empty_policy.yaml", "empty_credentials.yaml")
queries = {f.query for f in findings}
risks = {f.risk for f in findings}
assert "inference_relay" in queries
assert RiskLevel.CRITICAL not in risks
assert RiskLevel.HIGH not in risks
assert len(findings) == 1
assert findings[0].risk == RiskLevel.ADVISORY
assert len(findings) == 0
python/openshell/prover/queries.py
+17 -350
View File
@@ -1,7 +1,11 @@
# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
# SPDX-License-Identifier: Apache-2.0
"""Verification queries that ask reachability questions against the Z3 model."""
"""Verification queries — two Zelkova-like yes/no security questions.
1. Can data leave this sandbox? (exfiltration)
2. Can the agent write despite read-only intent? (write bypass)
"""
from __future__ import annotations
@@ -18,11 +22,8 @@ if TYPE_CHECKING:
class RiskLevel(Enum):
LOW = "low"
MEDIUM = "medium"
HIGH = "high"
CRITICAL = "critical"
ADVISORY = "advisory"
@dataclass
@@ -46,49 +47,10 @@ class WriteBypassPath:
endpoint_port: int
policy_name: str
policy_intent: str
bypass_reason: str # "l4_only", "l7_bypass_protocol", "credential_write_scope"
bypass_reason: str # "l4_only", "l7_bypass_protocol"
credential_actions: list[str] = field(default_factory=list)
@dataclass
class InheritancePath:
"""A binary that inherits network access through the ancestor chain."""
parent: str
child: str
endpoint_host: str
endpoint_port: int
child_capabilities: list[str]
@dataclass
class OverpermissiveMethodPath:
"""An endpoint where wildcard or overly broad HTTP methods are allowed."""
endpoint_host: str
endpoint_port: int
policy_name: str
binary: str
allowed_methods: str # e.g. "*" or "GET, POST, PUT, PATCH, DELETE"
needed_methods: str # e.g. "POST" — what the endpoint likely needs
excess_methods: str # e.g. "DELETE, PUT, PATCH" — what's unnecessary
risk_detail: str # why the excess matters
@dataclass
class L4PolicyGapPath:
"""An endpoint missing L7 enforcement where HTTP-capable binaries have access."""
endpoint_host: str
endpoint_port: int
policy_name: str
binary: str
binary_can_http: bool
binary_bypasses_l7: bool
has_sibling_l7: bool # True if other endpoints in same policy group have L7
detail: str
@dataclass
class Finding:
"""A single verification finding."""
@@ -97,20 +59,18 @@ class Finding:
title: str
description: str
risk: RiskLevel
paths: list[
ExfilPath
| WriteBypassPath
| InheritancePath
| OverpermissiveMethodPath
| L4PolicyGapPath
] = field(default_factory=list)
paths: list[ExfilPath | WriteBypassPath] = field(default_factory=list)
remediation: list[str] = field(default_factory=list)
accepted: bool = False
accepted_reason: str = ""
def check_data_exfiltration(model: ReachabilityModel) -> list[Finding]:
"""Check for data exfiltration paths from readable filesystem to writable egress channels."""
"""Can data leave this sandbox?
Maps every path from readable filesystem locations to writable egress
channels: L4-only endpoints, wire protocol bypasses, and L7 write channels.
"""
findings = []
if not model.policy.filesystem_policy.readable_paths:
@@ -125,13 +85,11 @@ def check_data_exfiltration(model: ReachabilityModel) -> list[Finding]:
for eid in model.endpoints:
expr = model.can_exfil_via_endpoint(bpath, eid)
# Use a fresh solver to check each path independently
s = z3.Solver()
s.add(model.solver.assertions())
s.add(expr)
if s.check() == z3.sat:
# Determine the mechanism
ek = eid.key
bypass = cap.bypasses_l7
@@ -210,7 +168,11 @@ def check_data_exfiltration(model: ReachabilityModel) -> list[Finding]:
def check_write_bypass(model: ReachabilityModel) -> list[Finding]:
"""Check for write capabilities that bypass read-only policy intent."""
"""Can the agent write despite read-only intent?
Checks whether any combination of binary capabilities, credential scopes,
and transport protocols allows write operations that the policy intends to block.
"""
findings = []
bypass_paths: list[WriteBypassPath] = []
@@ -305,304 +267,9 @@ def check_write_bypass(model: ReachabilityModel) -> list[Finding]:
return findings
def check_binary_inheritance(model: ReachabilityModel) -> list[Finding]:
"""Check for binaries that inherit network access through the ancestor chain."""
findings = []
inheritance_paths: list[InheritancePath] = []
for bpath in model.binary_paths:
children = model.binary_registry.transitive_spawns(bpath)
if not children:
continue
for eid in model.endpoints:
access_key = f"{bpath}:{eid.key}"
if access_key not in model.policy_allows:
continue
for child in children:
child_cap = model.binary_registry.get_or_unknown(child)
capabilities = []
if child_cap.can_write:
capabilities.append("can_write")
if child_cap.bypasses_l7:
capabilities.append("bypasses_l7")
if child_cap.can_exfiltrate:
capabilities.append("can_exfiltrate")
if child_cap.can_construct_http:
capabilities.append("can_construct_http")
if capabilities:
inheritance_paths.append(
InheritancePath(
parent=bpath,
child=child,
endpoint_host=eid.host,
endpoint_port=eid.port,
child_capabilities=capabilities,
)
)
if inheritance_paths:
seen = set()
deduped = []
for ip in inheritance_paths:
key = (ip.parent, ip.child)
if key not in seen:
seen.add(key)
deduped.append(ip)
findings.append(
Finding(
query="binary_inheritance",
title="Binary Ancestor Chain — Transitive Access Inheritance",
description=(
f"{len(deduped)} binary pair(s) where child processes inherit "
f"network access from parent binaries via ancestor matching."
),
risk=RiskLevel.MEDIUM,
paths=deduped,
remediation=[
"Review which child processes are spawned by allowed binaries.",
"If a child binary (e.g., git, curl) has write or L7-bypass capabilities "
"that exceed the policy intent, consider removing the parent binary or "
"restricting it to a more specific binary path.",
],
)
)
return findings
def check_inference_relay(_model: ReachabilityModel) -> list[Finding]:
"""Flag inference.local as a potential side channel for policy bypass."""
return [
Finding(
query="inference_relay",
title="Inference Relay — inference.local Bypasses Policy",
description=(
"inference.local is always reachable from within the sandbox and bypasses "
"OPA policy evaluation entirely. If the backing model supports tool use "
"or function calling, the agent may instruct it to access external services, "
"creating a side channel outside the policy boundary."
),
risk=RiskLevel.ADVISORY,
paths=[],
remediation=[
"Verify that the inference backend does not support unrestricted tool use "
"or code execution.",
"If using tool-use models, ensure the inference router restricts which tools "
"are available and what external access they can perform.",
"Consider auditing inference.local traffic for unexpected patterns.",
],
)
]
def check_overpermissive_methods(model: ReachabilityModel) -> list[Finding]:
"""Flag endpoints using wildcard or overly broad HTTP method rules."""
endpoint_hints: dict[str, tuple[set[str], str]] = {
"integrate.api.nvidia.com": (
{"POST"},
"NVIDIA Cloud Functions management APIs (DELETE /v2/nvcf/assets, "
"DELETE /v2/nvcf/deployments) share this host",
),
"inference-api.nvidia.com": (
{"POST"},
"Inference endpoint — only POST to completion paths is needed",
),
"api.anthropic.com": (
{"POST"},
"Anthropic management APIs (DELETE /v1/files, DELETE /v1/skills) share this host",
),
"statsig.anthropic.com": (
{"POST"},
"Telemetry endpoint — only POST to ingest paths is needed",
),
"sentry.io": (
{"POST"},
"Error reporting — only POST to ingest paths is needed; "
"Sentry management APIs (DELETE projects, releases) share this host",
),
"registry.npmjs.org": (
{"GET"},
"Package installation is read-only (GET); wildcard allows npm publish (PUT)",
),
}
paths: list[OverpermissiveMethodPath] = []
for policy_name, rule in model.policy.network_policies.items():
for ep in rule.endpoints:
if not ep.is_l7_enforced:
continue
allowed = ep.allowed_methods
if not allowed:
continue
has_wildcard = any(r.method == "*" for r in ep.rules)
has_delete = "DELETE" in allowed
if not has_wildcard and not has_delete:
continue
hint = endpoint_hints.get(ep.host)
if hint:
needed, risk_detail = hint
excess = allowed - needed - {"HEAD", "OPTIONS"}
else:
if not has_delete:
continue
needed = allowed - {"DELETE"}
excess = {"DELETE"}
risk_detail = "DELETE method allowed but likely not required"
if not excess:
continue
for b in rule.binaries:
for port in ep.effective_ports:
paths.append(
OverpermissiveMethodPath(
endpoint_host=ep.host,
endpoint_port=port,
policy_name=policy_name,
binary=b.path,
allowed_methods="*"
if has_wildcard
else ", ".join(sorted(allowed)),
needed_methods=", ".join(sorted(needed)),
excess_methods=", ".join(sorted(excess)),
risk_detail=risk_detail,
)
)
if not paths:
return []
unique_endpoints = {
(p.endpoint_host, p.endpoint_port, p.policy_name) for p in paths
}
return [
Finding(
query="overpermissive_methods",
title="Overpermissive HTTP Methods — Destructive Operations Allowed",
description=(
f"{len(unique_endpoints)} endpoint(s) allow HTTP methods beyond what is needed. "
f'Wildcard (method: "*") or explicit DELETE on endpoints that share hosts with '
f"management APIs enables destructive operations."
),
risk=RiskLevel.HIGH,
paths=paths,
remediation=[
'Replace `method: "*"` with explicit method lists matching actual usage.',
"Inference endpoints: restrict to `POST` on `/v1/chat/completions`, "
"`/v1/messages`, `/v1/responses`.",
"Telemetry endpoints: restrict to `POST` on known ingest paths.",
"Package registries: restrict to `GET` for installation (no publish).",
],
)
]
def check_l4_policy_gaps(model: ReachabilityModel) -> list[Finding]:
"""Flag endpoints without L7 enforcement where HTTP-capable binaries have access."""
paths: list[L4PolicyGapPath] = []
for policy_name, rule in model.policy.network_policies.items():
has_any_l7 = any(ep.is_l7_enforced for ep in rule.endpoints)
for ep in rule.endpoints:
if ep.is_l7_enforced:
continue
for b in rule.binaries:
cap = model.binary_registry.get_or_unknown(b.path)
if not (
cap.can_construct_http or cap.bypasses_l7 or cap.can_exfiltrate
):
continue
detail_parts = []
if has_any_l7:
l7_siblings = [
f"{sib.host}:{sib.effective_ports[0]}"
for sib in rule.endpoints
if sib.is_l7_enforced and sib.effective_ports
]
detail_parts.append(
f"Inconsistent: sibling endpoint(s) {', '.join(l7_siblings)} "
f"in '{policy_name}' have L7, but this one does not"
)
if cap.can_construct_http:
detail_parts.append(
f"{b.path} can construct arbitrary HTTP — all methods/paths "
f"pass uninspected"
)
if cap.bypasses_l7:
detail_parts.append(
f"{b.path} uses non-HTTP protocol — even with L7, "
f"traffic would bypass inspection"
)
for port in ep.effective_ports:
paths.append(
L4PolicyGapPath(
endpoint_host=ep.host,
endpoint_port=port,
policy_name=policy_name,
binary=b.path,
binary_can_http=cap.can_construct_http,
binary_bypasses_l7=cap.bypasses_l7,
has_sibling_l7=has_any_l7,
detail="; ".join(detail_parts),
)
)
if not paths:
return []
has_inconsistent = any(p.has_sibling_l7 for p in paths)
unique_endpoints = {(p.endpoint_host, p.endpoint_port) for p in paths}
return [
Finding(
query="l4_policy_gaps",
title="L4-Only Endpoints — No HTTP Inspection",
description=(
f"{len(unique_endpoints)} endpoint(s) lack `protocol: rest` — all traffic "
f"passes without HTTP method or path enforcement. "
+ (
"Some share a policy group with L7-enforced siblings, indicating "
"inconsistent enforcement."
if has_inconsistent
else "HTTP-capable binaries have unrestricted access."
)
),
risk=RiskLevel.HIGH if has_inconsistent else RiskLevel.MEDIUM,
paths=paths,
remediation=[
"Add `protocol: rest` with `enforcement: enforce` and `tls: terminate` "
"to enable HTTP inspection.",
'Define explicit method and path rules (e.g., `allow: { method: GET, path: "/**" }`) '
"to restrict what traffic is permitted.",
"If L4-only is intentional (e.g., for binary protocols like git), "
"document the rationale and restrict the binary list tightly.",
],
)
]
def run_all_queries(model: ReachabilityModel) -> list[Finding]:
"""Run all verification queries and return findings."""
findings = []
findings.extend(check_data_exfiltration(model))
findings.extend(check_write_bypass(model))
findings.extend(check_overpermissive_methods(model))
findings.extend(check_l4_policy_gaps(model))
findings.extend(check_binary_inheritance(model))
findings.extend(check_inference_relay(model))
return findings
python/openshell/prover/report.py
+20 -1010
View File
File diff suppressed because it is too large Load Diff