鉴释人物丨专访首席科学家李隆： 重一步业务逻辑验证，省百步漏洞补缺

作者：李隆博士，目前担任鉴释科技核心技术的首席科学家，专注于代码验证基础架构。

近年来，随着人工智能和物联网的兴起和广泛应用，人们生活的方方面面被各种“智能”、“自动”的服务所渗透，为提供这些服务而开发的大量软件应运而生。遗憾的是，软件的质量并没有随着软件行业的大繁荣而得到明显提升，数据显示，82%的漏洞来源于应用程序；每 1000 行应用程序源代码中就有 1 个安全问题；每 1400 行中就有 1 个高危问题。软件规模、数量的大爆发也带来了漏洞数量的大爆发。

面临这样的严峻考验，由鉴释自主研发的爱科识应运而生。今天我们与鉴释首席科学家李隆博士就《用于验证超出常见漏洞的业务逻辑的工具》一同讨论。

01 您在去年的全球 C++技术大会上曾发表过关于“验证业务逻辑”的演讲，您能简单介绍一下什么是业务逻辑吗？

通常，一款软件的开发目标就是实现某种功能，实现这种功能的途径就是它的业务逻辑。一款软件可以很复杂，它可以拥有很多功能和实现，那么它的核心功能对应的就是它的核心的业务逻辑。实践中，一款软件往往会被拆分成小的功能模块分别实现后再整合。软件的开发过程就是开发、使用简单的业务逻辑以构建、整合成复杂的业务逻辑的过程。

02 业务逻辑漏洞的产生有许多种原因，您可以举些例子吗？

软件中的漏洞往往来源于设计或实现上的缺陷或偏差。对于一款待开发软件，如果功能描述不完整，或设计时考虑不全面，在拆解实现的过程中开发团队都会遇到问题，从而影响到核心功能；如果很明确知道它所要提供的功能，那么就可以采用已有的成熟的解决方案来实现这个功能。但在设计实现的过程中，即便顶层描述十分清晰，在将自然语言描述翻译为开发所使用的编程语言时，往往会出现偏差，从笼统的语言描述到细节的实现，存在差距并不稀奇，这也是 bug 的来源。

其次，一款复杂的软件在开发过程中往往需要多个团队的支持。在各个团队明确分工后，开发人员对功能的理解、实现都可能会出现一定程度的偏差。如果开发团队在不同模块的接口之间的功能描述不够清晰、实现存在偏差，那么整个程序跑起来就可能存在问题。尤其是软件功能增强时，对原有功能改造以及新加入开发人员时，更容易发生类似情况。

此外，开发人员对第三方或者库函数的理解偏差，也是软件漏洞的一个来源。Chrome 的 0day 漏洞 cve-2019-5786 就是开发者对 std::move()的理解不全面而导致的。对新标准、新接口的尝鲜心理普遍存在于软件开发者中，但在真正使用这些新事物之前，开发者自身需要投入时间精力，学习并真正理解。而且，并不是所有的新标准、新接口的设计也都是合理的，比如这里提到的 std::move()，其功能在一个编译器的优化流程中就应该能自动实现。通过开放一个接口让所有开发者来尝试实现编译器优化未能完成的工作，同时提供了一个可能导致大量漏洞的来源，我个人很难理解其目的和意义。

03 我们如何高效且有效地验证业务逻辑的漏洞？使用 FSM(Finite-State Machine 有限状态机)会对客户带来哪些好处？如果这是个复杂的算法，那扫描代码会非常费时吗？

如果只验证主要功能，其实不费时。简单说，这就是从语言描述转换成扫描工具能够认识的检测原语的一个过程。那么如何验证这些漏洞呢？

首先，我们在工具上提供接口，让用户把用语言描述定义的软件功能，即业务逻辑，能够映射到其对应的开发语言上。比如，我用某语言写了一段程序，又有一段语言描述，这时我们提供相同编程语言的接口，映射到鉴释的接口函数上，再通过接口函数的描述，对软件进行扫描，查看真正的实现过程中是否符合了语言描述中所要实现的功能。

