LinLi's Blog

Finding Logic Bugs in Spatial Database Engines via Affine Equivalent InputsAbstract空间数据库管理系统（SDBMSs）旨在存储、操作和检索空间数据。SDBMSs 被广泛应用于现代各类应用中，例如地理信息系统、计算机辅助设计工具和基于位置的服务。然而，SDBMSs 中存在逻辑错误可能导致错误的结果，极大地削弱这些应用的可靠性。在 SDBMSs 中检测逻辑错误非常具有挑战性，因为缺乏用于识别错误结果的真实基准。在本文中，我们提出了一种自动几何感知生成器，用于为 SDBMSs 生成高质量的 SQL 语句，并引入了一个新的概念仿射等价输入 (AEI) 来验证 SDBMSs 的结果。我们将这些概念实现为一个名为 Spatter (Spatial DBMSs Tester) 的工具，用于检测四种流行 SDBMSs 中的逻辑错误：PostGIS、DuckDB Spatial、MySQL 和 SQL Server。我们的测试活动检测到了 34 个之前未知且独特的错误，其中已有 30 个得到确认，18 个已被修复。我们的 ...

ClDiff: Generating Concise Linked Code DifferencesABSTRACT分析和理解源代码变更在多种软件维护任务中非常重要。为此，已经提出了许多代码差异分析和代码变更摘要的方法。然而，对于某些任务（例如代码审查和软件合并），这些差异分析方法生成的代码变更表示过于细粒度，而这些摘要方法生成的代码变更表示又过于粗粒度。此外，它们没有考虑代码变更之间的关系。因此，生成的差异或摘要在某些软件维护任务中难以分析和理解。 本文提出了一种代码差异分析方法，称为 ClDiff，用于生成简明的关联代码差异，其粒度介于现有代码差异分析方法和代码变更摘要方法之间。ClDiff 的目标是生成更易于理解的代码差异。ClDiff 以变更前后的源代码文件为输入，包括三个步骤。首先，它通过修剪解析的抽象语法树中的未更改声明来预处理源代码文件。其次，它通过对语句级别及以上的细粒度代码差异进行分组，并描述每组中的高级别变更，生成简明的代码差异。最后，它根据五种预定义的链接方式将相关的简明代码差异链接起来。 通过对 12 个 Java 项目（74,387 次提交）的实验和对 1 ...

Drowzee: Metamorphic Testing for Fact-Conflicting Hallucination Detection in Large Language ModelsABSTRACT大型语言模型（LLMs）已在语言处理领域引发了革命，但它们面临着安全性、隐私以及生成幻觉（即看似合理但事实上不准确的输出）等关键挑战。一个主要问题是事实冲突幻觉（FCH），即LLM生成的内容与事实真相相矛盾。解决FCH问题非常困难，主要面临两个挑战：1）自动构建和更新基准数据集较为复杂，因为现有方法依赖于人工整理的静态基准数据集，无法涵盖FCH案例的广泛、不断发展的范围；2）验证LLM输出背后的推理过程本身具有挑战性，尤其是对于复杂的逻辑关系。 为了解决这些问题，我们提出了一种新颖的逻辑编程辅助变形测试技术，用于FCH检测。我们开发了一个全面且可扩展的框架，通过爬取像维基百科这样的资源，构建一个全面的事实知识库，并将其无缝集成到Drowzee中。通过逻辑推理规则，我们将这些知识转化并增强为大量具有事实真相答案的测试案例。我们通过基于模板的提示对LLM进行测试，要求它们提供有理有 ...

Vision: Identifying Affected Library Versions for Open Source Software VulnerabilitiesABSTRACT漏洞报告在减少开源软件风险中起着至关重要的作用。通常，漏洞报告包含受影响的软件版本。然而，尽管安全专家已经验证了漏洞并且厂商也进行了审查，但受影响的版本并不总是准确的。特别是在处理多个版本及其差异时，保持版本的准确性变得更加复杂。虽然已经有一些方法用来识别受影响的版本，但它们仍然面临一些限制。首先，某些现有的方法是基于代码托管平台（如 GitHub）来识别受影响的版本，但这些版本与包注册表中的版本（如 Maven）并不总是保持一致。其次，现有的方法未能区分多个方法和变更块中漏洞方法与修补语句的重要性。 为了解决这些问题，本文提出了一种新的方法——Vision，旨在准确识别漏洞的受影响库版本（ALVs）。Vision使用来自包注册表的库版本作为输入。为了区分漏洞方法和修补语句的重要性，Vision通过关键方法选择和关键语句选择来优先考虑重要的变更及其上下文。此外，漏洞签名通过加权的跨过程程序依赖图（IP ...

