安全性
形式化验证。
不只是声称。
大多数安全声明只是被测试过。InferNode 的安全声明是被证明的。三种独立的形式化验证工具确认命名空间隔离在每一种可能的操作序列中都成立—数十亿状态,零违规。
架构
未授予的资源,
根本不存在。
每个智能体都运行在自己的命名空间内—一个完全由你显式交付的资源构成的世界视图。你的凭据、SSH 密钥、邮件和私有文件并非对智能体被隐藏,它们就是不在那里。无可寻觅。
这不是在传统操作系统之上加装的沙箱,而是 Plan 9 的原始设计,经过精炼并被形式化证明正确。隔离边界是结构性的—在内核层面强制执行,而不是靠策略或祈祷。
一次试图读取你 SSH 密钥的提示注入攻击,得到的回应与请求月球上的某个文件相同:那个路径根本不存在。
证明
三种工具,零违规。
形式化验证意味着检查每一种可能的状态,而不只是你想到要测试的那些。InferNode 使用三种互补的工具,各自捕获不同类别的缺陷。
抽象规约
TLA+ 在最高抽象层级建模命名空间,并穷举地证明隔离在每一个可达状态中都成立。核心定理:在命名空间复制之后挂载的资源,除非子命名空间显式挂载它,否则不会出现在子空间中。11 条不变量,零违规。
并发协议
SPIN 在并发访问下验证命名空间—多个线程在每一种可能的交错中同时运行。它检查死锁、竞争条件,以及智能体是否能通过文件系统遍历逃离它的容器。这些情况都不会发生。
真实的内核代码
CBMC 直接在真实的 C 源码上验证属性—不是它的模型。数组边界、整数运算与隔离保证在真实的内核实现中得到检查。113 条断言,零失败。每次提交都会自动运行。
密码学
为后量子时代而设计。
抗量子加密
实验性InferNode 已经初步实现了 NIST 标准化的后量子算法—ML-KEM 用于密钥交换,ML-DSA 用于数字签名—这正是业界正在迁移的算法。两者都基于格、抗量子攻击,并原生运行在保护你智能体的同一套轻量级操作系统之上。
该实现尚不建议用于生产,但密码敏捷性是一项首要设计目标。当传统公钥密码学被攻破之时,InferNode 已经准备好了一条出路。