概率符号执行技术赢得软件测试与分析影响力奖

Jaco Geldenhuys和Willem Visser赢得ISSTA影响力论文奖

Jaco Geldenhuys（某中心网络服务首席应用科学家）和Willem Visser（某中心网络服务高级首席应用科学家）因其提出的概率符号执行概念而获得了2022年国际软件测试与分析研讨会影响力论文奖。概率符号执行是一种推导计算机代码执行概率的新方法。他们的2012年论文《概率符号执行：通过模型计数进行定量程序分析》与弗吉尼亚大学Robert Thomson杰出计算机科学教授Matthew Dwyer合著。该论文展示了模型计数如何估计程序部分被执行的概率，而不是评估约束是真还是假。

“这开辟了一个全新的领域，”Visser说。“在我们之前，没有人做过这件事。通常，如果代码中有任何问题，那就是坏事，需要修复。现在可以计算程序的可靠性——因为只要‘那件事’不发生，代码就没问题，而且你现在知道它发生的可能性有多大。”

由ACM软件工程特别兴趣小组举办的ACM SIGSOFT ISSTA，31年来一直是软件测试和分析领域的领先研究会议。该会议每年颁发影响力论文奖给一篇发表已满10年、并对软件测试与分析的研究或实践产生重大影响的论文。

Geldenhuys、Visser和Dwyer的论文对涉及计算机程序系统性分析的许多应用产生了影响，尤其是在安全应用中涉及侧信道分析的应用。侧信道会泄露程序运行的间接信息（例如执行时间），攻击者无需直接访问代码即可利用这些信息。

“在这个特定应用领域，很少有工作不直接或间接源于这篇论文，”Geldenhuys说。“至少到目前为止，我们的论文仍然是其他工作得以生长出来的根。这是令人欣慰的事情。”

研究人员指出，他们的论文最初因所描述方法的复杂性而受到质疑，这导致分析在计算资源方面成本高昂。随后，三人合作撰写了第二篇关于如何提高概率分析效率的论文，四个月后发表了《Green：在程序分析中减少、重用和回收约束》。

“关于重用约束的研究最终被证明具有普适性，”Geldenhuys说。“虽然我们开始这项工作是为了扩展概率分析，但同样的想法在其他类型的符号执行上也产生了奇迹。那项工作有了自己的生命。”

南非公民Geldenhuys和Visser在斯泰伦博斯大学攻读计算机科学硕士学位时，在同一导师指导下相识。Geldenhuys于2005年在芬兰坦佩雷理工大学获得技术博士学位。他回到斯泰伦博斯大学担任教授，直到2020年全职加入某中心。

Visser于1998年在英国曼彻斯特大学获得计算机科学博士学位。在硅谷NASA Ames研究中心工作10年后，Visser回到斯泰伦博斯大学任教，并与Geldenhuys重聚。

Dwyer于2011年获得富布赖特学者资助，在斯泰伦博斯大学进行研究时结识了Geldenhuys和Visser。当他们在分布式问题上应用符号执行工具一起工作时，他们偶然发现了2012年那篇论文的灵感。

“我们逐渐认识到，即使没有任何随机语句或任何暗示分布的程序，本质上也是概率性的，”Visser说。“例如，如果某个值应该等于42，那么输入实际上为42、该特定执行发生的可能性非常小。于是我们开始沿着这个思路思考：‘我们能否从代码中的执行路径可能性角度来分析程序？’ 这最终成为了这篇论文的核心思想。”

Visser在担任某中心顾问一年多后，于2019年11月全职加入某中心。Visser主要从事某中心CodeGuru的开发工作，这是一个为开发者提供智能建议以改进代码质量并识别应用程序中最耗资源代码行的工具。

Geldenhuys在某中心网络服务的某中心自动推理组工作，致力于开发和验证工具及技术，以证明所有某中心网络服务客户使用的权限管理系统的正确性和安全性。

“这是一个非常有趣的挑战，”Geldenhuys说。“有数百万客户依赖这个系统。我喜欢解决那些能用我的技能让客户生活变得更美好的问题。”