学术与产业协作为亚马逊客户提供真实世界安全保障

2018年7月16日，亚马逊杰出科学家拜伦·库克在牛津大学联合逻辑会议上发表主题演讲，这是一个自1996年以来每四年举办一次的计算机逻辑聚会。

在演讲中，库克描述了他的团队如何使用名为cvc（合作有效性检查器）的开源软件工具来识别代码中的逻辑问题并修复它们。坐在台下的斯坦福大学教授克拉克·巴雷特已经在cvc项目上工作了近20年。

Cvc被开发用于分析编码为可满足性模理论问题的验证问题。SMT是形式化方法的支柱，即使用自动推理来证明程序或系统将按预期运行。通过大规模应用SMT，cvc可以检测代码和系统中的逻辑错误，比如用于身份验证和访问管理的系统。

"我有点震惊，真的很兴奋，"巴雷特说。"这真正开始于一个令人兴奋的时刻，意识到，嘿，我们的工作正在被亚马逊使用。"

库克和巴雷特的邂逅最终促成了一项持续多年的研究合作，最终巴雷特在2023年成为亚马逊学者。最初，亚马逊通过亚马逊研究奖项目向巴雷特在斯坦福工程学院的实验室提供小额资助；随着研究的进展，这些资助逐步增长为更大的资金承诺。这项资助支持的基础研究，加上两个团队之间的深度技术合作，使得cvc5的开发成为可能，这是该开源软件的最新版本。Cvc5为亚马逊客户和更广泛的行业都提供了重大价值，同时推进了学术研究。

举例来说，cvc5被用于自动推理检查，这是亚马逊Bedrock的一个新功能，用于根据组织政策验证自然语言内容。它为访问策略分析工具提供动力，包括身份和访问管理访问分析器，这是一项帮助客户安全管理AWS资源访问的服务。最近，亚马逊开始在Kiro中部署cvc5进行规范分析和测试生成，Kiro是一个新的智能体开发环境。在这些应用中，cvc5现在每天处理约10亿次求解器调用，为AWS客户增强了安全性、可靠性和持久性。

与巴雷特共同参与该项目的是AWS的高级首席应用科学家罗伯特·琼斯，他们两人在斯坦福大学读博士时师从同一位导师。多年来还有许多渴望测试自己技能的学生和博士后参与了该项目。其中不少人后来加入了亚马逊，开发新的实现和应用，延续了他们作为学生研究者时开始的工作。

"真正有趣的是，比如刚完成博士学位的人，经常为长期存在的研究挑战带来新的见解，因为他们以不同的方式思考这些问题，"琼斯说。"我发现协作最好的部分是不同的人倾向于为同一个问题构建不同的心理模型。当这些模型结合在一起时，你经常对如何思考问题或如何将其映射到你已经知道如何解决的不同问题有新的见解。"

学术研究和商业资助的成功结合可以产生巨大影响，但正如巴雷特指出的，需要专注于可实现的目标。巴雷特说，很容易陷入一个有趣的项目想法，但最终导致实际的死胡同。

"如果你在象牙塔里，构建你的工具，而你无法接触到真正的问题，很容易构建错误的工具。我实际上犯过这个错误，"他说。"你造了一把锤子，然后四处寻找钉子，但找不到任何合适的东西。你对某种特定方法感到兴奋，但没有考虑这种方法可能适用于什么。所以我现在更喜欢相反的方式，我去找一个真正的问题，然后退一步说，'我们实际上可以使用什么方法来解决这个问题？'"

当你改变代码时，他说，"80%的时间它会做得更好，20%的时间它会做得更差。在某些情况下，这实际上不是那么好。"他补充说，将精华与糟粕分开对于产生强大和可扩展的代码至关重要，需要大规模测试来发现和修复在代码更改时可能无意中引入的问题。

琼斯说，在这个级别分析交互需要多个头脑，人越多越好。古话"人多力量大"在混合公共研究和实际应用时特别有用。

"我真的喜欢处理需要多人解决的难题。我享受科学中涉及的协作，"他说。"我一直发现多个头脑一起解决同一个问题比一个人更好。"

巴雷特和琼斯都同意，使这项工作成功的是愿意从学术和商业两个角度来看待问题。有时纯研究目标可能有非常有益的结果，有时则不然，但将这两种方法融合在一起来解决严重问题可以带来巨大的好处。

两人都同意，沟通是关键。

"学术界的难题之一是知道哪些问题最重要，以及这些问题如何影响行业中遇到的现实问题，"琼斯说。"能够更开放地讨论我们正在努力解决的问题类型，以及克拉克告诉我们他的研究议程，这对我们双方都有帮助。它使亚马逊能够指出感兴趣的领域，并帮助克拉克理解我们在实践中尝试应用这些工具和技术时每天遇到的具体问题。"

Q&A

Q1：cvc5是什么软件？它在亚马逊有什么用途？

A：cvc5是一个开源软件工具，用于识别和修复代码中的逻辑问题。在亚马逊，它被用于自动推理检查、身份和访问管理分析器以及智能体开发环境Kiro中，每天处理约10亿次求解器调用，为AWS客户提供安全性、可靠性和持久性保障。

Q2：学术界和工业界合作研发软件有什么好处？

A：学术界和工业界合作可以结合理论研究和实际应用需求。学术界提供新颖的理论见解和研究方法，而工业界提供真实的问题场景和大规模测试环境。这种合作避免了纯学术研究可能脱离实际的问题，确保研发的工具能够解决真正的业务需求。

Q3：为什么说沟通在学术产业合作中很重要？

A：沟通帮助学术界了解哪些问题在工业界最重要，以及研究成果如何影响现实应用。同时，工业界可以向学术界说明他们面临的具体技术挑战，学术界则可以分享研究议程。这种双向沟通使合作更加有效，确保研究方向与实际需求对接。