Hwang S , Lee S , Kim J , et al. JUSTGen: Effective Test Generation for Unspecified JNI Behaviors on JVMs[C]// 2021 IEEE/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). ACM, 2021.

1. 摘要

Java 原生接口(JNI)为 Java 应用程序提供了一种访问原生库的方法，但是很难开发出正确的 JNI 程序。此外，核心 Java 库已经使用 JNI 来提供像图形用户界面这样的系统特性。因此，许多主流的 Java 虚拟机都支持 JNI。由于性能开销，JVM 默认情况下不会验证错误的 JNI 互操作，但只有在启用调试功能-xccheck:JNI 选项时才会验证它们。因此，JNI 程序的正确性高度依赖于 JVM 的-xccheck:JNI 选项的检查。然而，该功能提供的检查质量仍然存在问题。

在本文中，我们使用 JNI 规范中未指定的边角案例， 实证研究 了-Xcheck:JNI 选项对主流 JVM 的验证质量和影响。我们的实验结果表明，JNI 调试特性会导致严重的运行时错误，例如违反 Java 类型系统和内存损坏。我们向相应的 JVM 供应商报告了 792 个未经 JVM 验证的未指定案例。我们认为 JNI 规范应该明确规定缺失案例的语义，并且应该完全支持调试特性。

关键字：Java 本地接口，Java 虚拟机，测试，实证研究，调试

1. 介绍

JNI 接口定义了 Java 代码和用 C 或 C++编写的本机代码之间的互操作。使用 JNI，开发人员可以通过在本机代码中实现性能关键模块，并通过 JNI 将它们与 Java 模块组合成一个单独的程序，从而提高程序的性能。 此外，没有任何公开可用的工具可以检测到这样的互操作错误。

JNI 不检查编程错误，原因如下：

（1）强制 JNI 函数检查所有可能的错误条件会降低正常(正确)本机方法的性能

（2）在许多情况下，没有足够的运行时类型信息来执行这种检查。

JNI 支持-Xcheck:-Xcheck:JNI 选项是一个命令行选项，它使虚拟机对传递给 JNI 函数的参数进行额外的验证。我们的研究有两个技术挑战:

（1）如何识别 JNI 规范中未指明的情况

（2）如何生成触发未指定案例行为的测试程序

本文的贡献包括：

1. 提出了一种从规范中识别未指定案例的方法，并实现了 JUSTGEN，该 JUSTGEN 从机械化的规范中自动识别它们，并生成激发它们的测试代码。

2. 从 JNI 规范中确定了未指明的情况。

3. 这是第一个在五个主流 JVM 上分析-Xcheck:JNI 选项质量的工作。

图 1. 正常和未指定行为的 JNI 代码示例

2. 背景和示例

2.1 JNI 互操作

JNI 是一个外部函数接口，支持 Java 和本地应用程序之间的双向互操作。图 1(a)显示了带有 JNI 程序入口点的 Java 代码，图 1(b)显示了编译到本机库 Hello.so 的 C 代码。在第 2 行执行 System.loadLibrary 方法时，本机方法与一个 C 函数 Java_HelloJNI_foo 相链接。当程序运行时，主方法在第 5 行调用本机方法 foo。然后，JVM 将程序控制转移到链接的 C 函数 Java_HelloJNI_foo 的入口。在 C 代码中，函数 Java_HelloJNI_foo 通过一系列三个 JNI 函数调用来调用 Java 方法名。在图 1(b)的第 6 行，C 代码通过调用第 1 行定义的 get_name_id 来获得一个 Java 方法 ID。该函数调用 GetObject Class JNI 函数，该函数接受一个 JNIEnv 指针和一个 Java 对象，并返回该 Java 对象的类信息。然后，它调用 GetMethodID，使用类信息、方法名和方法签名获得一个 Java 方法 ID。使用方法标识和 Java 对象，它通过 CallObjectMethod JNI 函数调用 Java 方法名。

2.2 未指明的情况和 JNI 调试功能

