清华大学软件系统安全保障小组两项研究成果被 OOPSLA 2026 接收
OOPSLA（Object-Oriented Programming, Systems, Languages, and Applications）是程序语言与软件系统领域的重要国际学术会议之一，长期关注编程语言、软件工程、系统实现、程序分析与自动化测试等方向的前沿研究。2026 年，清华大学软件系统安全保障小组共有 2 项研究成果被 OOPSLA 2026 接收。
第一项成果是 “VeriEQ: Finding Verilog Simulators and Synthesizers Bugs with Equivalence Circuit Transformation”。该工作面向 Verilog 仿真器与综合器中的行为偏差缺陷检测问题，提出了一套基于等价电路变换的自动化测试框架 VeriEQ，在 4 个主流 Verilog 工具中发现了 33 个此前未知的缺陷，其中包括 29 个行为偏差缺陷 和 4 个挂起类缺陷，已有 27 个缺陷被修复。实验结果表明，VeriEQ 相较现有代表性工具可取得 138.1% 至 4161.9% 的效率提升。该工作由清华大学硕士生颜臻、清华大学博士生陈元亮、清华大学博士生马福辰、清华大学博士生喻泽弘等人参与完成，清华大学博士生陈元亮和清华大学姜宇副教授等人共同指导。
研究成果概要：
Verilog 仿真器和综合器是芯片设计与验证流程中的核心基础软件，广泛应用于硬件描述、功能验证、逻辑综合和自动化测试等关键环节。然而，由于这类工具内部涉及语法分析、中间表示构建、位宽推断、符号属性传播以及逻辑优化等复杂处理流程，极易引入各类软件缺陷。其中，一类尤为严重的问题是 行为偏差缺陷（Behavioral Deviation Bug, BDB）：这类缺陷不会像程序崩溃那样直接暴露异常，而是会在仿真或综合过程中悄然引入细微却关键的语义偏差，使芯片实际行为偏离设计预期，甚至可能被攻击者利用以植入硬件后门，带来严重的安全风险。现有针对 Verilog 工具的测试方法大多依赖差分测试，即随机生成 Verilog 程序并在多个仿真器或综合器之间比较结果差异。然而，这类方法往往存在两方面局限：一方面，不同工具对未知值传播、事件调度等语义细节的处理并不完全一致，容易掩盖真正的缺陷；另一方面，现有方法通常忽视了更容易触发行为偏差缺陷的关键语法结构，因此难以系统性覆盖深层缺陷。为此，该工作提出了 VeriEQ，通过生成“语义等价但语法不同”的 Verilog 程序，在单个工具内部执行变形测试，从而更有效地暴露隐藏的行为偏差问题。
VeriEQ 的主要流程如下，包含三个重要组件：Initial Code Generator、Equivalent Code Transformer 以及 Bug Detector。
初始代码生成器（Initial Code Generator）： 为了提高触发行为偏差缺陷的概率，VeriEQ 首先系统分析历史缺陷案例，总结出更容易导致行为偏差错误的代码结构特征，并据此构建 Verilog 模板。基于这些模板，系统能够生成更具针对性的初始测试程序和输入激励，从而提升测试样例命中高风险语义边界的概率。该过程还会跟踪表达式中各变量的位宽与符号属性，为后续等价变换提供语义基础。
等价代码变换器（Equivalent Code Transformer）： Verilog 的表达式语义高度依赖位宽和 signedness，若直接套用常见代数恒等式，往往会破坏原程序语义。为此，VeriEQ 设计了一组面向 Verilog 语义特点的 等价电路变换规则，仅在满足严格位宽和符号约束时应用变换，生成多份语义一致、语法多样的等价变体。这些变体能够在保持功能不变的前提下，触发工具内部不同的处理路径，从而更容易暴露潜在缺陷。
缺陷检测器（Bug Detector）： 为了兼顾效率与通用性，VeriEQ 设计了 内联偏差检测机制，将多个等价模块同时嵌入到同一个 testbench 中，在共享输入激励下直接比较它们的输出结果。这样既能够高效识别语义不一致问题，也能统一支持仿真器和综合器的测试流程。此外，系统还实现了异常监测机制，用于检测测试过程中的挂起等异常行为，并自动生成错误报告以供后续分析。
第二项成果是 “Beacon: Detecting Broken Access Control Vulnerabilities in DBMSs via System Catalog Consistency Validation”。该工作面向数据库管理系统（DBMS）中的访问控制漏洞检测问题，提出了一种基于系统表一致性验证的自动化测试方法 Beacon，在 8 个主流数据库系统中发现了 39 个此前未知的访问控制漏洞，其中包括 19 个权限提升漏洞和 20 个未授权信息泄露漏洞，所有漏洞均已被厂商确认，已有 23 个漏洞被修复。该工作由清华大学硕士生彭宗睿、清华大学博士生符景洲、清华大学博士生吴志镛等人参与完成，由清华大学姜宇副教授、北航梁杰副教授等人共同指导。
研究成果概要：
数据库管理系统（DBMS）是现代信息系统中的核心基础软件，广泛应用于金融、医疗和互联网等关键领域。访问控制机制作为数据库系统的核心安全保障，用于限制用户对数据资源的访问。然而，由于数据库权限机制通常具有多层级结构、动态变化以及实现复杂等特点，其实现过程中易引入各类软件缺陷。其中，一类尤为严重的问题是 访问控制漏洞（Broken Access Control, BAC）：这类漏洞不会像程序崩溃那样直接暴露异常，而是可能在系统正常运行过程中悄然允许用户执行超出权限范围的操作，例如访问其他用户的数据或修改关键数据库对象，从而带来严重的安全风险。现有针对这类漏洞的检测方法主要依赖人工测试，耗时且难以覆盖全部场景。同时，静态分析方法在数据库系统中也面临困难，因为数据库权限具有多层级结构且动态变化，使得基于固定规则的静态分析难以有效应用。为此，该工作提出了 Beacon，通过利用数据库系统中系统表（System Catalog）与访问权限之间的一致性关系，实现对访问控制漏洞的自动检测。
Beacon 的主要流程如下，包含三个重要组件：Privilege-Aware Test Case Generation、Unauthorized Object Identification 以及 Catalog Consistency Validation。
权限感知的测试用例生成（Privilege-Aware Test Case Generation）： 为了系统性探索数据库中不同权限配置下的执行行为，Beacon 自动构造包含多种 SQL 操作（如 CREATE、INSERT、SELECT 等）的操作序列，并为每个操作动态配置权限（GRANT/REVOKE）。该过程能够生成语法和语义均正确的测试用例，同时覆盖多种数据库对象和权限组合，从而提高触发访问控制漏洞的概率。
未授权对象识别（Unauthorized Object Identification）： 在执行每条 SQL 操作之前，Beacon 分别以管理员用户和普通用户查询系统目录，并对查询结果进行差分分析。通过比较两类用户可见的数据库对象，系统能够识别出普通用户不可访问的对象集合，这些对象即为后续漏洞检测的关键目标。
系统表一致性验证（Catalog Consistency Validation）： 在执行 SQL 操作后，Beacon 检测未授权对象是否出现在查询结果、错误信息或成功执行的 SQL 语句中。如果未授权对象被返回、泄露或被成功访问，则说明数据库系统的访问控制机制存在缺陷，从而识别出访问控制漏洞，包括权限提升和未授权信息泄露两类问题。