DALEQ -- Java 字节码的可解释等价性

近年来，软件构建的安全性引起了广泛关注，这与 solarwinds 和 xz 等事件有关。目前，Oracle、Google 等多家公司会在安全环境中重新构建开源项目，并通过专门的仓库发布生成的二进制文件。这一做法使我们能够直接比较这些重建的二进制文件与开发人员在诸如 Maven Central 等仓库中发布的原始二进制文件。虽然这些二进制文件通常不完全相同，但在大多数情况下，差异可归因于构建环境的差异，二进制文件仍可视为等价。然而，建立此类等效性是一个费力且容易出错的过程。虽然已有一些工具可用于此目的，但它们都未能提供源信息，即解释两个二进制文件为何等价或不等价。为此，我们提出了 daleq，这是一个将 Java 字节码解码为关系数据库的工具，并可通过应用 datalog 规则对该数据库进行标准化。随后可用于推断两个类的等效性。值得注意的是，等效陈述伴随 datalog 证明，记录标准化过程。我们通过涉及 2,714 对 jar 包、 comprising 265,690 对 class 类的大规模评估展示了 daleq 的实际应用价值。在该评估中，daleq 被用于与两种现有字节码转换工具进行比较。我们的发现表明，daleq 在评估非按位相同制品时显著减少了需要人工检查的工作量。此外，结果显示 daleq 通过识别更多从同一代码重建的制品等价，即使不存在行为差异，也优于现有工具。