LinLi's Blog

SMT Solver Validation Empowered by Large Pre-trained Language ModelsABSTRACTSMT求解器已被用于检验逻辑公式的可行性，并已应用于多个关键领域，包括软件验证、测试用例生成和程序合成。然而，隐藏在SMT求解器中的错误可能导致严重的后果，引发SMT求解器中的错误结果。因此，确保SMT求解器的可靠性和健壮性至关重要。尽管已提出了多种测试方法用于SMT求解器，生成有效的测试公式对于全面测试SMT求解器仍是一项挑战。为了解决这一挑战，本研究提出将大型语言模型（LLMs）用于生成用于模糊测试SMT求解器的SMT公式。具体而言，本研究提出了一种新的重训细调流程来释放语言模型生成有效SMT公式的潜力，并通过数据增强提高其生成性能。我们将该方法实现为一个实用的模糊测试工具，名为LAST，并对当前最先进的SMT求解器，即Z3、cvc5和Bitwuzla进行了广泛测试。迄今为止，LAST已成功揭示了65个真实错误，其中45个已被开发者修复。 INTRODUCTIONBackground SMT求解器概述: 定义：高级自动定理证明工具 ...

MR-Adopt: Automatic Deduction of Input Transformation Function for Metamorphic TestingABSTRACT尽管最近的研究揭示，许多开发者编写的测试用例可以编码为可重用的变形关系（MR），但其中超过70%直接对源输入和后续输入进行了硬编码。这些编码的MR不包含将源输入转换为相应后续输入的显式输入转换，因此无法通过新的源输入重用来增强测试充分性。 在本文中，我们提出了MR-Adopt（自动推导输入转换），以自动从硬编码的源和后续输入中推导输入转换，旨在使编码的MR能够与新的源输入一起重用。以一个通常只包含一对源输入和后续输入的MR编码测试用例为例，我们利用LLM（大语言模型）理解测试用例的意图并生成额外的源-后续输入对。这有助于引导生成可推广至多个源输入的输入转换。此外，为了缓解LLM生成错误代码的问题，我们通过数据流分析移除与MR无关的代码元素，进一步优化LLM生成的转换。最后，我们基于编码的输出关系评估候选转换并选择最佳转换作为结果。 评估结果表明，MR-Adopt能够生成适用于72.00%编码MR的所有 ...

Domain Adaptation for Code Model-Based Unit Test Case GenerationAbstract最近，基于深度学习的测试用例生成方法被提出，用以自动生成单元测试用例。在本研究中，我们利用基于Transformer的代码模型，通过领域适应（Domain Adaptation，DA）在项目级别上生成单元测试。具体而言，我们使用CodeT5，这是一种相对较小的在源代码数据上训练的语言模型，并将其微调用于测试生成任务。接着，我们对每个目标项目数据应用领域适应，以学习项目特定的知识（项目级别DA）。我们使用Methods2test数据集微调CodeT5以进行测试生成任务，并使用Defects4j数据集进行项目级别的领域适应和评估。我们将我们的方法与以下基线进行比较：(a) 没有DA的CodeT5微调测试生成，(b) A3Test工具，以及(c) GPT-4，在Defects4j数据集的五个项目上进行了实验。结果表明，使用DA生成的测试相较于上述(a)、(b)和(c)基线，可以分别提高18.62%、19.88%和18.02%的行覆盖率，并提高16.4 ...

LPR: Large Language Models-Aided Program Reduction程序简化是一种广泛使用的技术，用于通过自动最小化触发编译器错误的程序来促进调试编译器。现有的程序简化技术要么是通用的，可以适用于多种编程语言（如Perses和Vulcan），要么是专门为某一特定语言优化的，通过利用特定语言的知识（例如，C-Reduce）。然而，如何在程序简化中将跨语言的通用性与针对特定语言的最佳性有机结合，仍然是未被探索的领域。 本文提出了LPR，这是一种首次利用大语言模型（LLMs）进行多语言特定程序简化的技术。关键思想在于利用像Perses这样的通用程序简化器的语言通用性，以及LLMs所学到的特定语言语义。具体而言，通用程序简化器可以将程序有效地简化为LLMs能够处理的小尺寸程序；LLMs可以通过学到的语义有效地转换程序，创建新的简化机会，以便通用程序简化器进一步简化程序。 我们在三种编程语言（即C、Rust和JavaScript）上的50个基准测试的详细评估表明，LPR在实用性和优越性上超过了Vulcan，这是当前最先进的通用程序简化工具。在有效性方面，LPR在C ...

Understanding and Detecting SQL Function Bugs Using Simple Boundary Arguments to Trigger Hundreds of DBMS Bugs Abstract内置 SQL 函数在数据库管理系统（DBMS）中非常关键，支持各种操作和计算，跨多种数据类型，它们对于查询、数据转换和聚合至关重要。尽管内置 SQL 函数的重要性，但 SQL 函数中的错误已经在现实世界中引起了广泛的问题，从系统故障到任意代码执行。然而，对这些错误特征的理解有限。更重要的是，传统的函数测试方法难以生成语义正确的 SQL 测试用例，而数据库管理系统的测试工作难以对内置 SQL 函数进行评估。 本文介绍了对 318 个内置 SQL 函数错误的全面研究，阐明了这些错误的特征和根本原因。我们的调查发现，87.4% 的错误是由参数边界值的不当处理造成的。参数的边界值来自三个来源：字面值、类型转换和嵌套函数。通过研究这三个来源的错误，我们总结了十种引起错误的 SQL 查询模式。此外，我们还设计了一种基于这些模式的测试工具 SOFT，用于测试包括 ...

