标题： DALEQ -- Java字节码的可解释等价性 显示英文标题

标题： DALEQ -- Explainable Equivalence for Java Bytecode

摘要： 软件构建的安全性近年来引起了越来越多的关注，这是对SolarWinds和xz等事件的回应。 现在，包括Oracle和Google在内的几家公司在安全环境中重新构建开源项目，并通过专用存储库发布生成的二进制文件。 这种做法使得这些重新构建的二进制文件可以与开发者在Maven Central等存储库中发布的原始二进制文件进行直接比较。 这些二进制文件通常不是按位完全相同的；然而，在大多数情况下，差异可以归因于构建环境的变化，这些二进制文件仍然可以被认为是等价的。 然而，建立这种等价性是一个劳动密集且容易出错的过程。 虽然有一些工具可用于此目的，但它们都无法提供来源信息，即为什么两个二进制文件是等价的或不等价的可读解释。 为了解决这个问题，我们提出了daleq，这是一个将Java字节码反汇编到关系数据库中的工具，并可以通过应用Datalog规则对这个数据库进行规范化。 然后可以使用这些数据库来推断两个类之间的等价性。 值得注意的是，等价性陈述会附带记录规范化过程的Datalog证明。 我们通过一项涉及2,714对JAR文件（包含265,690对类）的大规模评估，在工业环境中展示了daleq的影响。 在这项评估中，daleq与两种现有的字节码转换工具进行了比较。 我们的研究结果表明，评估非按位等价的工件所需的手动工作量显著减少，否则这些工件需要大量的人工检查。 此外，结果表明，daleq在识别从同一代码重新构建的更多等价工件方面优于现有工具，即使没有行为上的差异。 显示英文摘要

摘要： The security of software builds has attracted increased attention in recent years in response to incidents like solarwinds and xz. Now, several companies including Oracle and Google rebuild open source projects in a secure environment and publish the resulting binaries through dedicated repositories. This practice enables direct comparison between these rebuilt binaries and the original ones produced by developers and published in repositories such as Maven Central. These binaries are often not bitwise identical; however, in most cases, the differences can be attributed to variations in the build environment, and the binaries can still be considered equivalent. Establishing such equivalence, however, is a labor-intensive and error-prone process. While there are some tools that can be used for this purpose, they all fall short of providing provenance, i.e. readable explanation of why two binaries are equivalent, or not. To address this issue, we present daleq, a tool that disassembles Java byte code into a relational database, and can normalise this database by applying datalog rules. Those databases can then be used to infer equivalence between two classes. Notably, equivalence statements are accompanied with datalog proofs recording the normalisation process. We demonstrate the impact of daleq in an industrial context through a large-scale evaluation involving 2,714 pairs of jars, comprising 265,690 class pairs. In this evaluation, daleq is compared to two existing bytecode transformation tools. Our findings reveal a significant reduction in the manual effort required to assess non-bitwise equivalent artifacts, which would otherwise demand intensive human inspection. Furthermore, the results show that daleq outperforms existing tools by identifying more artifacts rebuilt from the same code as equivalent, even when no behavioral differences are present.