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