静态分析SAST应用安全漏洞扫描代码质量【免费下载链接】codeqlCodeQL: the libraries and queries that power security researchers around the world, as well as code scanning in GitHub Advanced Security项目地址https://gitcode.com/gh_mirrors/co/codeql点击查看免费下载导读本文围绕 CodeQL C 分析库 4.1.0 版本新增的核心数据流 API 展开DataFlow::Node类上新增了asUncertainDefinition与asCertainDefinition两个谓词用于在数据流分析中判定某个定义definition是否整体覆盖overwrite目标缓冲区。这一能力对缓冲区溢出、空终止null termination、内存安全类查询的准确性至关重要——例如只有确定全量写入的定义才可能在污点分析中作为屏障barrier被安全放行。读完本文你将理解这一 API 的语义边界、底层 SSA静态单赋值实现机制并掌握在真实安全查询中组合使用这两类定义判定、提升查询精度的实战方法。一、发布背景4.1.0 变更说明原文本仓库cpp/ql/lib/change-notes/released/4.1.0.md中记录了本次变更的原始描述New FeaturesAddedNode.asUncertainDefinitionandNode.asCertainDefinitionto theDataFlow::Nodeclass for querying whether a definition overwrites the entire destination buffer.这是 4.1.0 版本中唯一列入 New Features 的条目。它是对既有DataFlow::Node.asDefinition()系列 API 的一次语义细化在原有获取与该节点关联的定义表达式能力之上进一步区分定义是否保证整体覆盖目标缓冲区从而让下游查询尤其是污点分析中的屏障判定可以更精确地表达该定义之后污点状态已不可靠/已中止这类语义。对应的版本记录同时可参见仓库内 cpp/ql/lib/CHANGELOG.md其中按语义化版本持续跟踪 C 库的用户可见变更。二、API 速览两个新谓词与既有asDefinition的关系两个新谓词定义在DataFlow::Node类上位于 DataFlowNodes.qll谓词签名语义asCertainDefinitionExpr asCertainDefinition()当且仅当该节点是一个确定定义certain definition时返回与该节点关联的定义表达式asUncertainDefinitionExpr asUncertainDefinition()当且仅当该节点是一个不确定定义uncertain definition时返回与该节点关联的定义表达式它们的实现非常直观本质是对通用谓词asDefinition(boolean uncertain)的两种参数化调用Expr asCertainDefinition() { result this.asDefinition(false) } Expr asUncertainDefinition() { result this.asDefinition(true) }而asDefinition(boolean uncertain)的完整逻辑DataFlowNodes.qll为Expr asDefinition(boolean uncertain) { exists(StoreInstruction store | store this.asInstruction() and result asDefinitionImpl(store) and if this.isCertainStore() then uncertain false else uncertain true ) }由此可见certain确定与uncertain不确定的分野取决于底层存储指令StoreInstruction是否被判定为确定存储certain storecertain false即asCertainDefinition该定义保证整体覆盖定义目标地址所指向的缓冲区uncertain true即asUncertainDefinition该定义不能保证整体覆盖目标缓冲区。注意这两个谓词返回的是Expr即与节点关联的定义表达式如赋值语句的右值、自增表达式本身等而非节点本身。它们的语义完全遵循 DataFlowNodes.qll 中asDefinition()对定义表达式的既有约定例如int x 42;返回42x 34;返回x 34x;返回xx;返回x而x 1;与复合表达式还会存在多个关联定义结果。三、核心语义什么叫覆盖整个目标缓冲区官方文档对certain/uncertain的判定给出了明确的可执行判定标准DataFlowNodes.qll若uncertain false则该定义保证覆盖定义目标地址所指向的整个缓冲区否则uncertain true即写入可能只覆盖缓冲区的一部分。文档附带的两个经典示例int x; x 42; // 确定保证覆盖 x 分配的全部字节 int p[10]; p[3] 42; // 不确定写入并未覆盖 p 指向缓冲区的全部内容对int x; x 42;变量x的缓冲区大小即一个int整值赋值必定写满全部字节因此是确定定义对int p[10]; p[3] 42;只写入数组p的第 4 个元素剩余 9 个元素的字节未被本次定义覆盖因此是不确定定义。这类判定在内存安全分析中非常关键只有确定覆盖整个缓冲区的定义才能在被判定为屏障时安全地认为缓冲区的全部旧内容已被新值取代进而阻断污点传播或消除对旧状态的依赖。四、底层实现从isCertainStore到 SSA 定义certain判定的根基在私有谓词isCertainStore()DataFlowNodes.qllprivate predicate isCertainStore() { exists(SsaImpl::Definition def | SsaImpl::defToNode(this, def, _) and def.isCertain() ) }即节点对应的存储指令必须能在 SSA 层找到某个确定的定义def.isCertain()成立。这里SsaImpl::Definition是 SSA 实现中定义节点的抽象基类defToNode负责建立 SSA 定义与数据流节点之间的映射详见 SsaImpl.qll 与 DataFlowUtil.qll 中的别名class Definition SsaImpl::Definition。4.1 SSA 定义类别的isCertain实现在 SsaImpl.qll 中不同类别的定义分别覆盖isCertain()谓词构成确定的完整语义图景地址定义DefAddressImpl如DefVariableAddressImpl等初始化地址的定义isCertain()恒为真any()因为取得某变量的地址本身就是确定事件SsaImpl.qll普通直接定义DefImpl如 SsaImpl.qll 所示isCertain()取决于底层isDef(true, _, address, _, _, indirectionIndex)是否成立——即该定义在 SSA 表中被标记为确定且覆盖给定间接层级的目标地址后自增/自减的保存定义SavedPostfixCrementDefImplisCertain()同样取决于isDef(true, _, storeInstruction.getDestinationAddressOperand(), _, _, indirectionIndex)SsaImpl.qll即保存操作对应的存储指令是否是确定存储直接使用DirectUseImpl与间接使用通过isUse(true, ...)判定如 SsaImpl.qll其他确定语义的类别isCertain()直接返回any()SsaImpl.qll表示这些定义天然确定。4.2 Φ 节点的特殊处理环与固定点语义SSA 中的 Φphi节点合并了多条控制流路径上的定义其isCertain()实现SsaImpl.qll尤为精巧override predicate isCertain() { // 若该 Φ 节点属于 Φ 环phi cycledatalog 的最小固定点语义会给出错误答案 // 因此先做 SCC 归约以模拟最大固定点语义。 getCycle(this).isCertain() or // 若不在环中通过传统递归即可得到正确语义 // 当且仅当所有输入定义都确定时Φ 节点才是确定的。 not exists(getCycle(this)) and forex(Definition inp | inp this.getAnInput() | inp.isCertain()) }这段注释清晰地说明了工程取舍对于位于循环中的 Φ 节点直接递归会因 datalog 的最小固定点least fixed-point语义而误判因此代码先对 Φ 环做 SCC强连通分量归约来模拟最大固定点greatest fixed-point语义而对于无环情况规则退化为朴素的全输入确定则确定。五、实战用法在污点分析中作为屏障判定新增 API 最直接的价值体现于安全查询的屏障barrier定义中。以仓库内真实查询 ImproperNullTerminationTainted.qlCWE-170用户可控数据可能未空终止为例predicate isBarrier(DataFlow::Node node) { isSink(node) and node.asExpr().getUnspecifiedType() instanceof ArithmeticType or node.asCertainDefinition().getUnspecifiedType() instanceof ArithmeticType or mayAddNullTerminator(_, node.asIndirectExpr()) }该查询将node.asCertainDefinition().getUnspecifiedType() instanceof ArithmeticType作为屏障条件之一只有当某个定义是确定定义保证覆盖整个目标缓冲区且目标类型为算术类型时才中断污点传播。理由很直观若一个污点字节被某个确定写入的算术值整体覆盖那么后续对该缓冲区的读取不再依赖污点来源反之若只是p[3] 42这类部分写入则不能作为屏障污点仍需继续跟踪。查询其余部分ImproperNullTerminationTainted.ql展示了完整的配置结构可作为组合使用新 API 的模板源sourceread、fread、recv、recvfrom、recvmsg等函数写入栈上变量的参数source.asDefiningArgument()汇sinkvariableMustBeNullTerminated(va)判定需要空终止的变量访问屏障barrier如上所述利用asCertainDefinition过滤掉已被确定全量覆写的节点流引擎TaintTracking::GlobalConfig驱动全局污点流结果选择输出va位置并附注污染源类型例如 String operation depends on $ that may not be null terminated.。5.1 何时用asUncertainDefinitionasUncertainDefinition的典型场景与asCertainDefinition互补当查询需要专门追踪部分写入时例如分析缓冲区部分内容被改写后残留污点、检测数组元素级写入是否完整初始化缓冲区等可以写from DataFlow::Node n, Expr e where e n.asUncertainDefinition() select n, This definition does not overwrite the entire destination buffer: e.toString()两个谓词也可以结合asDefinition()形成穷举式分支Expr asDefinition() { result this.asDefinition(_) } // 既有 API见 DataFlowNodes.qll即有定义等价于确定定义或不确定定义的并集三者在逻辑上构成完整划分。六、与既有 API 的对照与迁移建议新 API 并不是对asDefinition()的破坏性替代而是语义细分。对照关系如下需求既有写法4.1.0 新增写法只要节点有定义表达式n.asDefinition()保持不变只关心保证覆盖整个缓冲区的定义需自行结合asDefinition与 SSA 内部谓词n.asCertainDefinition()只关心不能保证覆盖整个缓冲区的定义无直接手段n.asUncertainDefinition()从 DataFlowNodes.qll 的既有实现可见asDefinition()本身即asDefinition(_)因此三个谓词共享同一套asDefinitionImpl与isCertainStore底层逻辑不存在重复维护的成本。库作者在文档注释DataFlowNodes.qll中也明确要求读者参照asDefinition/1的说明理解确定/不确定定义的语义保证 API 家族的一致性。七、适用前提与注意事项适用范围本 API 属于 C 语言的 IR 数据流库semmle.code.cpp.ir.dataflow其判定依赖 IR 的StoreInstruction与 SSA 信息因此仅在包含 IR 数据流的 CodeQL C 查询中可用使用前需确保查询导入了对应的数据流模块如semmle.code.cpp.dataflow.new.TaintTracking与semmle.code.cpp.ir.IR。返回类型是Expr而非布尔两个谓词在条件不满足时节点不是确定/不确定定义不产生结果而非返回false。因此它们在where子句或屏障谓词中作为存在性条件使用符合 QL 的逻辑语义。部分写入的判定粒度certain只回答是否覆盖整个目标缓冲区不回答具体覆盖了多少字节。对需要字节级精确建模的查询仍需结合缓冲区大小、写入偏移等额外信息。Φ 环的特殊语义当定义处于 SSA Φ 环中时isCertain经由 SCC 归约获得最大固定点语义查询作者无需干预但应理解这一行为可能使循环内定义比朴素递归更宽容更多被判定为确定。结语Node.asCertainDefinition与Node.asUncertainDefinition是 CodeQL C 库 4.1.0 对数据流 API 的一次精准增强它们把该定义是否整体覆盖目标缓冲区这一内存安全分析中的高频判定从底层 SSA 细节提升为DataFlow::Node的一等公民谓词。通过仓库内的实现与真实查询ImproperNullTerminationTainted.ql可以看到二者与既有asDefinition家族共享底层isCertainStore/ SSAisCertain机制既保持了 API 一致性又为编写更精确的屏障、更细粒度的部分写入追踪提供了直接抓手。对于正在开发或维护 C 污点分析查询的开发者这两个谓词值得纳入标准工具箱。赞分享静态分析SAST应用安全漏洞扫描代码质量【免费下载链接】codeqlCodeQL: the libraries and queries that power security researchers around the world, as well as code scanning in GitHub Advanced Security项目地址https://gitcode.com/gh_mirrors/co/codeql点击查看免费下载相关推荐CodeQL C 库 0.0.10 新增特性Variable::isStructuredBinding 谓词详解CodeQL C 库 0.0.10 新增特性 Variable::isStructuredBinding 谓词详解 CodeQL 的 C 查询库在版本静态分析SAST应用安全漏洞扫描代码质量CodeQL 1.21 C/C 分析改进全解新增安全查询、既有查询强化与 QL 库 API 更新CodeQL 1.21 C/C 分析改进全解新增安全查询、既有查询强化与 QL 库 API 更新 本文以 CodeQL 仓库 change notes/1静态分析SAST应用安全漏洞扫描代码质量CodeQL 1.18 C 分析改进全解新查询、查询重构与 QL 库 API 演进CodeQL 1.18 C 分析改进全解新查询、查询重构与 QL 库 API 演进 导读 本文以 CodeQL 仓库的 change notes/1.18/a静态分析SAST应用安全漏洞扫描代码质量上一篇免费在电脑运行 Switch 游戏yuzu 模拟器安装、配置与调优全攻略下一篇3步安装Android Studio中文语言包把IDE界面切换成中文创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考