paperbot · PL 论文追踪

全部论文 待读 收藏

P2 JUSTGen: Effective Test Generation for Unspecified JNI Behaviors on JVMs

JUSTGen:针对 JVM 上未指定 JNI 行为的有效测试生成
ICSE 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)2021匹配度 3/10 · 论文属于程序语言与软件测试/形式化方法交叉,使用 DSL 和 SMT 发现 JNI 规范未指定行为并生成测试,具有工业 JVM 实践价值;但它不涉及 LLM/Agentic 程序、静态分析、浮点程序分析或贝叶斯程序分析,与用户当前核心研究方向仅有较弱的 PL 方法论关联。引用 24 inbox
Sungjae Hwang, Sungho Lee, Jihoon Kim, Sukyoung Ryu
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:提出 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 规范应明确缺失语义,调试特性应完整支持。

问题
JNI 程序因跨语言互操作语义复杂而难以保证正确,而 JVM 默认不检查错误的 JNI 互操作,仅靠 -Xcheck:jni 调试选项验证;该选项对规范未指定情形的检查质量与影响尚不清楚。
方法
提出 JUSTGen,用 DSL 表达 JNI 规范,通过 SMT 求解器自动发现未指定情形并生成触发测试,以系统评估 JVM 的 JNI 调试检查能力。
评估
在主流 JVM 上运行生成的测试,发现数千个未指定情形未被验证且可引发类型系统违反、内存破坏等严重错误;向厂商报告 792 个案例,563 个已修复。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · DBLP

BibTeX
@inproceedings{HwangLKR21,
  title = {JUSTGen: Effective Test Generation for Unspecified JNI Behaviors on JVMs},
  author = {Sungjae Hwang and Sungho Lee and Jihoon Kim and Sukyoung Ryu},
  booktitle = {ICSE},
  year = {2021},
  doi = {10.1109/icse43902.2021.00151}
}