由于 JVM 的性能开销，它不会在运行时验证参数值，因此未指定的情况可能会导致意外的行为，甚至是安全漏洞。图 1(c)显示了 JNI 函数 CallObjectMethod 的一种未指明的情况。函数 Java_HelloJNI_foo 通过 get_name_id 函数获取 Java 方法名的 ID。但是，在第 4 行，它试图使用在第 3 行创建的 Java 字符数组对象来调用 Java 方法名，而不是从 Java 传播的 Java 对象。JNI 规范对 CallObjectMethod 的行为描述如下：

NativeType CallMethod(JNIEnv*env,jobject obj,jmethodID methodID,…);

在示例中，由于方法 ID 是从 HelloJNI 派生的，而这种类型的类是 字符数组 ，因此没有指定其行为，这可能会在主流 JVM 上造成问题。

当在启用了-xccheck:JNI 选项的 OpenJ9 JVM 上执行图 1(c)中的示例时，JVM 会检测到无效的参数，并抛出一个异常显示错误消息:

JNI error in CallObjectMethod/CallObjectMethodV: Ineligible receiver.

然而，由于可调试性高度依赖于 JVM，JNI 程序中的无效互操作在调试过程之后可能仍然没有被发现，这降低了 JNI 程序的质量。

3. 方法

3.1 概述

为了评估-Xcheck:JNI 选项的质量，我们使用从 JNI 规范中半自动提取的未指定情况来测试 JVM。图 2 展示了由两个阶段组成的测试方法的概述。

在 JNI 代码生成阶段，JUSTGEN 从 JNI 规范中提取未指定的案例，并生成激发未指定案例行为的测试程序。第一步是定义一种领域特定语言(DSL)，并手动将规范中的语义转换为 DSL 中的机械化规范。然后提取器通过使用 SMT 求解器从机械化规范中发现未指定的情况。提取器通过添加已识别的未指定案例来更新规范，并重复上述过程，直到公式变得不可满足。对于每个未指定的情况，测试代码生成器会自动生成一系列有效的 JNI 函数调用，触发未指定情况的行为。然后，它用我们定义的 Java 和 C 模板代码组成 JNI 函数调用。

在 JVM 测试阶段，我们在启用了-Xcheck:JNI 选项的主流 JVM 上执行生成的测试程序。手动检查测试结果并分析每个 JVM 的调试功能的能力，并识别由于缺乏来自 JVM 的验证而导致的潜在危险。

3.2 领域特定语言的 JNI 规范

为了自动处理 JNI 规范，我们定义了一个简单的 DSL 来描述 JNI 函数的行为。手动将它们转换为 DSL 中表达的机械化规范。

图 3 展示了 DSL 语法。规范 s 是一系列类型声明 typedef t、一系列细化谓词声明 refinedef t@p 和一系列 JNI 函数规范 d。类型 t 表示 C 编程语言中的类型，包括原语类型和 JNI.h 中 JNI 的预定义类型。

细化谓词 p 表示谓词名称，它返回输入是否满足其条件。细化类型 t@p 表示一组具有类型 t 并满足细化谓词 p 的值。JNI 函数规范 d 由一个 JNI 函数描述符和一系列精细函数描述符组成。一个 JNI 函数描述符类型 t F(t)表示一个返回类型 t，一个 JNI 函数名 F，以及一系列参数类型 t。F(t[@r]？)表示可选的优化返回类型 t[@r]？，一个 JNI 函数名 F，以及一系列可选的优化参数类型 t[@r]？其中 κ 是规格值或未用值。精炼 r 是精炼谓词 p 或它的连词。我们定义了 38 种类型和 105 种细化类型。为了区分函数描述符，JVM 不验证 JNI 函数的返回值。在规范中指定的以及在使用 SMT 求解器查找未指定情况时构建的那些，我们对前者使用规范，对后者使用 unspec。

图 4 显示了 DSL 中的 JNI 函数规范示例。JNI 函数 SetIntArrayRegion 接受一个 JNI 环境指针 JNIEnv，一个 Java 整数数组 jintArray，一个代表数组 jsize 起始索引的整数值，一个指示要复制的 jsize 元素数量的整数值，以及源缓冲区(jint)，将 指定数量的元素从源缓冲区复制到 Java 数组。我们将 DSL 中的上述规范转换为 spec 语句。

图 2. 未指定情况下 JVM 测试的整体结构

图 3. 定义 JNI 语义的领域特定语言

图 4. DSL 中的 JNI 函数规范示例

