【免费下载链接】OpenShellOpenShell is the safe, private runtime for autonomous AI agents.项目地址https://gitcode.com/gh_mirrors/op/OpenShell点击查看免费下载openshell-prover是 OpenShell 项目提供的独立可执行文件用于在本地验证一份完全组合后的候选策略是否被限制在运维人员设定的边界策略之内。它以openshell-prover-clicrate 形式构建是一个围绕openshell-prover可复用包含引擎containment engine的薄同步适配层自身只负责本地文件加载、命令行解析、结果渲染与进程退出码管理。读完本文你将掌握openshell-prover check的完整用法、五类退出码与 JSON 结果契约、内置测试场景以及把该命令接入 CI 与沙箱策略评审流程的实操方案。一、工具定位它是干什么的又刻意不做什么从 openshell-prover-cli/README.md 的定义看这个包构建的是独立命令openshell-prover其核心职责只有一个检查一份完全组合后的候选策略candidate policy是否始终处于运维方提供的边界策略boundary policy之内。两条最典型的调用方式openshell-prover check candidate.yaml --boundary boundary.yaml openshell-prover check candidate.yaml --boundary boundary.yaml --output json需要特别强调的是该命令的职责边界它不会去发现网关gateway、不会获取策略状态、也不会应用任何策略变更。它纯粹是一个本地文件到本地文件的静态形式化验证工具。这一点与openshell-provercrate 内部的另一套提案风险proposal-risk查询 API 形成对比——后者由网关在自动审批流程中使用而 CLI 只包装独立于网关的包含检查containmentAPI。从 openshell-prover-cli/src/main.rs 的check实现可以看出完整调用链读取候选策略文件 → 读取边界策略文件 → 分别用parse_policy_str解析 → 调用openshell_prover::containment::check_within_boundary_cancellable求解 → 包装结果信封envelope→ 按 text/json 格式渲染并返回退出码。整个过程不依赖任何网络连接。二、安装与构建标准 OpenShell 安装器会一并提供openshell-provercurl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | sh openshell-prover --version如果你只需要独立二进制也可以直接取发布产物参见 docs/reference/policy-prover.mdx 中的支持矩阵说明。发布归档内已包含求解器所需的链接Z3不要求预先安装主openshell命令、网关配置或单独的 Z3 环境。从源码构建与测试该包cargo build -p openshell-prover-cli --bin openshell-prover cargo test -p openshell-prover-cli从 Cargo.toml 可以看到该 crate 依赖openshell-prover路径依赖、clap命令行解析、serde/serde_jsonJSON 渲染并在 Unix 平台额外依赖nix与signal-hook用于 SIGINT 优雅取消处理。它还提供了bundled-z3与prebuilt-z3两个特性用于控制 Z3 求解器的链接方式。三、命令语法与参数详解openshell-prover目前只有一个子命令check其参数定义见 src/main.rs参数说明默认值candidate位置参数完全组合后的生效候选策略文件路径即变更后的完整有效策略须包含 provider 贡献的授权必填--boundary FILE运维方拥有的边界策略文件路径它本身不授予任何权限只作为上限必填--output text\|json结果输出格式text--timeout duration求解器时间预算格式为正整数 ms/s/m后缀10s关于--timeout的解析细节见 src/main.rs 的parse_duration支持250ms、2s、3m这类写法0ms、无后缀的1、小数1.5s、负数、以及超过u32::MAX毫秒的值都会被拒绝对应的单元测试rejects_invalid_durations覆盖了这些边界。一个带超时与 JSON 输出的完整示例openshell-prover check candidate.yaml \ --boundary boundary.yaml \ --timeout 30s \ --output json无参数直接运行openshell-prover会打印帮助信息并以 0 退出对应show_help分支。四、退出码契约自动化集成的关键结果使用以下退出码见 README 表格及 src/main.rs 的result_envelope映射逻辑退出码含义0候选策略处于边界之内within_boundary仅当所有被建模域都证明包含时才成立1候选策略超出边界exceeds_boundary应检查反例counterexample2用法、输入、输出或内部错误error如参数缺失、文件打不开、策略语法错误3不支持的策略语义unsupported或无法得出结论的求解inconclusive130Unix 下按 Ctrl-C 中断inconclusivecancelled优雅退出时 JSON 输出仍会给出结论只有退出码0才算验证成功。在 CI 中unsupported与inconclusive都必须视为失败——这是fail-closed失败即关闭设计哲学的体现模型无法对策略形状做可靠推理时绝不静默放行。sigint_interrupts_the_check_with_exit_130测试见 crates/openshell-prover-cli/tests/cli.rs验证了 SIGINT 场景向正在求解的子进程发送SIGINT后进程以退出码130结束JSON 中result为inconclusive、reason_code为cancelled。该机制依赖signal_hook在 Unix 上注册的SIGINT处理器src/main.rs。五、JSON 结果契约面向机器的稳定输出当使用--output json时结果信封envelope包含以下字段定义见 src/main.rsschema_version数字版本号版本化JSON 结果契约本身prover_version产生该结果的实现版本取自CARGO_PKG_VERSIONcheck固定为boundarycoverage.domains机器可读的被建模域声明列表消费者必须检查它并确保所有与自身授权决策相关的域都在其中resultwithin_boundary/exceeds_boundary/unsupported/inconclusive/error之一exit_code数字退出码inputs候选与边界文件的路径counterexampleexceeds_boundary时为类型化反例对象否则为nullreason_codeerror/unsupported/inconclusive结果对应的稳定标识符否则为nullreason与reason_code配对的人类可读说明否则为null。自动化脚本应优先解析result与reason_code而不是去解析人类可读的reason文本。稳定的reason_code集合包括invalid_input、unsupported_policy_shape、unresolved_workdir、unresolved_binary_path、unresolved_filesystem_path、solver_timeout、solver_unknown、resource_limit、invalid_witness、cancelled。一个包含场景的稳定 JSON 输出形状被 contained_policy_returns_stable_json_and_zero 测试锁定{ schema_version: 1, check: boundary, result: within_boundary, exit_code: 0, coverage: { domains: [filesystem, network_l4, network_rest, process, landlock] }, counterexample: null }5.1 反例counterexample的四种域类型counterexample.domain决定反例对象的形状见 src/main.rs 的CounterexampleJson枚举以及 tests/cli.rs 中锁定的 JSON 形状域字段filesystemaccessread或write、pathprocessfieldrun_as_user或run_as_group、boundary、candidatelandlockboundary、candidate兼容模式networkbinary、ancestor_binary、binary_identity_required、host、destination_ip、trusted_gateway、port、protocol、method、path其中网络反例的binary/ancestor_binary在二进制身份强制关闭时为nullmethod/path对 L4 证据为nulltrusted_gateway: true表示证据使用了被认可的 host-gateway 别名绑定false表示普通目标校验。文本格式下这些反例会渲染成counterexample: process ...、counterexample: landlock ...、counterexample: filesystem ...、counterexample: network ...等单行输出。六、完整实操从边界策略到 CI 集成6.1 构造边界策略与候选策略边界策略是运维方设置的天花板自身不授予任何权限。创建一个boundary.yamlversion: 1 filesystem_policy: read_only: - /usr - /etc再创建一个被包含的候选candidate.yamlversion: 1 filesystem_policy: read_only: - /usr运行检查openshell-prover check candidate.yaml --boundary boundary.yaml会输出result: within_boundary并退出0这一组合正是 contained_policy_returns_stable_text_coverage_and_zero 测试覆盖的场景文本输出为result: within_boundary\ncoverage: domainsfilesystem,network_l4,network_rest,process,landlock\n。6.2 触发超出边界并阅读反例把candidate.yaml换成允许向/tmp写入的策略而边界并未授予任何写权限version: 1 filesystem_policy: read_only: - /usr read_write: - /tmpopenshell-prover check candidate.yaml --boundary boundary.yaml此时退出码为1JSON 模式下的反例类似对应 exceeding_policy_returns_counterexample_and_one{ result: exceeds_boundary, exit_code: 1, counterexample: { domain: filesystem, access: write, path: /tmp } }其他已锁定的反例形态还包括process域候选把run_as_user从sandbox改成root、landlock域候选把hard_requirement降级为best_effort、network域候选引入边界之外的 IPv6 目标2001:db8::。6.3 检查现有沙箱的生效策略要检查某个已存在沙箱的当前生效策略可先导出不包含展示性元数据再验证openshell sandbox get my-sandbox --policy-only candidate.yaml openshell-prover check candidate.yaml --boundary boundary.yaml注意两点导出内容包含 provider 贡献的规则而对于尚未生效的拟议变更你必须自行提供变更后的完整生效策略——独立证明器不会把基础策略与 provider 规则做组合。6.4 集成到 CI典型的 CI 流程可以是从候选分支提取策略 → 以运维仓库中受版本管理的boundary.yaml作为上限 → 运行openshell-prover check并遵循仅0为通过、2/3/130一律失败的判定。为了让失败原因可机器读取建议始终使用--output json并解析result、reason_code、coverage.domains与counterexample字段。七、输入校验与安全加固细节CLI 在读取文件阶段就做了多道防线见 read_policy仅接受普通文件通过metadata().is_file()双重检查打开前与打开后各一次拒绝 FIFO 等非常规输入。在 Unix 上还会用O_NONBLOCK打开以避免打开 FIFO 时在可取消之前挂死 CLI——fifo_input_is_rejected_without_blocking测试专门验证了这一行为4 MiB 输入上限MAX_POLICY_BYTES 4 * 1024 * 1024先检查文件长度再用Read::by_ref().take(MAX_POLICY_BYTES 1)读取并复核实际字节数防止 TOCTOU 竞态绕过rejects_oversized_policy_before_parsing测试验证了超限文件在解析前即被拒绝输入必须是合法 UTF-8文本诊断输出前会对控制字符做转义escape_terminal防止终端注入text_diagnostics_escape_terminal_controls测试验证了 ESC 被转义为\u{1b}输入错误在 JSON 模式下会渲染为result: error、reason_code: invalid_input、exit_code: 2的错误信封见render_input_error而不是写入 stderr——保证脚本只解析 stdout 即可获得全部信息。八、结果解读边界包含 ≠ 一切安好从 openshell-prover/README.md 与 docs/reference/policy-prover.mdx 的Interpretation and Limits章节必须理解包含检查的语义边界包含的含义Allowed(candidate)是被建模域下Allowed(boundary)的子集。它不建立最小权限、不意味着自动审批资格、不证明策略语义安全也不等同于运行中沙箱内核的真实状态成功只覆盖声明过的域消费者必须检查coverage.domains并确保与自身授权决策相关的每个域都在其中不支持的形状必须失败识别到覆盖范围之外但被 schema 认可的授权时返回unsupported退出码3而非静默忽略。两个输入文件共用与 OpenShell 运行时相同的受限 YAML/JSON 解析器未知字段、重复键、类型错误、受管理的metadata/review注解都会以invalid_input退出码2失败见canonical_schema_errors_fail_closed_in_both_inputs测试该测试把同样的非法输入分别放在 candidate 与 boundary 两侧验证资源上限在语义形状校验之前会先施加聚合限制——1,024 条网络规则、4,096 个端点、4,096 个二进制选择器、65,536 个端口条目、4,096 条allowed_ips、16,384 条 REST 规则、每个模式 4 KiB、模式文本总量 1 MiB。超过任一限制返回inconclusiveresource_limit退出码3。over_limit_mixed_protocol_policy_is_rejected_before_shape_validation测试用 5,000 个端点的策略验证了这一路径ASCII 与 NUL 限制网络二进制选择器、端点 host/path 选择器、REST allow/deny 的 method/path 选择器必须使用 ASCII 字面量非 ASCII 字面量返回unsupported_policy_shapenon_ascii_network_literals_are_unsupported_in_both_inputs测试验证了它在两侧输入中都以退出码3失败嵌入 NUL 字节同样不受支持embedded_nul_network_literal_is_unsupported_without_panicking。这是证明器模型限制而非通用策略校验规则——文件系统路径与无关策略文本保留原有 Unicode 行为进程与 Landlock 语义匹配的run_as_user/run_as_group值不会扩展配置把显式非 root 身份改成root/0返回exceeds_boundary并给出字段与两个值其他身份变更返回unsupportedCLI 不从沙箱镜像解析账户。Landlockhard_requirement不得降级为best_effort文件系统包含的保守性支持移除授权、以及在匹配路径上把写降级为只读边界对/的授权覆盖其他路径的同类访问其余跨路径比较返回unsupportedunresolved_filesystem_path——因为词法子路径可能通过符号链接解析到父目录之外无关路径也可能解析到同一对象symlink_descendants_require_sandbox_path_resolution测试正是用符号链接目录验证这一点。若边界根本没有授予该种访问新增访问即为exceeds_boundary运行时与环境依赖命令不在 CLI 所在主机上做 DNS 解析依赖镜像 workdir 等环境上下文的授权在结果取决于缺失上下文时返回unsupportedL4 与强制 REST 端点重叠的策略返回unsupported检测选择依赖完整端点配置集。九、底层实现Z3 形式化验证模型openshell-provercrate 把策略 附加凭据集 二进制能力注册表编码为Z3 SMT 模型再运行可达性查询以发现评审者应当留意的凭据可达与能力变化。包含检查 APIopenshell_prover::containment独立于旧版提案风险模型只解析规范作者 schema 并在授权落入其不支持的包含模型时失败关闭见 containment.rs 的模块文档。CheckResult刻意封闭为四种状态Within、Exceeds、Unsupported、InconclusiveFilesystemAccess同样封闭为Read/Write。ReasonCode、CheckDomain、Protocol、Counterexample允许新增变体CheckOptions、CheckCoverage、WithinEvidence与既有反例变体允许新增字段——API 使用方应配合..与通配分支匹配把未知值视为 fail-closed 结果。Rust 源码兼容性与 CLI 的 JSON schema 契约是两回事后者由数字schema_version版本化prover_version标识产生结果的实现。十、测试矩阵行为即契约openshell-prover-cli的集成测试tests/cli.rs与tests/fixtures/下的 13 个 YAML 夹具共同锁定了 CLI 的对外行为包括help_and_version_succeed/bare_invocation_shows_help--help、--version、裸调用均成功contained_policy_returns_stable_json_and_zero/...text_coverage_and_zero包含结果的 JSON 与文本输出完全稳定exceeding_policy_returns_counterexample_and_one/counterexamples_have_stable_json_shapes超出结果与四类反例的 JSON 形状unsupported_policy_returns_reason_and_three/unsupported_network_surfaces_fail_closed_at_the_cli_boundary五种不被模型支持的网络形态把 REST 控件混入 L4、REST 无强制检查、GraphQL/JSON-RPC/MCP 超出初始模型全部在 CLI 边界 fail-closedusage_errors_return_two/removed_maximum_option_is_rejected/timeout_must_be_positive参数错误返回2已移除的--maximum选项被显式拒绝missing_json_mode_input_uses_error_envelope_and_two/invalid_json_mode_input_uses_error_envelope_and_two文件缺失与非法策略在 JSON 模式下都走error信封 退出码2fifo_input_is_rejected_without_blockingFIFO 输入在 2 秒内被拒绝且不阻塞sigint_interrupts_the_check_with_exit_130SIGINT 优雅取消退出码130。这份测试矩阵本身就是很好的行为即契约参考资料任何把openshell-prover集成进工具链的团队都可以对照这些用例建立自己的验收清单。十一、适用前提与限制说明本指南以当前仓库OpenShell 工作区中的代码与夹具为准命令、参数、退出码与 JSON 字段在发布版本间可能演进接入自动化时应以schema_version与--version输出为准openshell-prover需要 Z3 求解器链接发布归档已内置源码构建可用bundled-z3/prebuilt-z3特性控制该工具面向静态配置检查无法替代运行期代理proxy的强制执行代理是执行层证明器是变更评审层。延伸阅读openshell-prover-cli/README.md——本文所依据的包级文档docs/reference/policy-prover.mdx——安装、使用与解读的官方参考crates/openshell-prover/README.md——底层形式化验证引擎与提案风险查询 APIcrates/openshell-prover/src/containment.rs——包含检查核心实现与资源上限常量crates/openshell-prover-cli/src/main.rs——CLI 入口、参数解析、结果渲染与退出码映射crates/openshell-prover-cli/tests/cli.rs——行为契约测试矩阵docs/reference/policy-schema.mdx——完整的策略语言参考。赞分享【免费下载链接】OpenShellOpenShell is the safe, private runtime for autonomous AI agents.项目地址https://gitcode.com/gh_mirrors/op/OpenShell点击查看免费下载相关推荐OpenShell 策略形式化验证器openshell-prover深度解析Z3 可达性模型、四类风险判定与边界包含检查OpenShell 策略形式化验证器openshell prover深度解析Z3 可达性模型、四类风险判定与边界包含检查 导读 openshell pOpCore-Simplify30分钟搞定OpenCore EFI配置的终极解决方案OpCore Simplify30分钟搞定OpenCore EFI配置的终极解决方案 你是否曾经花费数小时甚至数天时间研究OpenCore配置手动调整数百个OpenShell RFC 0005 解读沙箱代理出站适配器模型Egress Adapter如何统一 CONNECT、Forward HTTP 与透明 TCP 的授权边界OpenShell RFC 0005 解读沙箱代理出站适配器模型Egress Adapter如何统一 CONNECT、Forward HTTP 与透明 T上一篇终极指南如何三步解决模拟人生1宽屏适配难题下一篇Xtreme Download Manager专业级下载加速与视频下载解决方案创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考
