Verifying Object Construction
Verifying Object Construction
复制标题
DOI：
10.1145/3377811.3380341
复制
发表时间：
2020-06
期刊：
影响因子：
--
通讯作者：
Martin Kellogg;Manli Ran;Manu Sridharan;Martin Schäf;Michael D. Ernst
中科院分区：
文献类型：
--
作者：
Martin Kellogg;Manli Ran;Manu Sridharan;Martin Schäf;Michael D. Ernst
在面向对象的语言中，构造函数通常具有必需和可选的形式参数的组合。对于程序员来说，为每个组合手工编写构造函数是繁琐和不方便的。对于客户端来说，大量的构造函数容易出错，并且由于大量的构造函数参数，客户端代码很难阅读。因此，程序员经常使用能够实现更灵活的对象构造的设计模式构建器模式、依赖注入或工厂方法。然而，这些设计模式可能过于灵活：并非所有逻辑参数的组合都能构造出结构良好的对象。当客户端使用构建器模式构造对象时，编译器不会检查是否提供了有效的值集。不正确地使用构建器可能会导致安全漏洞、运行时崩溃和其他问题。这项工作展示了如何静态地验证对象构造的使用，比如构建器模式。使用一种简单的规范语言，程序员指定允许哪些逻辑参数组合。我们的编译时分析检测可能不安全地构造对象的客户端代码。我们的分析是基于一个新的特殊情况下的类型状态检查，积累分析，模块化的原因积累的方法调用。由于积累分析不需要精确的混叠信息的健全性，我们的分析规模的工业计划。我们对超过900万行代码进行了评估，发现了包括以前未知的安全漏洞和大量使用的开源代码库中潜在的空指针违规在内的缺陷。我们的分析具有较低的假阳性率和较低的注释负担。我们的实施和实验数据是公开的。
In object-oriented languages, constructors often have a combination of required and optional formal parameters. It is tedious and inconvenient for programmers to write a constructor by hand for each combination. The multitude of constructors is error-prone for clients, and client code is difficult to read due to the large number of constructor arguments. Therefore, programmers often use design patterns that enable more flexible object construction-the builder pattern, dependency injection, or factory methods. However, these design patterns can be too flexible: not all combinations of logical parameters lead to the construction of well-formed objects. When a client uses the builder pattern to construct an object, the compiler does not check that a valid set of values was provided. Incorrect use of builders can lead to security vulnerabilities, run-time crashes, and other problems. This work shows how to statically verify uses of object construction, such as the builder pattern. Using a simple specification language, programmers specify which combinations of logical arguments are permitted. Our compile-time analysis detects client code that may construct objects unsafely. Our analysis is based on a novel special case of typestate checking, accumulation analysis, that modularly reasons about accumulations of method calls. Because accumulation analysis does not require precise aliasing information for soundness, our analysis scales to industrial programs. We evaluated it on over 9 million lines of code, discovering defects which included previously-unknown security vulnerabilities and potential null-pointer violations in heavily-used open-source codebases. Our analysis has a low false positive rate and low annotation burden. Our implementation and experimental data are publicly available.