重一步逻辑验证，省百步漏洞补缺

近年来，随着人工智能和物联网等新兴科技的广泛应用，各种“智能”、“自动”的科技服务已经渗透到人们生活的方方面面。在这些服务的背后，是无数个应运而生的软件和应用程序在支撑。遗憾的是，软件行业的大繁荣并没有带来软件代码质量的明显提升。Forrester研究数据显示，82%的漏洞来源于应用程序。与软件规模、数量的井喷一同出现的，是软件漏洞的大爆发，以及随之而来的隐私泄漏、网络欺诈等漏洞“后遗症”。

面对如此巨大的风险，企业内部的软件开发团队通过践行代码审查、各种测试以及代码分析以期减少代码中的漏洞从而提高代码质量。然而，这些方法往往也只能确保“砖块”可用，由这些“砖块”搭建起来的建筑是否符合设计、是否安全可靠就很难验证了。由此，用以检测软件设计或功能实现上的缺陷或偏差的“业务逻辑验证”就应运而生了。

偏差是漏洞之源

一款软件从设计到实现，往往会被拆分成许多小的功能模块，分别实现后再组装整合。大量简单的业务逻辑被用于构建复杂而又丰富的业务逻辑，设计或实现上的偏差或缺陷都会导致漏洞的产生。实践中，团队在拆解实现时，即使顶层描述十分清晰，将文字表达翻译为编程语言，将笼统的语言描述到细节的代码实现，其中可能产生的偏差不是代码审查、各种测试和代码分析能够轻易发现的。同时，如果开发团队在不同模块接口之间的功能描述不够清晰、实现存在偏差，程序一旦运行，问题就会浮出水面。尤其是在增强软件功能、对原有功能改造以及新加入开发人员时，发生类似状况的风险也会上升。

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

业务逻辑验证的重要性

业务逻辑验证，这个步骤可以帮助企业在被认可的合理范围内交付软件，而不是提供一个拥有过多或过少功能的半成品。功能过少的弥补方法相对简单，延长交付时间进行添加即可；而功能过多，则有可能提供了通往用户隐私数据的入口，从而导致不可挽回的严重后果，这类例子比比皆是。

图： 国家信息安全漏洞共享平台收集整理信息系统高危漏洞数量

在智能家居普及的今天，黑客利用监控设备的漏洞将监控片段上传至互联网，造成用户隐私泄露，甚至财产损失的事件屡见不鲜。据CNCERT披露的《中国互联网络发展状况统计报告》显示，2020年信息系统的高位漏洞数量同比2019年增长52.2%。诸多例子都在警醒我们软件安全问题就潜伏在身边。

验证业务逻辑，就是从语言描述转换成扫描工具能够认识的检测原语，并证明其成立的一个过程。传统的验证方法是将语言描述转换为严谨的数学表达，证明过程繁复且困难，不仅用人门槛极高，且费时费力。而且一旦顶层的语言描述发生变化，整个推导过程又需要从头开始。在传统形式化方法的实践中，为了验证一行软件源代码，验证过程中需要写17行的代码去验证。此外，传统形式化方法在证明失败的地点分析问题的症结所在并不容易，往往需要沿证明路径倒推检查。一般的开发者并不具备轻易掌握传统方法的能力。

为提供高效的业务逻辑验证服务，最好的方法是在静态代码扫码工具上提供接口，让用户将其业务逻辑映射到对应的开发语言上，再由机器快速高效的完成验证工作。即，如果有某语言编写的一段程序，又有它的一段语言描述，只要代码扫码工具提供了相同编程语言的接口，就可将语言描述的业务逻辑映射到的验证引擎可以识别的接口函数上，对软件进行扫描，查看真正的实现是否符合了语言描述中所要实现的功能。全程由机器执行的工具不仅拥有更快的速度、更高的效率，其对使用者的水平要求也更低，更能直观地帮助客户了解软件开发的具体症结所在。在实践中，80%的客户的定制化验证需求是可以通过有限的扫描引擎描述接口由客户自行实现的，而另外20%的客户的特定的需求，则需要花费大量精力去帮助解决。

左移已是开发标配

软件生命周期包括：设计、实现、测试以及交付使用。早发现问题早解决，弥补的成本也随之而下降。在用户开始使用时才暴露出来的错误，其修复的人力和时间成本最高，远超过开发时就发现并修复的成本。与其在用户使用后才报错，不如在内部开发的早期就践行业务逻辑验证，确保 “我做的是客户想要的”，因为一个软件到实现功能之后再重新设计改造，其时间、人力成本都会很高。

关于作者

李隆博士专注于代码验证基础架构，现任鉴释科技首席科学家。李隆于2008年在中科大获得计算机软件和理论博士学位。其学术研究集中在应用基于程序设计语言理论的技术构建可靠高效的软件上，并发表了数篇期刊和会议论文。毕业后，李隆博士加入了三星电子，从事高级技术小组的统计机器翻译工作。并于2010年加入HP编译器团队，从事HP Non-Stop编译器后端和SDK。

责编：Luffy Liu