1年前 (2023-03-27)  相关技术 |   抢沙发  269 
文章评分 0 次,平均分 0.0

静态分析器在程序运行之前捕获错误的能力正在稳步提高。在Facebook使用Infer静态分析器https://fbinfer.com/)的过程中,我们经常被问及Infer与其他开源分析工具(如Findbugs、错误倾向和Clang静态分析器)之间的差异。一个主要区别是程序间错误,或涉及多个程序之间交互的错误。

我们将看看Infer在Java和C中发现的两个程序间错误示例——一个来自开源DuckDuckGo Android应用程序,另一个来自OpenSSL C代码。上述工具无法发现这些错误,这些工具仅执行程序内分析,或者在Clang静态分析器的情况下,仅执行文件内分析(可能是程序间分析,但仅限于一个翻译单元中的程序,一个包含在内的文件)。

程序间错误是重要的,因为它们构成了Infer发现的几种类型的错误中的大多数。Facebook开发人员已经修复了数千个这样的bug,这表明静态分析发现它们可能会产生巨大影响;我们包括一些来自Infer在Facebook部署的程序间错误频率数据。正如我们所发现的,过程间分析可以部署到大型且快速变化的代码库中,这些代码库由数百万行代码组成,每天要进行数千次修改。

DuckDuckGo

面向隐私的互联网搜索引擎DuckDuckGo的Android应用程序代码在GitHub上提供。在Infer报告后,DuckDuckGo开发人员修复了应用程序早期版本的以下问题:

src/com/duckduckgo/mobile/android/activity/DuckDuckGo.java:867: error: NULL_DEREFERENCE
object `feedObject` last assigned on line 866 could be null and is dereferenced by call to `feedItemSelected(...)` at line 867.
    
