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图,获取程序后向切片,对程序进行符号化执行分析查找执行路径,确认程序输入点,最后进行认证绕过(后门)的测试确认,可以自动化实现,提高了人工查找后门的低效率。

您可能还喜欢...