Android测试新范式：合成符号执行技术

作者与发表情况 本研究报告基于一篇发表于2018年ACM/IEEE自动化软件工程国际会议（ASE）的学术论文。该论文的主要作者包括：来自新加坡国立大学（National University of Singapore）的Xiang Gao（通讯作者）、Zhen Dong和Abhik Roychoudhury，以及来自中国南方科技大学的Shin Hwei Tan（该工作完成于新加坡国立大学）。论文标题为“Android Testing via Synthetic Symbolic Execution”。

学术背景与研究目标 本研究的核心领域是软件工程中的软件测试与调试，具体聚焦于Android应用的自动化测试技术。在Android应用测试中，符号执行（Symbolic Execution）是一种强大的程序分析技术，能够同时探索程序在不同输入下可能采取的多条路径。然而，将其应用于Android应用面临巨大挑战，因为Android应用高度依赖复杂且不断演进的Android框架/库。传统的符号执行方法在处理这类框架时，通常采用两种极端策略：一是“体外”（in-vitro）方法，即手动或半手动地为Android库构建模型（如JPF-Android工具），这种方法工作量大且难以跟上Android API的快速更新；二是“体内”（in-vivo）方法，即在真实设备上执行库代码，但这会导致符号值流入库后其约束关系丢失，引发“路径发散”（path divergence）问题，使得符号执行无法探索后续受库返回值影响的分支。

为了验证建模Android库的重要性，研究团队对68个Android应用（来自AndroTest基准集）进行了初步研究。通过污点分析，他们发现平均有37.1%的分支决策受到Android库调用结果的影响。这一数据表明，如果不能妥善处理库行为，符号执行将错过大量潜在的执行路径。

因此，本研究旨在解决上述难题。其核心目标是：在不依赖任何手动建模Android执行环境（即库）的前提下，构建一个动态符号执行（即混合执行，Concolic Execution）引擎，以缓解路径发散问题并提升Android应用的测试分支覆盖率。他们提出了一种名为“合成符号执行”（Synthetic Symbolic Execution）的新方法，其关键创新在于通过“按需程序合成”（on-demand program synthesis）来自动推断并精化库函数的符号表示。

详细研究流程与方法 本研究主要包含方法设计、系统实现与实验评估三大环节，其核心是所提出的“合成符号执行”工作流。

1. 核心方法：合成符号执行工作流 研究团队基于现有的Java混合执行引擎（具体实现中选择了JDart）进行扩展。整个流程围绕算法1（PathExploration 和 ExecuteConcolic）展开。当对Android应用进行混合执行时，引擎会同时维护具体内存（存储变量实际值）和符号内存（存储变量符号表达式）。执行过程中，对于遇到的方法调用语句，引擎进行区分处理： * 普通Java语句：由底层的混合执行引擎正常处理，收集路径约束。 * Android库调用语句：引擎会使用参数的具体值在真实Android设备/模拟器上具体执行该库方法，并获得一个具体的返回值。 * 关键合成触发点：如果该库调用的至少一个参数是符号变量，并且其返回值在后续程序分支决策中被使用，则引擎将创建一个待合成的函数δ来表示这个库调用。此时，返回值在符号内存中被标记为δ(输入符号变量)，从而将符号信息“流过”了具体执行的库。

当一次执行路径探索完成后，引擎像传统混合执行一样，选择路径条件中的一个分支条件进行取反，生成新的路径约束pc'。如果pc'中包含待合成的函数δ，则触发合成过程（算法2: Synthesize），而非直接求解。

