droidsaw/droidsaw-dex

# droidsaw-dex DEX (Dalvik Executable) 字节码解析器和反编译器。解析 `classes*.dex` 字节，构建 CFG，通过 Braun 算法构建 SSA，结构化区域，并生成 Java 源代码。逆向路径 `emit_dex` 将解析后的 `DexFile` 重新序列化为 DEX 字节；在 IR 层级满足 `parse ∘ emit_dex ∘ parse ≡ parse`。 位于工作区中 `droidsaw` 二进制文件的下层。依赖于 `droidsaw-common` 提供的通用图 / SSA / 区域 / 支配节点算法（该捆绑包对 `I: Instr` 进行了泛型抽象）；DEX 操作码表、`Opcode` 枚举（在 `src/opcodes.rs` 中有 224 个变体）以及 DEX 格式细节保留在此处。没有特定于格式的内容泄漏到 `droidsaw-common` 中。 ## 架构 DEX 和 Hermes 共享相同的反编译 pipeline。中间阶段在 `droidsaw-common` 中是通用的；此 crate 提供其自身的 `Insn` 类型和 DEX 特定的语法糖。 | 阶段 | 模块 | 输入 → 输出 | |---|---|---| | parse | `src/parser/mod.rs`, `src/header.rs`, `src/annotation.rs`, `src/access_flags.rs`, `src/ids.rs` | `&[u8]` → `DexFile` | | decode | `src/decode.rs`, `src/opcodes.rs` | code-item 字节 → `Vec` | | CFG | `src/cfg.rs` | `Vec` → 基本块 + 类型化边 | | dominators | `droidsaw-common::graph::dominators` | 基本块 → idom 映射 | | SSA (Braun) | `src/ssa.rs`, `droidsaw-common::ssa` | 基本块 → `SsaBody` | | types | `src/types.rs` | `DexType` 格栅；`Bottom` → 原语 / 引用 → `Top` | | optimize | `src/optimize.rs` | 拷贝传播，常量折叠（DEX 语义），DCE | | structure | `src/structure.rs`, `droidsaw-common::region` | CFG → `RegionTree` (`if`/`else`, `while`, `for`, `try`/`catch`, `switch`) | | sugar | `src/sugar.rs` | enhanced-for 恢复，短路 `||` / `&&` 重构 | | emit (Java) | `src/emit.rs`, `src/classes.rs` | `RegionTree` → Java 源代码 | | emit (DEX) | `src/emit_dex.rs` | `DexFile` → DEX 字节 | | validate | `tests/byte_identity_smoke.rs`, `tests/roundtrip_proptest.rs` | 源字节 / IR ≡ 输入 | 异常边是类型化的（`EdgeKind::ExceptionHandler(TypeIdx)` 和 `EdgeKind::ExceptionCatchAll`），并在 `exception_regions` 中单独跟踪，以便下游 pass 能够区分异常流和普通控制流。 `emit_dex` 中规范的 id-pool 排序通过 `NonDecreasing` 和 `StrictlyAscending` newtype 在结构上进行编码 —— emit 代码只能通过 `from_sorted` / `from_verified` 获取它们，因此规范对 `string_ids` / `type_ids` / `proto_ids` / `field_ids` / `method_ids` 的字典序排序要求是一个类型系统定理，而不是测试结果。不对称性 **emit 域 ⊊ parse 域** 是有意为之：parse 容忍异常以便在对抗性输入上进行分析；emit 则拒绝它们，因此任何格式错误的形状都无法进行后续的往返。 交叉引用 (`src/xrefs.rs`) 以稳定的描述符三元组（class, name, proto）为键，而不是基于每个 DEX pool 的索引，因此 `Xrefs::merge` 在 multidex APK 之间具有良好的定义。签名和保护器识别器 (`src/signatures/`) 包括 `javac21`、`kotlinc19` 和两种保护器形状 (`fragmented_string_literal`、`reflective_invoke_stub`)。 确定性 IR。仅使用 `BTreeMap`，不使用 `HashMap`。类型化的 `Opcode` 枚举（224 个变体，AOSP `bytecode.txt` v035–v041）。结构化的 try-catch（先分区后递归）。语法糖与核心结构化分离。 ## 输入 `classes*.dex` 内容的 `&[u8]`。Multi-dex APK 为每个 `classes.dex` 生成一个 `DexFile`；由 `droidsaw-apk` 提取。Header 和 id pool 在解析时进行验证；类数据、code item 和字符串 pool 按需解码。 `DexFile` 是一个借用调用者拥有的字节切片的零拷贝视图。字符串编码为 MUTF-8；编解码器位于 `src/mutf8.rs` 中，调用者绝不能绕过它。 ## 输出 - `DexFile` IR (`src/parser/mod.rs`) —— 类、方法、code item、调试信息、注解、调用点、方法句柄。 - `classes::decompile_class` —— 单个类的 Java 源代码。 - `smali::*` —— Smali 反汇编 (`src/smali.rs`)。 - `emit_dex::emit_dex` —— 解析后的 `DexFile` 对应的 DEX 字节 (`src/emit_dex.rs`)。 ## 正确性 五个关卡。每个关卡负责捕获其上一层遗漏的内容。 ### 1. 往返反汇编 `emit_dex` 是 `DexFile::parse` 的逆操作。等价性规范 *就是* 往返契约： ``` parse ∘ emit_dex ∘ parse ≡ parse ``` `src/parser/content_equiv.rs` 中的 `ContentEquiv` 是等价关系：pool 的大小和内容必须匹配；依赖于布局的字段（分节偏移量、header 校验和 / 签名、作为原始文件偏移量的 BTreeMap 键）被排除在外 —— 这些是确定性 emit 的结果，而不是 IR 内容。 在 `tests/roundtrip_proptest.rs` 中默认进行 256 个用例的 Proptest (`parse_emit_parse_structural_equivalence`)。`ContentEquiv` 上的商定律 —— 自反性、对称性、传递性 —— 在 `tests/quotient_laws_proptest.rs` 中进行了独立的 Proptest，因此该关系是真正的等价关系，而不是有泄漏的 `PartialEq`。 字节一致性是在 `tests/byte_identity_smoke.rs` 处测量的更严格关卡：字节完全相同的输出 ⇒ 空的 `applied_transformations`（归因契约 —— emit 绝对不能报告它实际上没有执行的转换）。在 F-Droid 语料库上测量 (`tests/corpus_byte_identity_fdroid_sweep.rs`)：**在 preservation 模式下，5767 个 DEX 文件中的 5767 个实现了 100% 字节相同的往返** (2026-05-23)。309 个文件 (5.4%) 仅在 24 个 header 字节上存在差异 —— 全部是旧版 `dx` 工具链的非规范 SHA-1 输入，通过 `CanonicalTransform::InputChecksumNormalized` 进行类型归因。 在本地验证： ``` cargo test -p droidsaw-dex --test roundtrip_proptest cargo test -p droidsaw-dex --test quotient_laws_proptest cargo test -p droidsaw-dex --test byte_identity_smoke -- --nocapture ``` ### 2. Fixture 棘轮 `tests/fixtures/java/` 中有 40 个 fixture，由 `tests/fixtures/manifest.toml` 驱动并由 `tests/fixture_ratchet.rs` 运行。每个 fixture 的完整 pipeline 是 `javac → d8 → decompile → javac → java`。带有 `expected_stdout` 条目的 fixture 将重新编译运行的 stdout 与该黄金文件进行比较；没有该条目的 fixture 使用原始 `java` 运行的输出作为黄金标准。 当前状态：39 个 `compile_pass`，1 个 `compile_fail`，0 个 `semantic_fail`。 Fixture 状态是一个棘轮。`semantic_fail` 保持为 0。`compile_fail` 单调递减。`compile_pass → compile_fail` 的翻转将阻止合并。 `UNRECOGNIZED_REGION` 棘轮在 `tests/unrecognized_ratchet.rs` 中是按 APK 划分的，每个文件的 SHA-256 基准位于 `tests/baselines/unrecognized.toml` 中。按 APK 单调（而非全局）：每个 APK 都根据其自身的基准进行门控；轮换的 APK 会显式报错失败，而不是静默地重新设定基准。 ### 3. 对抗性模糊测试 `fuzz/fuzz_targets/` 中的 libFuzzer target： | Target | 不变量 | |---|---| | `fuzz_parser` | `DexFile::parse(bytes)` 永远不会 panic。 | | `fuzz_opcode_decode` | `decode::decode_insns` 永远不会 panic。 | | `fuzz_cfg` | `Cfg::build` 在任何被解析器接受的 code item 上永远不会 panic。 | | `fuzz_ssa` | `SsaBody::build` 在任何被解析器接受的 body 上永远不会 panic。 | | `fuzz_emit_roundtrip` | `parse(emit_dex(parse(bytes)))` 成功，并且在每个接受的输入上对于首次解析的结果满足 `ContentEquiv`。 | | `fuzz_enum_cross_class` | 跨类枚举识别器不 panic。 | | `fuzz_protector_recognizer` | 保护器形状签名在对抗性输入上不 panic。 | | `fuzz_emulator` | 有界符号模拟器不 panic。 | | `fuzz_decode_debug_info` | `decode_debug_info` 在对抗性输入上永远不会 panic。 | | `fuzz_diag_collectors` | 诊断收集器在解析错误时不 panic。 | | `fuzz_proguard_mapping` | ProGuard 映射解析器在畸形输入上不 panic。 | | `parser_differential` | 在两者都接受的输入上满足 `naive_parse_dex(data).to_shape() == DexFile::parse(data).to_shape()`。用于检测静默错误解析 bug 的分层预言机。 | | `cfg_differential` | `naive_cfg(code).shape() == Cfg::build(code).to_shape()`。用于检测静默错误 CFG bug（这类 bug 会在不引发 panic 的情况下破坏 dominators）的分层预言机。 | 跟踪到的崩溃复现用例位于 `fuzz/crashes//` 下；精心挑选的种子位于 `fuzz/seeds//` 下。运行一个 target： ``` cd droidsaw-dex RUSTUP_TOOLCHAIN=nightly-2025-11-21 cargo fuzz run fuzz_parser RUSTUP_TOOLCHAIN=nightly-2025-11-21 cargo fuzz run fuzz_emit_roundtrip ``` `tests/fixtures/adversarial/` 下的对抗性 fixture（操作码不变量、OOM、header/map 不一致、try-item 范围、字符串长度不一致）既可作为 fuzz 种子，也可作为 `tests/opcode_invariant_fixtures.rs` 中的确定性回归测试。 ### 4. 跨工具差分 `dexdump` (Android SDK build-tools) 是一个 DEX 反汇编器，在此处用作代码单元覆盖率预言机。检查的目的不是比较反汇编或反编译的 Java 输出 —— 而是关于 droidsaw-dex 是否能看到反汇编器看到的每一个类和方法。差分测试从 `droidsaw-bench` 运行 (`src/dexdump_runner.rs` + `src/cross_tool.rs`)：`dexdump -d` 枚举的每一个类描述符和每一个方法 `(class, name, proto)` 三元组也必须出现在 droidsaw-dex 输出中。遗漏类或方法会导致构建中断。 ### 5. 形式化证明 `proofs/` 下有九个 Kani harness 文件，总计 40 个 `#[kani::proof]` 属性： | 文件 | 主题 | 子证明 | |---|---|---| | `proofs/header_size_gauge.rs` | `DexHeader::parse` 拒绝 `header_size != 0x70` | 2 | | `proofs/access_flags_spec_union.rs` | `access_flags::validate` 拒绝掩码外的位（3 个作用域 × 6 个用例） | 6 | | `proofs/debug_register_bound.rs` | `narrow_register` 阻止了 `register as u16` 截断走私路径 | 4 | | `proofs/class_def_off_bound.rs` | 4 个 `class_def` 偏移字段在解析时进行边界检查，而不是在首次读取时 | 4 | | `proofs/encoded_value_value_arg_bound.rs` | `annotation::check_value_arg_size` 阻止了破坏往返字节相等性的 11 个窄转换分支 | 12 | | `proofs/annotation_directory_cap.rs` | `AnnotationDirectoryItem::parse` 在总和 `fields + methods + parameters` 上限制了 `Vec::with_capacity` | 3 | | `proofs/endian_tag_gauge.rs` | Endian-tag 编解码器往返正确性 | 3 | | `proofs/sign_extend_4bit.rs` | 4 位寄存器宽度的符号扩展 | 2 | | `proofs/try_item_start.rs` | 在 `insn_count == 0` 时触发 `EmptyTryRegion` 违规（审计欺骗回归） | 2 | 运行一个 harness： ``` cd droidsaw-dex cargo kani --harness non_canonical_header_size_always_rejected ``` 每个证明都锚定了一个具体的过去回归 —— 每一个都是针对某类 bug 的规范化标尺，而不是同义反复。一旦定理的陈述符合 Kani 的有界可达性要求，它们就会从 Lean 迁移到 Kani；更广泛的 Lean 覆盖范围（dominators、post-dominators、lattice 单调性、路径属性）位于工作区的 `droidsaw-lean` crate 中。 每个非测试模块的编译时下限： ``` #![forbid(unsafe_code)] #![deny(clippy::unwrap_used, clippy::expect_used, clippy::panic, clippy::unreachable, clippy::todo, clippy::arithmetic_side_effects, clippy::indexing_slicing, clippy::string_slice, clippy::cast_lossless, clippy::cast_possible_truncation, clippy::cast_sign_loss, clippy::cast_precision_loss, clippy::cast_possible_wrap, clippy::as_conversions)] ``` `clippy::as_conversions` 在 crate 根目录被拒绝；非测试代码中新的 `as` 转换必须带有针对特定位置或文件级别的 `PROOF: ...` allow。 ## 性能 `src/optimize.rs` 使用 `FxHashMap` 存储每个 pass 的函数内映射。`VarId` 是 `Copy + Eq + Hash`，在优化器内部顺序不是承重元素（最终 emit 会在 IR 边界处重新排序）。 在任何顺序跨越 emit 边界或跨 pass 输出的地方，`BTreeMap` 仍然是规则 —— 确定性保证依然成立。 ## 许可证 BSD-3-Clause。

标签：Android, DEX, DSL, Rust, 云安全监控, 云资产清单, 反编译器, 可视化界面, 编译器工具链, 网络流量审计, 逆向工程, 通知系统, 静态分析