Trail of Bits @ ICSE 2019 – 回顾

三周前，我们在ICSE的WETSEB研讨会上展示了我们在Slither上的工作。ICSE是一个顶级的软件工程学术会议。本次会议举办得非常成功，组织者尽力吸引工业界人士参与讨论。会议中有许多并行进行的演讲，我们希望能同时参加多个演讲。以下列出一些我们推荐的演讲：

注意：以下部分论文仅限付费账户访问。我们将尽力在论文免费公开后更新链接。

静态分析

在Trail of Bits，我们投入大量精力构建可靠的静态分析器。例如，McSema允许我们将二进制文件直接提升到LLVM，而Slither利用静态分析来检查智能合约。ICSE提供了丰富的相关演讲。我们注意到两个有趣的趋势来改善静态分析的可扩展性：轻量级和昂贵分析的结合，以及参数的在线调优。

基于SMT的Clang静态分析器中虚假错误报告的驳斥

作者：Mikhail R. Gadelha, Enrico Steffinlongo, Lucas C. Cordeiro, Bernd Fischer, Denis A. Nicole (pdf)

这项工作在clang中突出了静态分析的可扩展性。作者通过使用SMT求解器来消除clang静态分析器发出的误报。该求解器旨在过滤出现有静态分析器检测到的简单误报。虽然技术本身并不新颖，但很高兴看到它在编译器中的具体实现。该技术可以开箱即用，没有显著开销。

通过在线抽象调整实现资源感知的程序分析

作者：Kihong Heo, Hakjoo Oh, Hongseok Yang (pdf)

在这项工作中，作者尝试根据可用资源（例如空闲RAM）动态调整分析参数。该技术启用或禁用变量的流敏感性。首先，他们用分数对每个变量进行排名，表示流敏感性的重要性。然后，控制器决定应有多少变量被流敏感地处理。如果未达到固定点，控制器可以动态更改被视为流敏感的变量数量。这项工作朝着自适应静态分析器迈出了重要一步，能够在现实环境中自我调整。

SMOKE：针对数百万行代码的可扩展路径敏感内存泄漏检测

作者：Gang Fan, Rongxin Wu, Qingkai Shi, Xiao Xiao, Jinguo Zhou, Charles Zhang (pdf)

SMOKE尝试解决在大型代码库中查找内存泄漏的问题。这项工作的直觉是，大多数内存对象可以在没有复杂分析的情况下被证明是安全的，而只有一小部分对象需要昂贵的分析。他们的方法分为两步：首先，他们使用所谓的use-flow图表示来执行不精确但快速的分析，以过滤掉大多数泄漏候选。然后，他们对剩余对象使用精确且昂贵的分析。值得注意的是，他们首先使用线性时间求解器过滤掉明显的结果，并仅在剩余情况下应用SMT求解器。SMOKE构建在LLVM之上。该工具似乎可以扩展到高达800万行代码的项目。工具和重现实验的数据可用（源代码不可用）。

测试

我们始终对最先进的测试技术感兴趣，以改进输入生成，无论是通过模糊测试还是符号执行。例如，我们最近在Manticore（我们的符号执行引擎）中添加了新的技术，用于加密原语的混合执行和符号路径合并。

生成随机结构丰富的代数数据类型值（AST）

作者：Agustín Mista, Alejandro Russo (pdf)

作者设计了一种在Haskell中生成代数数据类型值的方法。生成的值在随机生成每个值构造函数的频率方面更加“均匀”（多样性对于发现更多错误很重要）。生成后，这些值可用于测试其他程序（不一定是Haskell）。作者的系统在编译时工作，生成Haskell代码来生成值。源代码可在此处获取。

DifFuzz：用于侧信道分析的差异模糊测试

作者：Shirin Nilizadeh, Yannic Noller, Corina S. Pasareanu (pdf)

DiffFuzz使用差异模糊测试来检测侧信道。其想法是，不是最大化代码覆盖率，而是最大化两个输入之间使用的资源差异（即时间或消耗的内存）。输入旨在由相同的公共部分和不同的私有部分组成。如果使用的资源差异超过给定阈值，攻击者可以推断有关发送的私有部分的信息。论文使用特定基准进行了公平评估。代码可在此处获取。

SLF：无有效种子输入的模糊测试

作者：Wei You, Xuwei Liu, Shiqing Ma, David Mitchel Perry, Xiangyu Zhang, Bin Liang (pdf)

一篇有趣的论文，展示了在无种子或源代码可用时改进模糊测试的技术。SLF使用一种复杂的技术，分为多个步骤。首先，SLF使用AFL识别输入数据中的字段。然后，它使用轻量级动态分析来确定哪些字段在执行过程中被验证（例如，在解析文件时）以及使用了哪种类型的检查：算术、索引/偏移、计数或if-then-else。此外，SLF识别检查何时相互依赖。最后，该工具实现了一系列技术，根据每个字段的类型生成和变异输入。

实验评估是公平的，并在发现新错误和提高复杂程序测试覆盖率方面显示出良好结果。然而，SLF不是开源的，因此我们无法验证本文中呈现的结果。

二进制代码上的灰盒混合测试

作者：Jaeseung Choi, Joonun Jang, Choongwoo Han, Sang Kil Cha (pdf)