Validating LLM-Generated Programs with Metamorphic Prompt TestingAbstract软件开发领域的最新范式转变，通过大型语言模型（LLMs）带来的创新和自动化，尤其是生成式预训练变换器（GPT），展示了其自主生成代码的卓越能力，显著减少了各种编程任务所需的人工投入。尽管LLM生成代码的潜在好处十分广泛——尤其是在提升效率和快速原型开发方面——但随着LLM越来越多地被集成到软件开发生命周期以及由此产生的供应链中，由此产生的复杂且多方面的挑战浮现出来。这些挑战源于由此类语言模型生成的代码在质量和正确性方面存在的重大疑问。因此，研究需要全面探讨围绕LLM生成代码的这些关键问题。 在本文中，我们提出了一种称为变形提示测试（Metamorphic Prompt Testing）的新方法，以应对这些挑战。我们的直观观察是，在正确代码片段之间总是存在内在的一致性，但在存在缺陷的代码片段之间可能不存在这种一致性，因此通过检测不一致性，我们可以发现代码中的缺陷。为此，我们可以通过改写将一个提示扩展为多个提示，并让LLM生成多个版本的代码，以便 ...

MASTERKEY: Automated Jailbreaking of Large Language Model ChatbotsAbstract大型语言模型（LLMs），如聊天机器人，在多个领域取得了显著进展，但仍容易受到越狱攻击（jailbreak attacks）的影响，这类攻击旨在引诱模型生成不恰当的响应。尽管已有尝试识别这些弱点，但由于服务提供商未公开防御措施，现有策略对主流LLM聊天机器人仍然无效。本文提出了一个名为 MASTERKEY 的框架，用于探索越狱攻击及其对应的防御动态。我们提出了一种基于时间特性的全新方法，该方法受时间延迟SQL注入技术启发，用于剖析LLM聊天机器人的防御机制。这项技术揭示了这些防御的工作原理，并在多个LLM聊天机器人上演示了概念验证攻击（proof-of-concept）。 此外，MASTERKEY 提供了一种创新方法，可自动生成针对强防御LLM聊天机器人的越狱提示（jailbreak prompts）。通过对一个含有越狱提示的LLM进行微调，我们生成了成功率达 21.58% 的攻击，大幅高于现有方法的 7.33% 成功率。我们已将这些发现通 ...

How Effective Are They? Exploring Large Language Model Based Fuzz Driver GenerationAbstractFuzz驱动程序对于库API的模糊测试至关重要。然而，自动生成Fuzz驱动程序是一项复杂的任务，因为这需要编写高质量、正确且健壮的API使用代码。基于大语言模型（LLM，Large Language Model）的Fuzz驱动程序生成方法是一个颇具前景的研究领域。与传统基于程序分析的生成器不同，这种基于文本的方法更加通用，能够利用多样的API使用信息，从而生成更易于人类阅读的代码。然而，目前在这一方向上对其有效性和潜在挑战等基本问题的理解仍然不足。 为弥补这一空白，我们首次针对使用LLM生成高效Fuzz驱动程序的关键问题进行了深入研究。本研究整理了一个包含86个Fuzz驱动生成问题的数据集，涉及30个广泛使用的C项目。我们设计并测试了六种提示策略，并在五种最先进的LLM上使用五种不同的温度设置进行了评估。总共生成了736,430个Fuzz驱动程序，耗费了8.5亿个token（费用超过8000美元）。此外，我 ...

METAL: Metamorphic Testing Framework for Analyzing Large-Language Model QualitiesAbstract大型语言模型（LLMs）已经改变了自然语言数据处理的范式。然而，其黑箱性和概率特性可能导致多种LLM应用中输出质量的潜在风险。最近的研究通过生成对抗输入文本，测试了LLMs的质量属性（QAs），例如稳健性或公平性。然而，现有研究在覆盖LLMs的QAs和任务方面存在局限性，并且难以扩展。此外，这些研究通常仅使用一个评估指标——攻击成功率（ASR）来评估其方法的有效性。为了解决这些问题，我们提出了一种用于分析LLMs的变形测试（METAL）框架，通过应用变形测试（MT）技术来系统化地测试LLMs的质量。 这种方法通过定义变形关系（MRs），为评估提供模块化的指标，从而促进LLMs质量的系统测试。METAL框架可以从覆盖各种QAs和任务的模板中自动生成数百个MRs。此外，我们引入了结合ASR方法的新颖指标，将其整合到文本的语义质量中，以准确评估MRs的有效性。通过对三个主流LLMs的实验，我们证实了METAL框架能够 ...

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的所有 ...