静态分析
在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)
在这项工作中，作者尝试根据可用资源（如空闲内存）动态调整分析参数。该技术启用或禁用变量的流敏感性。首先，他们为每个变量评分，表示流敏感性的重要性。然后，控制器决定应有多少变量被流敏感处理。如果未达到固定点，控制器可以动态更改流敏感处理的变量数量。这项工作为自适应静态分析器迈出了重要一步，使其能够在实际环境中自我调整。
SMOKE：针对百万行代码的可扩展路径敏感内存泄漏检测
作者：Gang Fan, Rongxin Wu, Qingkai Shi, Xiao Xiao, Jinguo Zhou, Charles Zhang (pdf)
SMOKE尝试解决在大型代码库中查找内存泄漏的问题。这项工作的直觉是，大多数内存对象可以通过简单分析证明安全，而只有少数对象需要昂贵分析。他们的方法分为两步：首先，使用所谓的用流图表示进行快速但不精确的分析，以过滤掉大多数泄漏候选；然后，对剩余对象使用精确且昂贵的分析。值得注意的是，他们首先使用线性时间求解器过滤明显结果，仅对剩余情况应用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中（我们类似Google Test的基于属性的C和C++测试工具）。
区块链
区块链在学术界仍然是一个热门话题。几个新会议专门关注这一领域。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或我们的区块链工具链）。我们享受与学术界交流技术愿景。我们也乐意提供任何技术支持，以将我们的工具用于学术研究。如果您的工作使您尝试我们的工具，请联系我们获取支持！