模糊测试实验

1. 实验原理

1.1. 模糊测试

模糊测试 （fuzz testing, fuzzing）是一种软件测试技术。其核心思想是将自动或半自动生成的随机数据输入到一个程序中，并监视程序异常，如崩溃，断言（assertion）失败，以发现可能的程序错误，比如内存泄漏。模糊测试常常用于检测软件或计算机系统的安全漏洞。

模糊测试工具主要分为两类，变异测试（mutation-based）以及生成测试（generation-based）。模糊测试可以被用作白盒，灰盒或黑盒测试

1.2. 黑盒、白盒、灰盒测试

  • 黑盒测试关注程序的功能是否正确，面向实际用户；
  • 白盒测试关注程序源代码的内部逻辑结构是否正确，面向编程人员；
  • 灰盒测试是介于白盒测试与黑盒测试之间的一种测试。

所以通俗来讲黑盒测试就是看我开始用一个软件，它可以满足我的需求不出错吗？白盒测试就是我写的程序代码是不是没有问题呢，我得在源程序中看看。灰盒测试就是综合两种测试策略

1.3. boofuzz

Boofuzz is a fork of and the successor to the venerable Sulley fuzzing framework. Besides numerous bug fixes, boofuzz aims for extensibility. The goal: fuzz everything.

1.4. BinWalk

Binwalk是一个快速、易用的工具，用于分析、逆向工程和提取固件图像。

1.5. QEMU

QEMU是一个通用的开源机器仿真器和虚拟化器

1.6. Firmadyne

Firmadyne是一款自动化分析嵌入式Linux系统安全的开源软件，由卡内基梅隆大学的Daming D. Chen开发完成的。它支持批量检测，整个系统包括固件的爬取、root文件系统的提取、QEMU模拟执行以及漏洞的挖掘。

1.7. Firmware Analysis Toolkit

Note:

FAT is a toolkit built in order to help security researchers analyze and identify vulnerabilities in IoT and embedded device firmware. This is built in order to use for the “Offensive IoT Exploitation” training conducted by Attify.

  • As of now, it is simply a script to automate Firmadyne which is a tool used for firmware emulation. In case of any issues with the actual emulation, please post your issues in the firmadyne issues.  

  • In case you are facing issues, you can try AttifyOS which has Firmware analysis toolkit and other tools pre-installed and ready to use.

1.8. 固件分析流程

  • StageDescription
    1. Information gathering and reconnaissanceAcquire all relative technical and documentation details pertaining to the target device’s firmware
    2. Obtaining firmwareAttain firmware using one or more of the proposed methods listed
    3. Analyzing firmwareExamine the target firmware’s characteristics
    4. Extracting the filesystemCarve filesystem contents from the target firmware
    5. Analyzing filesystem contentsStatically analyze extracted filesystem configuration files and binaries for vulnerabilities
    6. Emulating firmwareEmulate firmware files and components
    7. Dynamic analysisPerform dynamic security testing against firmware and application interfaces
    8. Runtime analysisAnalyze compiled binaries during device runtime
    9. Binary ExploitationExploit identified vulnerabilities discovered in previous stages to attain root and/or code execution

2. 实验内容

2.1. 安装固件分析工具包

固件分析工具包其实就是对Firmadyne的简单的封装，自动化了模拟新固件的过程。

1
2
3
4
5
6
7
8
9
10
11
git clone https://github.com/attify/firmware-analysis-toolkit

cd firmware-analysis-toolkit

./setup.sh

sudo vim fat.config
[DEFAULT]
sudo_password=attify123
firmadyne_path=/home/host/firmadyne
# These provide the sudo password as shown below.Firmadyne requires sudo privileges for some of its operations. The sudo password is provided to automate the process.

实物图

固件漏洞

2.3. 漏洞复现(CVE-2018-12710)

在D-Link DIR-601 2.02NA设备上发现了一个问题 在网络本地,并且仅具有 用户 帐户(这是低特权帐户)访问权限,由于管理员密码以XML显示,因此攻击者可以拦截POST请求的响应以获得 管理员权限

Running FAT

1
sudo ./fat.py dir601_revB_FW_201.bin
  • QEMU模拟路由器
  • ps:若不以sudo权限运行可能会有timeout error
  • 由于莫名的bug（死循环），FAT没法正常启动QEMU :( .懒得折腾了
  • 漏洞复现的大致思路是
    • 用用户身份登录
    • 进入后选择Tools option->Do Intercept response from this request
    • burpsuite 截获以xml显示的admin信息
1
2
3
4
5
6
7
8
9
10
HTTP/1.1 200 OK
Content-type: text/xml
Connection: close
Date: Sat, 01 Jan 2011 00:19:56 GMT
Server: lighttpd/1.4.28
Content-Length: 20088

<?xml version="1.0" encoding="UTF-8"?><root><login_level>0</login_level><admin_user><admin_user_name>admin</admin_user_name>
<admin_user_pwd>testagain</admin_user_pwd><admin_level>1</admin_level></admin_user><user_user><user_user_name>user</user_user_name>
<user_user_pwd></user_user_pwd><user_level>0 ...

2.4. Fuzz

安装

由于不可抗力，只能以FUZZ ftp服务案例作为boofuzz使用示例

  • ps:正常情况下多一步burp-suite，其他类似
1
python ftp_simple.py

3. Satisfiability modulo theories(SMT)

在计算机科学和数理逻辑中，可满足性模数理论（SMT）是确定一个数学公式是否可满足的问题。它将布尔可满足性问题（SAT）概括为涉及实数、整数和/或各种数据结构（如列表、数组、位向量和字符串）的更复杂的公式。这个名字来源于这样一个事实，即这些表达式是在一阶逻辑的某个形式化理论内（”modulo”）解释的，具有平等性（通常不允许量词）。SMT求解器（例如Z3和CVC4），旨在解决输入的实际子集的SMT问题，已经被用作整个计算机科学中广泛的工具的构建块，包括在自动定理证明、程序分析、程序验证和软件测试中。

由于布尔可满足性已经是NP-完备的，所以SMT问题通常是NP-困难的或不可判定的。研究人员研究哪些理论或理论的子集会导致可解码的SMT问题，以及可解码案例的计算复杂性。由此产生的决策程序常常直接在实际的SMT求解器中实现；例如，请看Presburger算术的可解性。SMT可以被认为是一个约束满足问题，因此是约束编程的某种形式化的方法。

4. ESBMC

ESBMC is an open source, permissively licensed, context-bounded model checker based on satisfiability modulo theories for the verification of single- and multi-threaded C/C++ programs. It does not require the user to annotate the programs with pre- or postconditions, but allows the user to state additional properties using assert-statements, that are then checked as well. Furthermore, ESBMC provides two approaches (lazy and schedule recording) to model check multi-threaded programs. It converts the verification conditions using different background theories and passes them directly to an SMT solver.

5. 参考