基于模型检查和机器学习的安卓恶意软件语义检测

### 基于模型检查和机器学习的安卓恶意软件语义检测 #### 1. 背景与动机 随着安卓恶意软件的迅速扩散，开发高效的自动分析和检测新威胁的技术变得至关重要。目前，基于签名的检测技术是最常用的方法之一，它能有效检测已知威胁，但容易被混淆技术绕过。因此，需要更强大的恶意软件检测技术。 传统的基于签名的检测技术存在以下问题： - 每个签名只能在语法上识别特定的恶意软件，无法检测其变体。 - 容易通过混淆技术规避检测。 - 难以随着恶意软件的不断演变，持续定期更新签名数据库。 为了解决这些问题，一些研究提出了静态/动态数据流分析工具来检测安卓恶意软件。这些方法能有效检测数据泄露，但无法检测更复杂的恶意行为。动态分析技术虽然有前景，但耗时较长；静态分析方法则在不断发展以应对不可判定性的挑战。 #### 2. 相关工作 ##### 2.1 基于模型检查的恶意软件检测 - **Kinder 等人**：将可执行文件的控制流图建模为 Kripke 结构，使用显式模型检查算法验证是否存在恶意模式，恶意模式用计算树谓词逻辑（CTPL）指定。 - **Battista 等人**：使用形式化方法描述安卓应用的行为，用通信系统演算（CCS）代数描述，用 μ - 演算指定常见恶意行为的时间属性，并使用并发工作台（CWB）验证算法进行验证。 - **Mercaldo 等人**：通过模型检查检测安卓勒索软件，手动检查样本提取恶意行为，用模态 μ - 演算表达，若应用的 CCS 模型满足时间逻辑属性，则判定为勒索软件。 - **Pommade**：检测二进制程序中隐藏的恶意行为，用下推自动机（PDS）建模程序栈，根据 SCTPL 或 SLTPL 指定的恶意行为进行检查。 - **Song 等人**：使用基于 Smali 反汇编器的模型构建器将安卓应用转换为 PDS，应用 SCTPL 和 SLTPL 模型检查来判断应用是否存在恶意行为，并引入谓词编码变量之间的数据依赖关系。 - **Cimino 等人**：从安卓应用的 Java 字节码派生 Lotos 进程，使用 CADP 工具包进行模型检查，验证 μ - 演算表达的逻辑规则，定位并移除恶意行为。 ##### 2.2 基于机器学习的恶意软件检测 - **Meng 等人**：结合静态分析和机器学习，从安卓恶意软件中提取常见恶意行为和模式到 DSA 中，先基于 DSA 提取的特征使用机器学习识别可疑应用，再用自动机包含进行分类。 - **[15] 的作者**：提出基于结构化特征（功能调用图的子图）的分类方法，使用图核解决图同构问题。 - **Kwon 等人**：引入下载器图抽象，根据反病毒和入侵预防系统的遥测数据构建下载图，使用影响图的属性（如增长率）作为分类特征。 - **Zhang 等人**：提出语义方法，用加权上下文 API 依赖图建模安卓应用的语义，使用基于图的特征向量对恶意和良性应用进行分类。 - **DREBIN**：进行静态特征提取，分析应用的清单文件和反汇编的 dex 代码，提取 API 调用、权限和网络地址等特征，使用机器学习算法进行二进制分类。 - **Andrana**：结合静态分析和机器学习进行二进制分类，确定一组特征（包括混淆技术的使用），反汇编应用字节码检查特征的存在，最后使用机器学习分类。 #### 3. 预备知识 ##### 3.1 LNT 语言 LNT 是由 CADP 验证工具包支持的高级形式化规范语言，结合了进程代数语言、函数式语言和命令式语言的特点。一个 LNT 规范包含控制和数据组件，系统规范由一组模块组成，模块定义可相互导入。 **进程定义**： ```plaintext <process_definition>::= process Π [ [ fg0, . . . , fgm ] ] [ [ fp1, . . . , fpn ] ] is pp1, . . . , ppl <behavior> end process <behavior>::= null // no effect (with continuation) | stop // (without continuation) | B1 ; B2 // sequential composition | var vd0, . . . , vdn in // variable declaration B0 end var | loop // forever loop B0 end loop | Π [ [actual_gates] ] [ (ap1, . . . , apn) ] // process call | select // non deterministic choice B0 [] ... [] Bn end select | par [G0, . . . , Gn in] // parallel composition [ G(i,0), . . . , G(i,ni) −>] B0 ∥... ∥ [G(i,0), . . . , G(i,ni) −>] Bm end par ``` **进程行为**： - **非确定性选择**：若进程 P 的行为是 `select B1 [] B2 end select`，则 P 要么表现为 B1，要么表现为 B2，选择由 P 与环境的交互决定。 - **并行组合**：由全局同步集 `{G0, ..., Gn}` 和接口同步集 `{G(i,0), ..., G(i,ni)}` 定义，只有当相关行为同时满足条件时，才能通过相应的门进行通信。 ##### 3.2 模态 μ - 演算 μ - 演算是 Hennessy - Milner 逻辑的扩展，用于描述标记转移系统（LTS）的属性。公式定义如下： ```plaintext ϕ :: = true | false | ¬ϕ | ϕ1 ∧ϕ2 | ϕ1 ∨ϕ2 | [K]ϕ | ⟨K⟩ϕ | μZ.ϕ | νZ.ϕ ``` LNT 进程 P 对公式 ϕ 的满足定义如下： - `P |= true` - `P ̸|= false` - `P |= ¬ϕ` 当且仅当 `P ̸|= ϕ`