Granullar: gradual nullable types for Java
Granullar: gradual nullable types for Java
复制标题
Grannullar：Java 的渐进可为空类型
DOI：
10.1145/3033019.3033032
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Ondřej Lhoták
中科院分区：
文献类型：
--
作者：
D. Brotherston;Werner Dietl;Ondřej Lhoták
Java和C#等面向对象语言允许所有引用都为空值。这支持许多灵活的模式，但导致了许多错误、安全漏洞和系统崩溃。% Static类型系统可以在编译时防止空指针异常，但需要注释，特别是对于使用的库。保守的默认值选择最严格的类型，防止许多错误，但需要大量的注释工作。Liberal默认选择最灵活的类型，需要更少的注释，但提供更弱的保证。可以提供可信的注释，但不进行检查，并且需要大量的手动工作。这些方法都不能很好地保证程序的检查部分与未检查部分是隔离的：即使使用保守的默认值，在检查部分也可能发生空指针异常。本文介绍了Granullar，一个渐进式的零安全系统。开发人员开始验证应用程序中最重要组件的空安全性。在未检查组件的边界处，Granullar插入运行时检查，以防止已验证系统被意外的空值污染。这确保了空指针异常只能发生在未检查代码内或检查代码的边界处;检查代码没有空指针异常。我们介绍了Java的Granullar，定义了检查-未检查的边界，以及如何生成运行时检查。我们评估我们的方法在真实的世界的软件标注为空安全。我们演示了运行时检查，以及可接受的编译时和运行时性能影响。Granullar能够以安全的方式将已检查的核心与不受信任的库相结合，从而提高了此类系统的实用性。
Object-oriented languages like Java and C# allow the null value for all references. This supports many flexible patterns, but has led to many errors, security vulnerabilities, and system crashes. % Static type systems can prevent null-pointer exceptions at compile time, but require annotations, in particular for used libraries. Conservative defaults choose the most restrictive typing, preventing many errors, but requiring a large annotation effort. Liberal defaults choose the most flexible typing, requiring less annotations, but giving weaker guarantees. Trusted annotations can be provided, but are not checked and require a large manual effort. None of these approaches provide a strong guarantee that the checked part of the program is isolated from the unchecked part: even with conservative defaults, null-pointer exceptions can occur in the checked part. This paper presents Granullar, a gradual type system for null-safety. Developers start out verifying null-safety for the most important components of their applications. At the boundary to unchecked components, runtime checks are inserted by Granullar to guard the verified system from being polluted by unexpected null values. This ensures that null-pointer exceptions can only occur within the unchecked code or at the boundary to checked code; the checked code is free of null-pointer exceptions. We present Granullar for Java, define the checked-unchecked boundary, and how runtime checks are generated. We evaluate our approach on real world software annotated for null-safety. We demonstrate the runtime checks, and acceptable compile-time and run-time performance impacts. Granullar enables combining a checked core with untrusted libraries in a safe manner, improving on the practicality of such a system.