3.3 使用表面贴装求解器查找未指定的行为

我们利用 Z3 SMT 求解器 4.8.1 版本从机械化 JNI 规范中自动查找未指定的情况。为了使用 SMT 求解器，我们将未指定的案例发现问题转换为 SAT 问题。

1）JNI 函数规范的位向量表示：

我们使用位向量来表示布尔公式中的每个 JNI 函数规范，以便 SMT 求解器可以对其进行操作。JNI 函数规范由一个可能细化的返回类型、一个函数名和一个可能细化的参数类型列表组成。将 JNI 函数规范编码到一个位向量列表中，其中每个位向量代表每个可能细化的参数类型。

定义 1(位向量表示):

（1）（类型）每个类型 t 被映射到唯一的比特向量表示 Bt。

（2）(细化谓词)对于每个细化类型 t@r，r 中的每个细化谓词 p 都映射到一个唯一的位向量 Bp，该位向量的 on 位不与表示 t 的细化谓词的其他位向量重叠。

（3）(精化)对于一个精化 r = p1∧…∧pn，它的位向量表示为 Br = Bp1|Bpn （|是按位 or 运算符）。

（4）(JNI 函数规范)对于 JNI 函数规范 t1@r1F(t2@r2，…，tn@rn)，其位向量表示为((Bt2，Br2)，…，(Btn，Brn))其中 Bti 和 Bri 分别是 ti 和 ri 的位向量表示。

位向量表示的一个挑战是定义类型之间的子类型关系。虽然 C 在类型之间没有任何子类型关系，但 JNI 引用类型有一个对应于 Java 类型层次结构的类型层次结构。我们使用按位“与”运算符&定义了两个位向量之间的子类型关系(<:t)。

定义 2(子类型关系):

假设 t1 是 t2 的子类型，Bt1 和 Bt2 分别是 t1 和 t2 的位向量表示。那么，子类型关系 Bt1<:tBt2 有效。子类型关系相当于一个布尔表达式，Bt1&Bt2=Bt2

定义 3(子限关系):

假设 r1 是 r2 的子限，Br1 和 Br2 分别是 r1 和 r2 的位向量表示。那么，子约束关系 Br1 <:rBr2 有效。子约束关系相当于一个布尔表达式，Br1&Br2= Br2。

2）未指定案例发现的可满足性:

使用编码的 JNI 函数规范，将每个 JNI 函数规范转换为一个布尔公式来查找未指定的情况。一个复杂性是大多数 JNI 函数采用多个参数，所以我们应该考虑许多参数组合。为了实用，单独处理每个参数，以减少搜索空间。对于一个有 n 个参数的 JNI 函数 F，我们让 n 个函数 F1，Fn，其中 Fi 只取 F 的第 i 个参数，然后，每个函数 Fi 转换成一个布尔公式，SMT 求解器独立地为每个 布尔 公式找到未指定的情况。

在定义了四个辅助定义之后，我们定义了一个布尔公式来使用辅助定义检查 JNI 函数参数的可满足性。

定义 4(完全求精):

对于每一个类型 t，它的完全求精位向量是 ，它是 t 的所有求精谓词的合取

定义 5(细化类型的有效性):

如果 Btx<:tBt 和 Brx<:r Bc^t ，则细化类型(Btx，Brx)的位向量表示对 t 类型有效。只有当(Btx，Brx)对 t 类型有效时，逻辑谓词有效((Btx，Brx)，t)才为真。

定义 6(等价类型可满足性)：

细化类型(Btx，Brx)的位向量表示是可满足另一位向量表示(Bty，Bry)的等价类型，如果 Btx=Bty 以及 Brx<:rBry。逻辑谓词 sateq((Btx，Brx)，(Bty，Bry))只有在(Btx，Brx)与(Bty，Bry)等价类型可满足时才为真。

定义 7(子类型可满足性):

细化类型(Btx，Brx)的位向量表示可满足另一个位向量表示(Bty，Bry)的子类型，如果 Btx <:TbTy 和 Btx6= Bty。逻辑谓词 satsub((Btx，Brx)，(Bty，Bry))只有在(Btx，Brx)子类型可满足(Bty，Bry)时才为真。

