协议状态机不再靠检索拼上下文：State-inferer按依赖切片喂给大模型，严格F值达95.2
核心概要
State-inferer把协议实现的状态机提取改成按程序依赖切片：从状态变量赋值出发，在系统依赖图上做有深度上限的前向与后向搜索，为每条状态转移切出一段紧凑代码交给大模型，再把RFC安全属性特化成该模型上的线性时序逻辑公式，用nuXmv模型检验。在TLS、IKEv2、SSH的七个开源实现上，其宏平均严格转移级F值为95.2，最强基线Codex为78.9；并发现四个此前未知漏洞，均已获得CVE或CNVD编号。
深度剖析
协议实现真正执行的状态机现在可以从源码里逐条转移地恢复出来，而且每条转移都带着对内部变量的守卫条件，而不只是收到什么消息。 此前的做法要么用静态分析，在大程序上遭遇路径爆炸；要么用动态学习，只能看到测试输入触达的行为；基于大模型的提取则受限于上下文窗口，并会漏掉依赖内部变量的转移。 在TLS、IKEv2、SSH的七个开源实现上，State-inferer的宏平均严格转移级F值为95.2，Codex为78.9，Claude Code为77.1，ProtocolGPT为46.2；忽略守卫条件后的骨架F值分别为99.2、88.6、88.3和67.5。
每条状态转移的代码上下文由程序切片给出，而不是按文本相似度检索出来的片段。 相似度检索只能取回提到目标状态变量的代码块，取不到跨函数、跨文件的调用链，于是转移的前置条件被丢掉，可达性也会判错。 从状态变量赋值节点出发，在系统依赖图上分别限制数据流深度8与控制流深度5做前向搜索，再对每个终点做对称后向搜索，两者交集加上起止节点构成一条转移的代码片段；WolfSSL TLS 1.3握手中原本跨4个函数、约400行的逻辑被压缩成42行片段，缩减89.5%。
RFC里的安全属性被自动改写成针对具体实现变量的线性时序逻辑公式，再交给nuXmv穷举状态空间检查。 RFC只描述协议语义层面的要求，不指名任何实现变量；不同实现的变量命名和状态结构差异很大，同一份属性模板无法直接复用。 在39组属性与实现的组合、三次运行共117条生成公式中，109条与专家参考公式等价，准确率93.2%；其余为4条语义错误、2条语法错误和2条映射错误，语法与映射错误在模型检验前即可被机械检出。
启示与展望
评测对象是TLS、IKEv2、SSH的七个开源实现，每个实现只覆盖固定发布版本的服务端状态机；切片与nuXmv检验在本地运行，分析一个实现约需18分钟。作者提出后续把分析扩展到深层调用链、复杂宏和异步控制流，并自动化部分参考模型构建与属性对齐工作。
参考模型由专家手工构建，虽经两人独立标注后讨论调和，仍存在歧义；基线只用GLM-5.1评测，默认切片深度由同一批被测对象上的敏感性分析选出，作者称F值在默认值附近平坦、加大深度不改变结果。转移级匹配只衡量与参考模型逐边一致，不建立迹等价或长期行为等价。