Firmalice – Automatic Detection of Authentication Bypass Vulnerabilities in Binary Firmware

美国加州大学圣塔芭芭拉分校信息安全实验室

知名CTF战队Shellphish主力成员

二进制安全研究方向

论文发表于NDSS 2015

摘要：

Firmalice，嵌入式设备二进制分析框架，支持符号执行，程序切片

使用一种认证缺陷模型查找用户输入型后门

查找三种商用设备中两类存在后门

介绍：

物联网设备迅速增加，种类繁多，覆盖率变高

设备更加智能和复杂，如打印机、摄像机、手表、眼镜等

设备之间通过软件（固件）进行连接和交流，如智能电视、门锁、摄像机、电表等

设备间会传递敏感信息（如电表、节目单等）或实现重要功能（如开锁），固件错误或恶意攻击会导致严重后果。如智能电表暴露用户日程和隐私，门锁允许非授权访问等。

固件中包含大量错误，如内存泄露、命令执行、逻辑缺陷等

认证绕过–后门，厂商预留用于管理和升级

无线路由器80%存在问题，Linksys路由器后门组建了30K级别僵尸网络

固件后门探测的难点：

设备专有、源码不公开、固件直接运行在硬件上而不是操作系统层

固件运行不标准（加载偏移、执行入口地址等） –> binary blob 固件

有厂商密码签名保护，难以进行修改分析

固件无法执行和修改，密码签名保护、硬件差异。已有固件分析系统基本是静态，不需要执行，无法处理复杂固件，并且需要有源码为前提。

当前后门检测方法都是手工：

1、对不同设备分析时很不实用

2、固件代码的复杂性使得手工分析依然存在错误

提出Firmalice，自动化查找后门、面向二进制层、大规模、无需设备源码

创建了一种基于用户输入的认证绕过模型。

特权操作定义不同，根据固件样本找到特定安全策略，加载样本，将二进制代码翻译为中间表示IR，进行静态全程序控制流和数据流以及符号执行分析。并测试了三种不同的固件：打印机、电表、摄像头

贡献

1、基于输入的认证绕过模型

2、自动化分析复杂的固件二进制代码

3、测试三种真实设备并发现漏洞，超越手工分析

认证绕过漏洞

特点：先授权后执行特权操作

种类：

1、硬编码 — 字符比较strcmp()

2、隐藏认证接口

3、无意bug — 命令执行

只关心输入和结果，不关心认证过程

实现

步骤：

1、固件载入

2、安全策略 — 找特权操作点

3、静态分析 — 从入口点到特权点生成程序认证切片

4、符号执行 — 查找运行到特权操作点的所有路径

5、后门检查 — 验证是否是后门，输出结果

固件载入部分

1、用户空间固件 — 运行在通用操作系统上，调用系统函数

2、binary-blob固件 — 运行在硬件上，初始化和运行时通常未知，载入偏移和程序入口点未知 –> [Static disassembly of obfuscated binaries]解决方法

固件载入 –> 反编译+IR（消除处理器架构差异） –> 跳转表位置和间接跳转指令之间的关系确定 –> 扫描获取函数，添加其中的call直至return指令，生成粗粒度CFG图，所有根节点都作为程序入口点（大部分无法到达特权程序点）

安全策略

查找特权程序点

静态输出 — 登录成功提示字符 DFG

行为准则 — 执行特权操作 CFG+DFG

内存访问 — DFG

指定特区函数 — 特权函数访问地址

静态分析

程序后向切片，从特权函数点反溯到程序入口点

创建PDG程序依赖图 — 包括 数据依赖图DDG 和 流程依赖图 CDG

1、生成CFG图

2、生成CDG — 从CFG转化

3、生成DDG — 内容、流敏感的数据流分析 def-use chains

4、后向切片 — 根据给定程序点，可以生成路径切片

符号执行

A、Symbolic State and Constraints 符号状态和约束条件

抽象表达式，描述跳转和约束条件，跟随约束路径直至特权函数点，求约束解

B、Symbolic Summaries 象征性总结

匹配特征函数，安排测试用例

C、Lazy Initialization 延迟初始化

binary-blob型固件 初始化比较复杂 监控内存地址的读写操作

认证绕过确认

约束求解，从用户输入到特权函数点，验证是否是登录绕过

A、确定输入输出

程序间交互，如网络连接，加载文件，ASCII码等

B、数据泄露

C、约束求解

结果

三个真实的物联网设备：智能电视、监控摄像头、打印机；已知存在的后门

使用本文方法成功验证两个后门，第三个因为认证逻辑过程过于复杂检测失败

局限

混淆和复杂的固件，数学运算型后门难以发现

提高符号化循环分析能力

总结

本文开发了IOT固件分析工具Firmalice，使用一种新的基于用户输入的认证绕过模型，定位认证后的特权操作地址，根据程序的CFG图和DDG图，获取程序后向切片，对程序进行符号化执行分析查找执行路径，确认程序输入点，最后进行认证绕过（后门）的测试确认，可以自动化实现，提高了人工查找后门的低效率。