AI编码用形式验证防越权漏洞
推荐指数 68.0 NO. 010 · 2026.05.21
发布2026/05/20Score68Comments11
为什么值得看
文章提出用形式验证门控替代更智能的Agent来解决AI编码中的安全漏洞问题，核心思路是通过结构化的系统约束（如类型系统、访问控制层）而非依赖模型每次正确推理。对正在用AI辅助编码的团队有直接参考价值，尤其是多租户系统和权限敏感场景。
媒体预览
编辑判断
这篇文章切中了当前AI编程工具的一个盲区：大家都在卷模型智能度，却忽视了系统架构层面的防护。Cursor、Windsurf这类工具把安全规则放在prompt里，本质和过去把权限校验写在业务代码里一样脆弱。
作者提出的"结构背压"思路——用编译器类型系统、数据库行级安全策略等不可绕过的机制来兜底——实际上是把DevSecOps的"shift left"原则推进到了AI生成代码的场景。如果你在用AI生成多租户应用的CRUD代码，建议优先投资数据库层的RLS和API网关的强制鉴权，而不是调prompt让模型"记得检查权限"。
这篇只有68分11评论的HN帖子，讨论质量却很高，说明真正做过生产系统的人对此有共鸣。
社区反馈
意见分歧 11 条评论
核心争论：形式验证门控是否优于直接采用更强类型语言，以及约束强度与实用性的权衡
Author here. The TL;DR: move rules from prompts into types the compiler refuses to violate, then bounce the AI coding loop off those refusals. The repo is github.com/pyrex41/Shen-Backpressure. Builds a lot on Geoff Huntley's backpressure idea -- none of this is rocket science, just an effo
Thank you, interesting work. Please, clarify what is possibly a naive question - your README states that the constraints imposed by your tool are weaker than the formal verification guarantees. Why not implement the backpressure as the full formal verification barrier? Too complex to implement?
TBH something like this sounds useful even without LLMs (although I haven't fully grokked this yet). The problem with the operational level is that you can't express the invariants etc at the type level - not least because you're working across multiple languages - so the kind of dumb issues that we