Efficient Branch-and-Bound Testing and Verification of zkVMs
零知识虚拟机（zkVM）通过把虚拟机语义翻译成执行轨迹上的代数约束，使通用程序能够被可验证地执行。这些约束的正确性至关重要：一条错误的约束可能使系统处于欠约束（under-constrained）状态，从而接受伪造的证明；也可能因过约束（o
#bug-detection
共收录 5 条相关情报。
← 返回所有主题Automata-Based Automated Detection of State Machine Bugs in Protocol Implementations.
该论文提出了一种基于自动机的黑盒技术，用于自动检测有状态网络协议实现中的状态机漏洞。有状态安全协议的实现需要维护一个状态机来跟踪协议进展，管理消息的类型和顺序以及加密材料，而状态机错误（即状态机bug）可能导致严重安全漏洞。该方法以协议的状
Finding Bugs Using Your Own Code: Detecting Functionally-similar yet Inconsistent Code.
本文提出了一种利用代码自身检测功能相似但不一致代码的新方法。研究背景是软件开发中常出现功能相似但实现不一致的代码片段，可能导致难以发现的bug。核心问题是如何自动识别这类语义等价但语法有差异的代码对。方法上，作者设计了一个基于程序分析和机器
MirChecker: Detecting Bugs in Rust Programs via Static Analysis.
Rust 作为一种系统级编程语言，通过强大的类型系统和所有权模型在编译时保证内存安全，但实际应用中仍然存在运行时崩溃和内存安全错误，可能导致可利用漏洞。现有静态分析工具在检测 Rust 程序中的缺陷时存在精度或覆盖面的不足。本文提出 Mir
Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers
该论文提出了一种自动检测 Linux 内核驱动中引用计数错误（reference counting bugs）的工具 DrvHorn。引用计数是内核实中管理资源（如内存、文件描述符等）生命周期的关键机制，一旦出现错误（如少放、多放或未初始化