一句话:提出 JUSTGen,用 DSL 和 SMT 发现 JNI 规范未指定情形并生成测试,揭示 JVM 调试检查的缺陷。
JNI 让 Java 应用调用 native 库,但跨语言互操作语义复杂,正确开发 JNI 程序困难。JVM 默认不校验错误的 JNI 互操作,仅在启用 -Xcheck:jni 时检查,其检查质量尚不明确。本文提出 JUSTGen:用 DSL 描述 JNI 规范,借助 SMT 求解器自动发现规范未指定情形,并生成触发这些行为的测试程序,实证评估 -Xcheck:jni 的验证能力。实验发现 JVM 调试特性未验证数千个未指定情形,可导致 Java 类型系统违反和内存破坏等严重运行时错误;向 JVM 厂商报告 792 个案例,其中 563 个已修复。作者据此认为 JNI 规范应明确缺失语义,调试特性应完整支持。
Java Native Interface (JNI) provides a way for Java applications to access native libraries, but it is difficult to develop correct JNI programs. By leveraging native code, the JNI enables Java developers to implement efficient applications and to reuse code written in other programming languages such as C and C++. Besides, the core Java libraries already use the JNI to provide system features like a graphical user interface. As a result, many mainstream Java Virtual Machines (JVMs) support the JNI. However, due to the complex interoperation semantics between different programming languages, implementing correct JNI programs is not trivial. Moreover, because of the performance overhead, JVMs do not validate erroneous JNI interoperations by default, but they validate them only when the debug feature, the -Xcheck:jni option, is enabled. Therefore, the correctness of JNI programs highly relies on the checks by the -Xcheck:jni option of JVMs. Questions remain, however, on the quality of the checks provided by the feature. Are there any properties that the -Xcheck:jni option fails to validate? If so, what potential issues can arise due to the lack of such validation? To the best of our knowledge, no research has explored these questions in-depth. In this paper, we empirically study the validation quality and impacts of the -Xcheck:jni option on mainstream JVMs using unspecified corner cases in the JNI specification. Such unspecified cases may lead to unexpected run-time behaviors because their semantics is not defined in the specification. For a systematic study, we propose JUSTGEN, a semi-automated approach to identify unspecified cases from a specification and generate test programs. JUSTGEN receives the JNI specification written in our domain specific language (DSL), and automatically discovers unspecified cases using an SMT solver. It then generates test programs that trigger the behaviors of unspecified cases. Using the generated tests, we empirically study the validation ability of the -Xcheck:jni option. Our experimental result shows that the JNI debug feature does not validate thousands of unspecified cases on JVMs, and they can cause critical run-time errors such as violation of the Java type system and memory corruption. We reported 792 unspecified cases that are not validated by JVMs to their corresponding JVM vendors. Among them, 563 cases have been fixed and the remaining cases will be fixed in near future. Based on our empirical study, we believe that the JNI specification should specify the semantics of the missing cases clearly and the debug feature should be supported completely.