AI安全

OpenShell 用形式化方法审权限，证明的边界仍取决于模型

在 OpenShell 团队的研究文章中，研究者尝试把 Agent 提出的权限变化编码为逻辑约束，再用 Z3 判断它是否超出预先批准的安全基线。文章同时讲述了一次演示中，凭据与另一种网络访问方式组合后绕过既有检查的教训。