2. 按需与迭代式程序合成 合成引擎的目标是生成一个表达式e，使其能近似表示库函数δ的行为，并帮助生成新的输入以探索目标分支（即所有受该库调用结果影响的分支）。合成过程是迭代和上下文相关的： * 初始化：基于第一次具体执行产生的输入输出对<in0, out0>，初始化表达式e为常数out0。 * 求解与验证：将约束pc' ∧ δ = e（或pc' ∧ δ ≠ e）提交给SMT求解器（如Z3），尝试生成新的输入x'。 * 具体执行与反馈：使用x'在真实环境中再次运行程序，得到新的输入输出对<in', out'>和实际执行的路径π。 * 判断与精化：如果π是目标路径，则合成成功，返回新输入x'用于后续探索。否则，将<in', out'>加入已有的输入输出对集合R，并调用基于组件的合成器（component-based synthesis）生成一个更符合所有R中观察结果的新的表达式e。然后重复上述过程。 * 合成组件与策略：合成器采用分层策略，按照复杂度递增的顺序尝试不同类型的组件：常量 → 位运算 → 算术运算 → 流程控制（如if-then-else）→ 数组访问。这种策略有助于降低合成复杂度。合成过程是“上下文相关”的，意味着它会为同一库方法在不同程序点（即不同的全局状态上下文）的调用生成不同的表达式，这通常能产生更精确的模型，因为库在特定上下文中可能只展现部分行为。

3. GUI约束的收集与整合 为了生成有效的、能被应用接受的输入，研究还提出了自动收集和整合图形用户界面（GUI）约束的方法。这些约束来自应用配置（XML）和运行时UI层次结构，例如屏幕边界、编辑框最大长度、列表项数量等。他们定义了一系列模板（如表2所示），将这些高层语义的GUI约束转化为SMT求解器能理解的逻辑约束，并将其加入路径条件pc中。

4. 系统实现：SYNTHESISE 研究团队实现了名为SYNTHESISE的工具。其架构分为三层： * 混合执行层：基于JDart，负责程序符号执行、约束收集与求解。 * JVM-Android通信层：通过修改JPF/JDart的模型Java接口（MJI），将Android API调用委托给通过Android调试桥（ADB）连接的真实设备执行。 * 执行环境层：包括运行符号执行的Java环境，以及运行具体Android代码的真实设备/模拟器环境。 合成引擎部分基于现有的程序合成工作（通过二阶约束求解实现）构建，并采用了上述的分层组件策略。

5. 实验评估设计与对象 为了评估SYNTHESISE的有效性，研究设置了两个研究问题（RQ）： * RQ1：将受Android库调用影响的所有分支视为目标，使用SYNTHESISE能到达多少目标？（对比基线） * RQ2：合成出的库代码质量如何？需要多少次迭代？ 实验选择了14个开源Android应用作为评估对象。选择过程如下：首先从JPF-Android工具支持的模型库中，筛选出具有基本类型输入和输出的方法；然后随机选取20个；最后通过GitHub找到实际调用这些方法、且其返回值确实影响分支决策的应用，最终确定了14个应用-方法对（如表3所示，例如getOffsetForPosition, getColor等方法）。每个应用的行数（LoC）从100行到16K行不等。 对比实验设置了三种变体： * Concrete：混合执行，但Android库完全具体执行（不合成，代表存在路径发散问题的基线）。 * SYNTHESISE：采用本研究提出的按需合成方法。 * JA Model：使用JPF-Android中已有的（半手动）模型进行混合执行。为了公平比较，将JPF-Android的模型导入到与SYNTHESISE相同的JDart引擎中运行，而非直接运行JPF-Android工具本身。

主要研究结果 1. 目标到达能力（RQ1） 实验结果如表5所示。对于大多数受测应用，SYNTHESISE在到达受库调用影响的分支（目标）方面表现优于其他方法： * 对比JA Model：在14个案例中，SYNTHESISE在9个案例中到达了更多目标。例如，在getColor方法中，SYNTHESISE到达了全部18个目标，而JA Model仅到达1个；在getOffsetForPosition方法中，SYNTHESISE到达6个，JA Model到达3个。对于checkSignatures方法，JA Model的模型会抛出异常，导致无法到达任何目标，而SYNTHESISE到达了1个（标注NA表示因达到迭代上限未合成出到达更多目标的表达式）。只有在少数几个案例（如compareSignalLevel）两者表现持平。 * 对比Concrete基线：SYNTHESISE在除了两个合成失败（达到迭代上限）和一个因单次测试输入限制所有方法均未完全到达的案例（getDimensionPixelOff）外，均到达了更多或相同的目标。这直接证明了合成模型能有效恢复因具体执行而丢失的约束，从而探索到原本因路径发散而无法到达的分支。 结论：SYNTHESISE能够到达更多受库输出影响的目标分支。