使用辅助定义，我们定义了一个由 SMT 求解器求解的参数可满足性的布尔公式。假设 JNI 函数声明是 t1F(t2)，其规范的位向量表示是(Bty，Bry)。将它的可满足性问题定义如下:

记录未指定的情况，并通过如下添加来更新公式:

因此，在下一次迭代中，除了之前发现的情况之外，SMT 求解器试图找到另一个未指定的情况。当 SMT 求解器未能找到更多未指定的情况时，它会得出公式不可满足的结论，意味着更新后的规范涵盖了所有有效参数。

3.4 JVM 上的测试用例生成和测试

测试代码生成器利用“JNI 函数映射表”和“模板代码”来生成有效的测试代码。首先，它通过将 JNI 函数的每个细化参数类型与其他 JNI 函数的细化返回类型进行匹配来构建映射表。有了映射表和模板代码，测试代码生成器通过构建有效的 JNI 函数调用链和传播精确参数类型的有效参数，为未指定的情况生成有效的 C 测试代码。我们编译生成的 C 测试代码，并将其与我们开发的 Java 模块相链接，以构建可执行的 JNI 测试程序。

为了在多个 JVM 上进行测试，我们将每个 JVM 安装在一个独立的 Docker 容器上，并在每个容器上执行生成的测试代码。然后，测试结果 汇编器 将执行结果分为四类:错误、分段错误、异常和验证。SegFault 和 Exception 类别分别表示测试代码导致分段错误和引发异常，Validation 类别表示测试代码以调试功能产生的错误或警告作为其验证结果而终止。测试结果汇编器比较 JVM 的执行结果，以识别 JVM 的不同调试能力。

表 1. 对 34990 个的评估结果

4. JVMS JNI 调试功能的评估

4.1 未指明情况的评估结果

选择了五个 JVM:Oracle 的 Hotspot、 IBM 的 OpenJ9、Azul 的 Zulu、 Amazon 的 Corretto 和 Oracle 的 GraalVM。Java 版本选择了 Java 11。

如表 1 所示，除了 OpenJ9 之外，JVM 之间的评估结果非常相似，因为它们是 OpenJDK 的变体。OpenJ9 验证的未指明案例比其他案例多得多，但它只验证了 30.3%的未指明案例。其他 JVM 仅验证了 13.4%。

4.2 类别:行为不端

我们手动调查了行为不当类别中未指明的案例。对于为不同类型提供相同功能的 JNI 函数族，我们随机选择了其中一个。最后，我们为 Hotspot、Zulu、Correctto 和 GraalVM 手动调查了 132 个未指定的案例，但只为 OpenJ9 调查了 17 个案例，因为它有少量的行为不端案例。

1）在所有 JVM 中:

我们发现了两个案例，在这两个案例中，所有五个 JVM 都无法识别未指定的案例。

发现 1：使用 JNI 函数的返回值进行错误处理是不可靠的。

发现 2：删除的引用未被完全验证

2）在四个 JVM 中:我们报告了六种情况，其中除了 OpenJ9 之外的所有 JVM 都无法识别未指定的情况。

发现 3：方法可以被视为构造函数。

发现 4：Java 对象可能未正确初始化。

发现 5：本机代码可能会调用带有错误类型的 Java 对象的 Java 方法。

发现 6：数组元素可以用不兼容类型的值更新。

发现 7：JNI 函数可能会改变 Java 方法的返回值。

发现 8：即使堆栈上不存在本地参考帧，也可以从本地参考帧中弹出对象。

3）仅在 OpenJ9 中:

我们发现了四个只有 OpenJ9 未能识别未指明病例的病例。我们把它们都报告给了 IBM，它们都是固定的。

发现 9：无效的 Java 对象可以用不正确的类名来构造，并且它们会导致后续 JNI 函数调用中的分段错误。

发现 10：可以用负容量创建本地引用。

发现 11：无效的 JNI 函数调用可能会被忽略。

发现 12：JNI 计划不得终止。

4.3 类别:SegFault

除了到目前为止描述的异常行为之外，我们还观察到，由于缺少-Xcheck:JNI 选项的验证，未指定的情况可能会导致分段错误。

如表所示，OpenJ9 中有 567 个未指定的案例引发了分段错误，GraaalVM 中有 1011 个案例，其他 JVM 中有 1051 个案例。对其进行了手动调查，以了解哪些属性未经验证，表二总结了结果。