THANOS: DBMS Bug Detection via Storage Engine Rotation Based Differential TestingABSTRACT摘要——差分测试是一种在自动化数据库管理系统（DBMS）测试中建立测试预言的普遍策略。然而，选择具有不同实现和兼容输入语法的等效DBMS需要大量的人工努力。在本文中，我们提出了THANOS，这是一种通过存储引擎轮换的差分测试来发现DBMS漏洞的框架。我们的关键见解是，不同存储引擎的DBMS必须提供一致的基础存储功能。因此，可以基于存储引擎轮换来构建等效的DBMS，确保相同的SQL测试用例在这些等效DBMS上产生一致的结果。该框架包括四个主要步骤：1）选择适当的存储引擎；2）提取所选存储引擎之间的等效性信息；3）综合确保DBMS等效性的特征导向测试用例；4）将测试用例发送到具有所选存储引擎的DBMS，并比较结果。 我们在三种广泛使用且广泛测试的DBMS上评估了THANOS，分别是MySQL、MariaDB和Percona，并将其与最先进的模糊测试工具SQLancer、SQLsmith和SQUIRREL进行了对比。 ...

SQLaser: Detecting DBMS Logic Bugs with Clause-Guided Fuzzing这篇文章是arXiv 24上的，存在许多问题，不值得学习。。。 ABSTRACT数据库管理系统（DBMS）是现代数据驱动系统中的重要组成部分。由于其复杂性，这些系统中往往会出现逻辑错误，这些错误是DBMS内部的实现错误，可能导致错误的查询结果、数据泄露、未经授权的访问等问题，而这些错误并不一定会引起系统的明显故障。现有的检测方法主要采用两种策略：基于规则的错误检测和基于覆盖率的模糊测试。然而，规则的指定本身就是一个挑战，因此基于规则的检测通常仅限于特定和简单的规则。基于覆盖率的模糊测试则是盲目地探索代码路径或代码块，其中许多路径不太可能包含逻辑错误，因此这种策略的成本效益较低。 在本文中，我们设计了SQLaser，一种基于SQL子句引导的模糊测试工具，用于检测DBMS中的逻辑错误。通过对现有大多数逻辑错误的全面研究（不包括导致系统崩溃的错误），我们识别了35种逻辑错误模式。这些模式表现为某些常见的SQL子句组合，而这些子句组合背后是一系列函数的组合。因此，我们将逻辑 ...

MVP: Detecting Vulnerabilities using Patch-Enhanced Vulnerability SignaturesABSTRACT复现漏洞在现实世界的系统中广泛存在并且通常未被检测到，这通常是由于重用代码库或共享代码逻辑所导致的。然而，脆弱函数与其修补函数之间潜在的小差异以及脆弱函数与目标检测函数之间可能存在的大差异，给基于克隆和函数匹配的检测方法带来了挑战，导致高误报率和漏报率。 在本文中，我们提出了一种新颖的方法来检测复现漏洞，具有低误报率和低漏报率。我们首先使用我们新颖的程序切片技术，从脆弱函数及其修补函数中提取漏洞和补丁签名，在语法和语义层面上进行分析。然后，如果目标函数匹配漏洞签名但不匹配补丁签名，则将其识别为潜在的脆弱函数。我们将该方法实现于一个名为MVP的工具中。我们在十个开源系统上的评估结果表明，i) MVP显著优于当前最先进的基于克隆和函数匹配的复现漏洞检测方法；ii) MVP检测到了一般漏洞检测方法无法检测到的复现漏洞，即两个基于学习的方法和两款商业工具；iii) MVP检测到97个新的漏洞，并已分配了23个CVE标识符。 IN ...

Movery: A Precise Approach for Modified Vulnerable Code Clone Discovery from Modified Open-Source Software ComponentsAbstract从第三方开源软件（OSS）组件继承的漏洞可能会危及整个软件的安全。然而，由于这些漏洞在不同的代码语法中广泛传播，因此发现传播的易受攻击代码是一项挑战，特别是由于OSS的内部更新和修改（例如，在OSS复用过程中发生的代码更改）。 在本文中，我们提出了一个名为Movery的精确方法，用于从修改过的OSS组件中发现易受攻击的代码克隆（VCC）。通过选择性地识别和提取只涉及核心漏洞和修补程序行的修改，Movery生成漏洞和修补程序签名，有效地解决了OSS修改的问题。为了可扩展性，Movery专注于仅从其他OSS项目借用的代码。最终，Movery通过匹配漏洞签名并与修补程序签名具有区别性来确定函数是否是VCC。 当我们将Movery应用于十个流行的软件选择自不同领域时，我们观察到91%的发现的VCC直接影响到了脆弱功能。然而，Movery发现的VCC ...

Translating between SQL Dialects for Cloud MigrationABSTRACT将系统从现场迁移到云端是许多工业机构的基本任务。此类云迁移的一个关键组成部分是将数据库转移到在线托管。在这项工作中，我们考虑了SQL数据库迁移的困难。尽管SQL是存储数据库程序的主要方法之一，但存在大量不同的SQL方言（例如，MySQL，Postgres等），当本地SQL方言与云端托管的方言不同时，这些方言会使迁移变得复杂。AWS和Azure等常见云服务提供商提供了一些工具来帮助方言之间的翻译，以缓解大部分困难。然而，这些工具无法成功翻译100%的代码。因此，软件工程师必须手动转换其余未翻译的数据库。对于大型组织来说，这项任务很快就变得难以处理，因此需要更创新的解决方案。 我们认为这个挑战是任何考虑云迁移的大型公司面临的新颖但重要的工业研究问题。此外，我们介绍了一些应对这一挑战的潜在研究途径，这些途径已经产生了有前景的初步结果。 INTRODUCTION在过去的十年里，向云迁移的兴趣和需求一直在加速增长。确实，越来越多的公司选择将现场功能迁移到云端，以支持在云上托管应 ...