FSM（Finite-State Machine 有限状态机）是一个学术说法，我们在验证过程中或多或少都有有限状态机的参与的，比如先做什么，得出结果后再做什么，只不过没有用很严格的数学语言表述出来。其实语言描述到严格的数学描述，也是会有不匹配、不完整的情况，也是出现漏洞的原因之一。

现在大家都提倡左移，越早发现问题越好，降低弥补成本。软件生命周期包括：设计、实现、测试，到交付使用。在用户开始使用时才暴露出来的错误，其修复的人力和时间成本最高，远超过开发时就发现并修复的成本。就是因为一个软件从设计到实现功能再重新改，时间、人力成本都很高，与其在用户使用后才报错，不如在内部开发的早期就保证“我做的是客户想要的”。

04 为什么验证业务逻辑这么重要，如果不做验证，软件将出现哪些问题

最大的问题就是提供的功能有偏差，过多或过少。过少弥补的方法很简单，把缺少的部分补添加就可以。但如果你提供了过多的功能，把不想让用户接触到的东西也暴露了，比如敏感数据等，这就会导致你的软件中存在安全漏洞。

如果不能严格的确认软件的业务逻辑，在被认可的合理范围内交付软件，那么对于恶意攻击方来说，你交付出去的不是软件，而是通向庞大隐私数据的入口，后果将会相当严重。就比如去年在新加坡就有黑客利用家用监控设备的漏洞，将监控视频上传至网络，造成了不小的轰动，也警醒人们要注意软件安全。

05 爱科识在验证业务逻辑上有什么帮助？

除了刚才提到的早发现早纠正，降低时间、人力成本，保证软件安全以外，其实只要能帮助用户把语言描述的功能在其对应的编程语言上验证，已经是很大程度上的帮助了。毕竟目前业内能实现该功能的软件少之又少。

许多客户需要针对自己业务逻辑来做定制化的验证，而很难找到优秀工具来实现，爱科识就这样应运而生了。由爱科识提供表达能力足够强的接口系统，客户可将其特定的业务逻辑从简单的文字描述转换成可通过扫描代码获取结果的表现形式。这就是爱科识的定制化过程。

06 关于“验证业务逻辑”，传统的形式化验证与爱科识的形式化验证有什么区别？

传统形式化方法是严格的数学过程。想要将语言描述转换到严格的数学表达，首先，用人门槛就很高，且很难验证得到的数学表达是准确的，转换和验证者都需要熟知业务逻辑及数学方法。其次，一旦顶层语言描述改变，大量需要手工完成的证明过程也需要推倒重来，效率低下。这两点决定了严格的数学证明过程耗时耗力。在传统形式化方法的实践中，为了验证一行软件源代码，验证过程中需要写 17 行的代码去验证。此外，传统形式化方法从证明失败的地方去倒推问题的症结所在并不容易。传统的形式化方法并不是一般的开发者能够轻易掌握的。

而爱科识由机器执行，不仅速度更快，效率更高，也降低了对使用者的要求，与传统形式化方法一样拥有高准确率，可以直观地帮助用户了解、认识到软件开发中的偏差问题。

在我们的实践中，80%的客户的定制化验证需求是可以通过有限的扫描引擎描述接口由客户自行实现的，而另外 20%的客户的特定的需求，则需要我们花费大量精力去帮助解决。爱科识不论在效率、准确性和性价比上都是突破性的。

由于自身的优秀功能与不可替代性，爱科识在行业内已经收获了不少厂商的信赖，如地平线、驭势科技、海信聚好联等等。爱科识的出现也在一定程度上鼓励了以往不愿意做业务逻辑验证的厂商，加入到重视业务逻辑的队列中，为厂商、乃至整个行业提升代码质量的路点亮了明灯。