将分段错误分为四个原因:类型检查、空检查、活性检查和可发布性检查。对于 OpenJ9，缺少 NULL Check 是主要原因，有 74.5%的分段错误。对于其他 JVM，分段错误的主要原因是缺少类型检查；HotSpot、Zulu 和 Corretto 上 76.1%的分段错误和 GraalVM 上 75.2%的分段错误是由于缺少类型检查造成的。OpenJ9 上分段错误的第二个主要原因是缺少活跃度检查。此外，我们还观察到了不可释放数组被 JNI 函数(如 ReleaseCharArrayElements)释放的未指定情况。我们发现这些未指定的情况只有 OpenJ9 才能检测到，其他 JVM 抛出了分段错误。

我们发现的另一个有趣的点是 HotSpot、Zulu 和 Corretto 具有相同数量的分割错误。对这些案例的分析得出结论，这些 JVM 的-Xcheck:JNI 选项验证了相同的属性。另一方面，OpenJ9 的行为与其他 JVM 大不相同。OpenJ9 上的-Xcheck:JNI 选项比其他 JVM 验证了更多的属性。

4.4 JVM 之间的差异

评估结果显示，有 6499 个未指定的案例被 OpenJ9 正确验证，但是 HotSpot 没有通过。相反，HotSpot 验证了 578 个未指定的案例，但是 OpenJ9 没有通过。分析结果总结在表三中，其中 O 表示 JVM 的-Xcheck:JNI 选项正确验证了未指定的案例，X 表示 JVM 没有验证未指定的案例。它显示了三个新的原因:修饰符、负整数和构造函数。修饰符原因表示 JVM 没有检查修饰符的正确使用。OpenJ9 不能验证它们，而 Hotspot 可以。其余结果在表中可找对对应信息。

表 2. 分段故障的根本原因

表 3. Hotspot 和 OpenJ9 的调试能力

表 4. JVM 未验证的未指定案例

我们的评估结果显示，不同 JVM 的调试特性检查不同的属性，因此在多个 JVM 上验证 JNI 程序，特别是 OpenJ9 和其他之一将是可取的。

4.5 没有来自任何 JVM 的验证

我们观察到，23880 个未指明的案例没有得到任何 JVM 的验证。其中，所有 JVM 为 23367 个案例抛出异常，但没有 JVM 为其余 513 个案例抛出异常。

如表中所示，其根本原因有三类。

（1）类别缺少空检查。

（2）缺少尺寸检查

（3）类型检查。

4.6 有效性威胁

我们采用了一种系统化和自动化的方法来从 JNI 规范中找到未指明的案例。发现未指明情况的唯一手动部分是将 JNI 规范转换为我们的 DSL。手动转换可能包含导致不正确转换的人为错误。此外，我们手动调查了由 JUSTGEN 自动生成的结果。人工调查证实结果是准确的，这表明 JNI 规范得到了正确的转换。手动评估的结果是值得信赖的，因为外部评审者也验证了这些结果。请注意，JUSTGEN 并不证明-Xcheck:JNI 实现的正确性，而是测试它们，这可能会导致误报和漏报。

5. 结论

在本文中，我们提出了一种半自动的方法来评估-Xcheck:JNI 选项在各种 JVM 上的验证能力和影响。从 JNI 规范中，我们手动将 JNI 函数的核心功能翻译成我们的 DSL，JUSTGEN 自动发现未指定的案例，并生成执行这些案例的测试代码。然后，我们在五个主流 JVM 上执行测试代码，并对执行结果进行分类，以评估它们的验证能力。在经验评估中，JUSTGEN 发现了 34990 个 JNI 规范没有涵盖的未指明的案例。我们发现 5972 个未指明的案例无法通过 Hotspot 的调试功能进行验证，5968 个由 Zulu 和 Corretto 验证，5928 个由 GraalVM 验证，1012 个由 OpenJ9 验证。我们向相应的 JVM 供应商报告了调试特性的验证问题，有 792 个未指定的案例，其中 563 个案例已经修复，其余的计划修复。

致谢

本文由 南京大学软件学院 2021 级硕士冯翔翻译转述