864.
865. public void feedItemSelected(String feedId) {
866. FeedObject feedObject = DDGApplication.getDB().selectFeedById(feedId);
867. feedItemSelected(feedObject);

与此报告一起,Infer生成了一个由18个步骤组成的过程间错误跟踪,这些步骤通过过程getDB()、selectFeedById(feedId)和feedItemSelected(feedObject)。有两个不同的feedItemSelected()方法,一个接受FeedObject作为参数,另一个接受String。下面是第866行selectFeedById(feedId)调用访问的代码:

src/com/duckduckgo/mobile/android/db/DdgDB.java:483: start of procedure selectFeedById(...)
    
482.
483. public FeedObject selectFeedById(String id){
484. FeedObject out = null;
485. Cursor c = null;
486. try {
487.   c = this.db.query(FEED_TABLE, null, "_id=?", new String[]{id}, null, null, null);
488.   if (c.moveToFirst()) {
489.    out = getFeedObject(c);
490.   }
491.  } finally {
492.      if(c!=null) {
493.            c.close();
494.      }
495.  }
496.  return out;
497. }

selectFeedById()有可能返回null,即当db.query()在第487行返回的游标c为空游标时。第488行对c.moveToFirst()的调用将返回false。

当分析feedItemSelected()中标记了空问题的原始代码时,Infer需要在第866行意识到空是可能的。错误实际上在第867行报告,这是另一个方法调用,在本例中涉及以下方法:

src/com/duckduckgo/mobile/android/activity/DuckDuckGo.java:842: start of procedure feedItemSelected(...)
    
841.
842.  public void feedItemSelected(FeedObject feedObject) {
843. // keep a reference, so that we can reuse details while saving
844.    DDGControlVar.currentFeedObject = feedObject;
845.    DDGControlVar.mDuckDuckGoContainer.sessionType = SESSIONTYPE.SESSION_FEED;
846.
847     String url = feedObject.getUrl();

这里我们看到feedObject在第847行被取消引用。因此,如果feedObject为空,我们将有一个空指针取消引用。

我们有一个过程间错误,其中null的源在一个方法中,null的汇在第二个过程中,源和汇过程从第三个过程调用。我们需要程序间推理来发现这个问题,因为纯粹的程序内工具不会发现这个错误。

如果在代码中添加了关于可空性和不可空性的注释,Findbugs、易出错工具和其他工具可以发现此错误。然而,在编写的代码中发现bug需要过程间推理。

理论:规范和总结

Infer使用一种称为合成、基于摘要的分析的技术发现了DuckDuckGo问题。Infer不是每次遇到一个方法时都重新评估它,而是参考该方法可能做什么的摘要或近似值。组合分析器计算摘要而不查看方法的所有调用位置;Infer尝试在一次传递过程中计算尽可能的摘要。

Infer将其摘要表示为程序逻辑中的规范。更详细地说,规范是先决条件和后决条件的一对(前、后)(熟悉于霍尔逻辑或其更现代的化身,分离逻辑)。(pre,post)对意味着如果逻辑属性pre在执行过程之前保持,post将在执行过程之后保持。有时会使用几个帖子来表示帖子的分离(“或”)。摘要是前/后对的集合,其中一个前财产需要在调用位置匹配才能继续推理。

对于selectFeedById(String id)方法,Infer计算

PRE: this.db |→ - (db is non-null and points to a valid object)
    
POST1: return == null (we are returning a null feed object)
POST2: return |→ - (we are returning a valid, non-null feed object)

也就是说,在摘要中有一个单独的前/后对,其中后是析取POST1或POST2。原始过程feedItemSelected(StringfeedId)中的符号执行将在第866行考虑feedObject的两种情况:根据两个后置条件,null和非null情况。然后,对于第867行的下一条语句,我们必须考虑调用feedItemSelected(feedObject)的空参数。再次,我们通过查询feedItemSelected的计算前/后规范来处理这个问题。摘要有五个前/后规范,但它们都包含

PRE: feedObject |→ - (feedObject is a valid, non-null object)

Infer选择此作为前提条件,因为我们需要feedObject为非空;否则,将发生错误(NullPointerException)。现在,当符号执行尝试feedItemSelected(feedObject)但feedObject==null时,我们无法满足前提条件。正是在这一点上,我们试图构建一个逻辑证明,证明没有运行时错误,并报告错误。

重要的一点是关于代码的推理

864.
865.  public void feedItemSelected(String feedId) {
866. FeedObject feedObject = DDGApplication.getDB().selectFeedById(feedId);
867. feedItemSelected(feedObject)

可以只使用它调用的程序的摘要来完成,而不需要(再次)深入研究它们的身体。对于Infer的大规模操作,过程抽象原则的应用是至关重要的,因为它能够独立于调用站点构建摘要。

Infer的总结概念还有其他细微差别,它比前面提到的前/后规范更详细。为了让Infer报告错误的跟踪,除了前/后规范之外,它还记得在摘要中显示代码路径的跟踪信息。而且,前/后规范本身比上述规范更复杂,为了说明的目的,这些规范被手动简化。您可以在这里找到Infer为这些程序计算的详细规格。

OpenSSL

我们已经展示了基于摘要的组合程序分析如何在Java中有效地发现大规模的过程间错误。它也适用于C语言。例如,2014年,我们向GitHub提交了在OpenSSL中发现的15个空引用和内存泄漏Infer,该项目的核心开发人员之一解决了这一问题。一些空解引用相当复杂,这说明了我们想对误报率提出的一点,即在任何程序运行中都不会发生的错误。

以下是Infer的报告之一:

apps/ca.c:2780: error: NULL_DEREFERENCE
pointer `revtm` last assigned on line 2778 could be null and is dereferenced at line 2780, column 6
2778. revtm = X509_gmtime_adj(NULL, 0);
2779.
2780.  i = revtm→length + 1;

问题是过程X509_gmtime_adj()在某些情况下可能返回null。总体而言,Infer发现的错误跟踪有61个步骤。此外,null的源(对X509_gmtime_adj的调用)在返回null之前在其子空间中有36个步骤;跟踪深入五个过程,最终在过程ASN1_TIME_adj()的调用深度4处从文件crypto/ASN1/a_TIME.c返回null。

crypto/asn1/a_time.c:113:6: Condition is true
111.
112. ts=OPENSSL_gmtime(&t,&data);
113. if (ts == NULL)
114.   {
115.      ASN1err(ASN1_F_ASN1_TIME_ADJ, ASN1_R_ERROR_GETTING_TIME);
116.       return NULL;
117. }

X509_gmtime_adj(NULL,0)返回NULL的条件有些复杂,Infer无法确定它们肯定会在程序运行中发生。Infer不会在每次报告潜在错误时构造一个一直返回main()的跟踪。相反,在试图构建逻辑证明的过程中,Infer有时会报告构建此类证明时遇到的困难。

在本例中,OpenSSL开发人员解决了这个问题。在代码库的其他地方,Infer报告被阻止,因为OPENSSL_gmtime()附带了一个空检查,这进一步证实了这个问题值得提出。

我们还在OpenSSL上运行Clang静态分析器。它能够执行文件内分析,其中的一个子集可以是程序间的,但据我们所知,不能在文件之间进行。此示例需要文件间分析;事实上,当我们在OpenSSL-1.0h上运行CSA时,它没有发现错误。值得注意的是,CSA报告的错误集与Infer不同,因此在C代码上运行这两个分析器是有意义的,同样,为Java分析运行Findbugs和Error。

一个有趣的问题是,这份OpenSSL报告是假阳性还是真错误。即使过了几个小时,我们仍然不确定。在大规模使用静态分析时,这种情况并不罕见:对于大型代码,有时工具和人员都不确定是否会发生错误。这就是为什么在部署静态分析后,我们对假阳性率的概念的重视程度不如学习其原理时的重视程度。由于代码基数庞大且不断变化,对于所有实际目的来说,这个速率都是无法测量的。一个更为人所知的概念是修复率,它能更好地说明分析给程序员带来的价值:由于开发人员的代码更改而消除的分析器问题的比例。

速度和渐进主义

为了说明Infer在OpenSSL(一个由超过300000行代码和700个文件组成的代码库)上的性能,我们分析了代码,对其进行了修改以修复上述错误,然后以增量方式重新分析了它。

$ # compile to infer's intermediate language
$ time infer capture -- make
[...]
real 5m0.545s
user 4m10.563s
sys 1m3.104s
    
$ # analyze the entire OpenSSL project, using one CPU only
$ time infer -j 1 analyze
[...]
real 22m20.320s
user 20m24.831s
sys 1m31.722s

$ # fix the bug
$ vi apps/ca.c
[...]
    
$ # run infer incrementally, using one CPU only
$ time infer -j 1 run -reactive -- make 
[...]
real 0m41.296s
user 0m36.920s
sys 0m2.379s

Infer在代码更改上的运行速度比在整个项目上快得多。反应模式仅对更改的文件执行捕获和分析的翻译工作。OpenSSL开发人员给出的apps/ca.c中的代码修复涉及插入一个简单的空检查。

2778 revtm = X509_gmtime_adj(NULL, 0);
2779
2780 if (!revtm)
2781 return NULL;
2782
2783 i = revtm→length + 1;

这种更快的增量分析有助于Infer在Facebook的部署模型,它与代码审查系统集成在一起;如果在出现代码更改时必须对整个程序进行操作,那么即使是线性时间分析也会太慢。

程序间修复的频率

人们有时会问,程序间分析是否会捕捉到许多本地分析无法捕捉到的错误,以及我们是否需要程序间分析。毕竟,本地工具会跟踪我们在Infer中讨论的一些相同类别的错误(例如,空引用)。

我们查看了Facebook开发人员修复的100份最新Infer报告,分为几个错误类别。由于文件间错误必然被分类为程序间错误,请注意,程序间错误是下表中最右两列中的错误。

过程内意味着错误发生在单个函数的范围内。文件内但过程间意味着错误跟踪经过多个过程或函数,涉及多个过程,但支持跟踪和推理仅限于单个文件。Inter-file是一个跨多个文件的程序间错误。

使用Infer静态分析器查找程序间的bug

我们发现,Java中修复的大多数空引用都是过程间的。在Objective-C中,更大的比例是程序内的。产生差异的部分原因是,我们已经实现了许多过程内检查,这些检查基于Facebook开发人员的输入来搜索ObjC特定的代码模式。程序间错误仍然占不可忽略的比例。

线程安全性是对用@ThreadSafe注释的Java类中方法之间的数据竞争的检查。同样,大多数是程序间的,甚至是文件间的。数据竞赛是对字段的访问或对容器的调用,这些字段和容器通常位于与注释的@ThreadSafe不同的类中。出于本表的目的,当我们有一个涉及两个过程的读/写竞争,但访问在过程本身内时,我们认为这是一个过程内竞争。发现它需要两个程序内推理,关于两个程序。

Allocates Memory是一种检查是否可以从注释为@NoAllocation的过程访问分配。

线程安全性和分配内存基于专门的过程间分析,不同于DuckDuckGo和OpenSSL的示例bug中提到的基于分离逻辑的分析。线程安全使用摘要的概念来记录访问和锁定信息。Allocates Memory是注释可达性分析器的一部分,其摘要存储跟踪信息。这两个分析器使用一个框架Infer.AI来编写Infer中的复合静态分析器。

Bad Pointer Comparison是Objective-C的一种lint检查,用于识别在比较中何时将NSNumber*等装箱基元类型强制为布尔值。它是用我们的AST语言AL编写的。我们将其作为不需要程序间推理的有用检查的一个例子,用于平衡。

结论

随着静态分析器越来越常见,它们通常用于执行简单的过程本地(过程内)检查。这些分析,例如开源工具Findbugs、Error-prone、ClangStaticAnalyzer和AndroidLint,部署相对广泛,并提供了积极的价值。例如,一个谷歌静态分析团队报告称,它广泛使用内部程序内检查,但避免大规模的程序间分析。Facebook在内部部署了几个linting和程序内分析解决方案,Infer在AL语言中包含了自己的解决方案。

相比之下,程序间分析似乎不太常用,但也有其他关键发展。两个重要的部署是Microsoft的前缀和静态驱动程序验证程序;静态驱动验证程序具有有限的扩展能力,而Prefix以自底向上的方式工作,就像早期版本的Infer一样,并且可以扩展到大型代码库。Coverity的专有静态分析器还支持程序间分析,使用一些与Infer相似的技术和其他不同的技术。这些努力提供了背景,但我们还没有进行详细的比较。一项对几种高级静态分析工具的独立研究发现,它们捕捉到了不同的错误集,这表明没有一种最好的分析器可以取代所有其他分析器。

因为Infer是合成的,这意味着过程的摘要是独立于调用上下文生成的,所以它可以扩展到大型代码库,并在频繁的代码修改上逐步工作。一般来说,我们觉得除了linting之外,高级静态分析技术还有很多潜力,比如检查程序间和其他更深层错误的技术。特别是,无论是在学术界还是在工业界,组合程序分析都将从进一步发展中受益。

原文地址:https://engineering.fb.com/2017/09/06/android/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer/

 

除特别注明外,本站所有文章均为老K的Java博客原创,转载请注明出处来自https://javakk.com/2802.html

关于

发表评论

表情 格式

暂无评论

登录

忘记密码 ?

切换登录

注册