一文了解全面静态代码分析
在开发具有安全性、可靠性和合规性的软件时,全面静态代码分析是一种有效的方法。在这里,我们将就静态分析而言,讨论全面静态代码分析的不同之处,阐述全面静态代码分析的重要性,以及如何进行全面静态代码分析。
什么是全面静态代码分析
全面静态代码分析,或只是全面分析,是指分析结果的完整性或“健全性”。静态代码分析工具据称能够提供可靠的分析结果,这意味着如果某个软件中存在特定的缺陷或漏洞,该分析工具将报告上述问题。
如果不确实是否存在问题,则提供某种形式的警告,这样就不会“漏掉”任何问题。
(注:这些问题在Helix QAC工具中被归类为可能存在的问题,如无必要,则可以不进行全面分析。)
全面静态代码分析不同于其他形式的静态分析,其他形式的静态分析结果可能基于在一定时间或资源范围内可能发生的情况。
鉴于程序的运行时行为建模需要某些近似值(例如,缺乏对程序输入或操作系统状态的了解),全面静态代码分析需要采用Over-approximations(过近似)。
Over-approximations(过近似)用以保证不存在漏报(对于给定的漏洞类型),而under-approximations(下近似)首先保证的是没有误报而却可能有漏报。
而其他形式的静态分析没有表现出这种严格性,可能既包含Over-approximations(过近似) 又包含 under-approximations(下近似)。
全面静态代码分析工具和非全面静态代码分析工具可能会为程序的特定部分提供一份健康报告,而全面静态代码分析工具引擎提供了额外的保证,即在提供这一健康证明的同时,所有可能性和所有路径均已得到验证。
全面静态代码分析工具的工作原理
当提到全面分析时,我们通常考虑更复杂的过程间和过程内控制以及数据流分析形式,与当今最先进的静态分析工具的工作原理相同。
相较于更为简单的代码语法和语义分析,不同之处在于控制和数据流静态分析通常与检测更为复杂的问题有关,包括:
- 空指针错误引用
- 数组或缓冲区下溢和上溢
- 使用未初始化的对象
- 分配内存和释放内存异常
- 数字上溢、下溢和环绕
- 除以零
- 死代码
- 数据竞争、死锁和其他并发冲突
控制和数据流分析是一项高计算负载的任务,因为必须考虑系统的所有可能输入以及通过系统所有可能的控制流路径。事实上,由于控制流和数据流分析的蛮力穷举算法会导致分析时间指数暴涨,因此很少采用该方案。符号执行和抽象解释算法将是一个更好的选择。
根据Roberto Amadini、Graeme Gange、Peter Schachte、Harald S?ndergaard 和Peter J. Stuckey的《抽象解释、符号执行和约束》,“抽象解释是一个静态代码分析框架,对程序所有可能运行时状态适用过近似。”
而“符号执行是可达性分析的框架,它试图探索程序所有可能的执行路径。”抽象解释和符号执行在执行期间都以不变量或路径条件的形式保持约束,这些路径约束决定了可以执行何种可能路径以及可以在各种数据源中保存哪些值。
但需要注意的一点是,虽然抽象解释较为全面,但符号执行却未全面执行。
为什么全面静态代码分析很重要?
全面性是安全关键软件系统中的一个重要因素,尤其是能够保证软件不存在任何正在检查的编码缺陷。也就是说,全面分析可用于确保软件中不存在错误。
基于此,在汽车系统的ISO 26262功能安全(FuSa)标准中,抽象解释分析被明确引用为软件单元验证方法(表7,方法1i)。
如何使用Helix QAC工具执行全面静态代码分析
由于能够提供深入和高度准确的分析结果,30多年以来,Helix QAC一直是值得信赖的静态代码分析工具。Helix QAC能够进行全面的静态分析,一直是符合合规性的严格监管和安全关键行业的首选工具。
但为了能在Helix QAC工具中启用全面分析,需要执行以下步骤:
需要将数据流深度(Dataflow Settings)设置为最大值 (5),这将添加多个 -prodoption,如上面的屏幕截图所示。(请参阅 QAC 或 QAC++ 组件手册中的"分析超时"一节,了解为什么该类"超时"设置对于全面分析是必需的。)此外,“df::inter=5”和“inter-TU Analysis”虽然不是全面分析所必需的,但可以以额外的计算成本启用,以减少可能需要报告的问题数量。这些设置可用于启用程序间和程序内分析。
为什么使用Helix QAC工具进行全面静态分析
亲自体验Helix QAC工具的全面静态分析对代码质量和全面性的影响。
立即联系 龙智 体验,开启您的Helix QAC免费试用之旅。
作者简介:
史蒂夫·霍华德(Steve Howard)
静态代码扫描工具(SAST)Perforce系统产品倡导者, 史蒂夫在软件验证和确认领域拥有超过15年的经验,尤其是在静态代码分析方面经验颇丰。
史蒂夫拥有威尔士大学计算机科学一等学位和多个软件测试和安全认证的研究生学历。