2. 合成结果质量（RQ2） 合成细节如表4所示。主要发现如下： * 合成成功率与效率：在14个目标方法中，SYNTHESISE成功为12个合成了表达式（其余2个达到迭代上限）。合成迭代次数从1次到15次不等，平均耗时约103秒。迭代次数少的通常是算术或位运算表达式，而需要模拟资源访问（如getColor根据资源ID取值）的方法通常合成为数组访问表达式，需要更多迭代。 * 表达式正确性分类：研究团队手动将合成表达式lib_syn与真实Android库实现lib_real进行比较，定义了三个正确性等级： * C1 正确：2个表达式语义完全匹配真实库。 * C2 条件正确：9个表达式在特定输入范围内行为一致。例如，为calculateSignalLevel合成的表达式0.18*x1+18在大多数输入下正确，但当输入x1小于某个常量min_rssi时，真实库返回0，而合成表达式未捕获此边界。若提供更多输入输出对，合成器可以精化出更精确的表达式。 * C3 上下文相关正确：在C2的9个中，有3个同时是上下文相关的，即它们仅模拟了在特定程序上下文（全局状态）下的库行为。 * 对比JA Model质量：研究表明，SYNTHESISE合成的模型通常比JPF-Android中的半手动模型更准确。许多JA Model简单地返回常量（如0或top_int）或仅处理部分参数，而SYNTHESISE能合成出反映输入输出关系的表达式（如算术运算、数组映射）。 结论：所有在迭代上限内合成的表达式都是正确、条件正确或上下文相关正确的，且常比现有手动/半自动模型更精确。

研究结论与价值 本研究提出并实现了“合成符号执行”，这是一种用于Android应用测试的新型混合执行方法。其核心贡献在于： * 按需框架合成：通过动态、按需的程序合成来自动推断Android库的输入输出关系，无需人工建模，从而使得符号执行引擎能够适配不同的Android SDK版本。该方法也适用于其他使用库的代码的符号执行。 * 整合GUI约束：自动提取并整合应用配置和UI层级中的约束，确保生成的测试输入符合应用的实际接受范围。 * 证明了建模Android库的重要性：通过实证研究量化了Android库调用对应用分支决策的广泛影响（平均37.1%），为相关研究提供了依据。 * 有效的实现与评估：构建了SYNTHESISE工具，并在真实应用上验证了其相较于传统具体执行和使用现有模型的方法，能够到达更多的受库影响的分支，且合成的模型质量更高。

研究亮点 1. 方法创新性：提出了介于“体内”和“体外”方法之间的“合成符号执行”新范式。它既不预先建模库（避免模型维护负担），也不仅仅具体执行库（避免路径发散），而是通过运行时合成来捕获库行为对符号探索的关键影响。 2. 按需与上下文相关合成：合成并非一次性生成完整库模型，而是根据符号执行探索路径的需要动态触发，并为特定调用上下文生成更精确的表达式。这提高了合成效率与针对性。 3. 实用性强：研究包含了从理论方法、算法设计、系统实现到实证评估的完整链条。提出的GUI约束整合机制增强了生成测试输入的有效性。工具基于现有成熟引擎（JDart）构建，提高了实用性。 4. 扎实的评估：评估设计合理，不仅对比了合成与不合成的效果，还与广泛使用的JPF-Android模型进行了直接比较，并通过手动分析验证了合成结果的质量，结论令人信服。

其他价值 本研究展示了程序合成技术与符号执行相结合解决软件测试中环境建模难题的巨大潜力。它不仅适用于Android测试，其“通过合成捕捉环境行为”的核心思想，对解决其他框架或库依赖严重的程序的符号执行问题也具有启发意义。论文最后指出，该方法发现的程序崩溃可用于驱动现有的自动程序修复技术，展现了其在软件质量保障全链条中的应用前景。