发表机构
OWASP（开放Web应用程序安全项目）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出基于CPG的C到Lean 4自动形式化转换器，通过信任账本区分拒绝与静默错误转换，揭示SQLite转换中单一成功率掩盖的2.4倍差距及静默错误风险。
AI 中文摘要
验证大型C代码库需要将其转换为可形式化检查的语义，但大多数自动形式化工作只报告一个单一的总体成功率，这混淆了两种不同的失败模式：翻译器拒绝处理的代码和翻译器错误翻译的代码。我们提出了一种确定性的基于代码属性图（CPG）的导出器，在三级正确性纪律下将C源代码转换为小型Lean 4核心语义：无洞、调用封闭和动态洞风险，使这些模式保持区分。应用于SQLite源代码树的重新导出（8,602个函数，超过150万个AST节点），该导出器转换了5,222个函数（60.7%）为无洞，其中只有2,134个（24.8%）是调用封闭的，这是单一比率会隐藏的2.4倍差距。这两个数字都在完整的按构造信任账本中报告，而不是单一分数。我们的主要贡献是方法论上的：一种协议，用于区分通过整个程序静态分析从根本上无法解决的构造（如公共API边界）与仅看起来如此的构造。例如，在追踪目标代码库中的具体反例后，我们撤回了自己关于函数指针/vtable分派的“不可能”分类。另外，搜索“更多洞被封闭”揭示了一个潜在的静默错误答案缺陷：一个翻译成功但结果不正确而不是拒绝，我们认为这种失败模式比任何洞都更危险，而仅计算洞的评估永远不会发现它。
英文摘要
Verifying large C codebases requires translating them into formally checkable semantics, but most autoformalization work reports a single aggregate success rate that conflates two different failure modes: code the translator declined to handle and code the translator translated incorrectly. We present a deterministic code-property-graph (CPG)-based exporter that translates C source into a small Lean~4 core semantics under a three-tier correctness discipline: hole-free, call-closed, and dynamic-hole-risk, that keeps these modes distinct. Applied to a re-export of the SQLite source tree (8{,}602 functions, over 1.5~million AST nodes), the exporter translates 5{,}222 functions (60.7\%) hole-free, of which only 2{,}134 (24.8\%) are call-closed, a $2.4\times$ gap a single rate would hide. Both figures are reported in a full per-construct trust ledger rather than a single score. Our main contribution is methodological: a protocol for separating constructs that are fundamentally unresolvable by whole-program static analysis (such as public API boundaries) from constructs that only look that way. For example, we retracted our own ``impossible'' classification of function-pointer/vtable dispatch after tracing a concrete counterexample in the target codebase. Separately, a search for ``more holes closed'' surfaced a latent silent-wrong-answer bug: a translation that succeeded with an incorrect result rather than declining, a failure mode we argue is more dangerous than any hole, and one a hole-count-only evaluation would never surface.
Comments12 pages