本文介绍了Eclipser，一个从符号执行中借鉴了一些想法但保持可扩展性的模糊测试器，适用于更大和更复杂的程序。我们非常喜欢他们的想法，以至于在最近的博客文章中详细描述了他们的论文，并将Eclipser集成到DeepState中，这是我们用于C和C++的类似Google-Test的基于属性的测试工具。

区块链

区块链在学术界仍然是一个热门话题。几个新会议专门关注这一领域。ICSE未能逃脱这股热潮。会上提交了几篇与区块链相关的论文。虽然质量参差不齐，但我们发现以下工作有前景：

更智能的智能合约开发工具（WETSEB）

作者：Michael Coblenz, Joshua Sunshine, Jonathan Aldrich, Brad A. Myers (pdf)

这个演讲介绍了Obsidian，一种新的智能合约语言，旨在比现有语言（如Solidity）更安全。Obsidian具有有趣的特性，包括一种用户级的前后条件类型系统。Obsidian尝试静态证明条件，并在需要时添加动态检查。当前实现仅编译到Hyperledger Fabric。该语言仍处于早期阶段，但有前景。作者正在进行用户研究以改进语言设计。

Gigahorse：智能合约的全面声明式反编译

作者：Neville Grech, Lexi Brent, Bernhard Scholz, Yannis Smaragdakis (pdf)

Gigahorse是一个EVM反编译器。作者以意想不到的方式使用Datalog，一种声明式逻辑编程语言：他们将反编译步骤编写为Datalog规则，并将其与外部固定点循环结合以克服语言限制。Web服务可在https://contract-library.com获取，但未提供源代码。

自动化修复

自动错误修补是一个有趣但复杂的话题。我们在CGC竞赛中应对了这一挑战，并通过slither-format在智能合约方面取得了初步成果。我们肯定有兴趣回顾这一研究领域的学术趋势。几篇论文展示了有前景的工作，但需要注意的是，它们通常专注于一种类型的问题，并且一些评估生成了不正确的补丁。

SapFix：大规模自动化端到端修复

作者：A. Marginean, J. Bader, S. Chandra, M. Harman, Y. Jia, K. Mao, A. Mols, A. Scott (pdf)

SapFix是Facebook部署的自动化端到端故障修复工具，设计用于大规模工作。该系统专注于空指针，并利用其他两个工具Sapienz和Infer。这项工作展示了启发式和模板的有趣组合，以创造对用户最不痛苦的体验。例如，该系统将结合动态崩溃信息和Infer静态分析器来改进故障定位。如果七天内没有开发人员审查补丁，它将放弃该补丁。论文呈现了有前景的结果。

关于补丁正确性评估的可靠性

作者：Xuan-Bach D. Le, Lingfeng Bao, David Lo, Xin Xia, Shanping Li, and Corina Pasareanu (pdf)

这项工作评估了补丁生成工具的有效性。不幸的是，这种类型的验证在会议中代表性不足。作者对八个自动软件修复工具进行了评估，涉及35名开发人员。论文显示，工具的结果不如声称的那样有前景，尽管它们仍然作为更成熟工具的补充有用。

海报会议

海报会议旨在展示进行中的工作，并允许与作者直接互动。我们发现了几个有前景的工作。

需求驱动的指向分析细化

作者：Chenguang Sun, Samuel Midkiff (pdf)

这项工作遵循我们在静态分析会议期间看到的趋势，以帮助可扩展性。目标是通过切片回答目标查询所需的相关程序元素来改进指向分析。

WOK：生产中的静态程序切片

作者：Bogdan-Alexandru Stoica, Swarup K. Sahoo, James Larus, Vikram Adve (pdf)

作者正在努力实现程序的可扩展动态切片，通过利用静态收集的数据流信息和现代硬件支持（例如Intel Processor Trace）。他们的初步评估显示了该技术的真正潜力。

有效性模糊测试和参数生成器用于有效随机测试

作者：Rohan Padhye, Caroline Lemieux, Koushik Sen, Mike Papadakis, Yves Le Traon (pdf)

这项进行中的工作试图通过两个特性指导基于生成器的测试（即QuickCheck）来改进输入生成：（1）使用验证器丢弃语义无效的输入，以及（2）从原始位输入转换为结构化输入。目标是能够保留输入的语法和语义，尤其是结构化输入（即文件格式）。

通过机器学习优化模糊测试中的种子输入

作者：Liang Cheng, Yang Zhang, Yi Zhang, Chen Wu, Zhangtan Li, Yu Fu, Haisheng Li (pdf)

作者旨在通过机器学习改进输入生成，遵循与Learn&Fuzz相同的技术。其见解是让神经网络学习输入和执行跟踪覆盖率之间的相关性，以生成更可能探索未见过代码的输入。他们在PDF上的首次实验与先前工作相比显示出令人鼓舞的结果。

贡献学术研究

在我们的工作中，我们花费相当多的时间基于最新研究构建可靠软件（参见Manticore、McSema、Deepstate或我们的区块链工具链）。我们享受与学术界交流我们的技术愿景。我们也乐意提供任何技术支持，以便将我们的工具用于学术研究。如果您的工作需要尝试我们的工具，请联系我们获取支持！

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News