feliam/pysymemu:intel 64符號模擬器 | 安全圈 | 专注于最新网络信息安全讯息新闻

一種符號執行工具，能够自動為x86/x64二進位程式生成有趣的輸入。

Ekoparty幻燈片：https://github.com/feliam/pysymmeu/blob/master/doc/pysymmeu.pdf？原始=真

API檔案：http://feliam.github.io/pysymemu/

特徵：

執行大多數x86/amd64指令
加載ELF32和ELF64檔案
允許通過API重新創建特定的電腦狀態
易於閱讀和擴展的指令語義
指令集可以在具體的或符號值中操作
對記憶體進行建模，使其可以是具體的或符號的（並且啟用了COW）
處理對符號指針和索引的操作
類比和符號狀態可序列化，這意味著可以暫停/恢復或並行化分析（dispy.sourceforge.net）
POSIX系統調用已建模（Linux32和Linux64）
指令測試用例的自動生成
API和說明檔案
結構單元測試的自動生成
通過pysmtlib支持的多個SMT解算器（Z3、YICES、CVC4）

依賴項：

頂石發動機解碼器/拆卸器。http://www.capstone-engine.org
z3，smt求解器。http://z3.codeplex.com/（一）
pyelftool，一個ELF解析庫。https://github.com/eliben/pyelftools

快速安裝deps？

  
  echo Installing Capstone engine
  sudo pip install capstone
  
  echo Installing pyelftools
  sudo pip install pyelftools
  
  #Install z3 SMT solver 
  echo Go to http://z3.codeplex.com/SourceControl/latest# click Download to download z3 source code
  echo Make a folder. Unzip z3 inside that folder. dos2unix on configure. Then configure;make

目錄結構

 doc/                    Slides and papers
 examples/               Asorted set of small C examples to emulate
 tutorial/               Very simple test cases
 test/                   Unittests
 setup.py                Setuputils/pipy related (not used yet)
 linux.py                The Linux operating system micro model
 memory.py               The symbolic memory model
 smtlibv2.py             Smtlib v2 solver API 
 system.py               A quick command line tool

測驗

您可以使用discover命令。

$python-m unittest發現測試

$ python -m unittest discover test

注意，cpu.py測試用例是使用test/auto中的工具半自動生成的

API檔案

您可以使用epydoc生成相當數量的API檔案。epydoc.sourceforge.net/，以下命令將生成包含api檔案的html/資料夾：

$epydoc cpu.py memory.py linux.py smtlibv2.py系統.py

$ epydoc cpu.py memory.py linux.py smtlibv2.py system.py

運行它

這是一個APLHA軟件，但是你可以直接在二進位ELF檔案上玩，直到你碰到一個未實現的指令或系統調用（2），命令列給了你一個莫名其妙的幫助。：）

 $ python system.py --help
 usage: system.py [-h] [--worspace WORSPACE] [--sym SYM] [--stdin STDIN]
                 [--stdout STDOUT] [--stderr STDERR] [--env ENV]
                 PROGRAM ...

 Symbolically analyze a program

 positional arguments:
   PROGRAM              Program to analyze
   ...                  Program arguments. Need a -- separator. Ex: -- -y 2453
 
 optional arguments:
   -h, --help           show this help message and exit
   --worspace WORSPACE  A folder name fpor temporaries and results. (default pse_?????)
   --sym SYM            Consider a filename as symbolic
   --stdin STDIN        A filename to pass as standar stdin (default: stdin)
   --stdout STDOUT      A filename to pass as standar stdout (default: stdout)
   --stderr STDERR      A filename to pass as standar stderr (default: stderr)
   --env ENV            A environment variable to pass to the program (ex. VAR=VALUE)

基本上，您傳遞一個二進位檔案供pysymemu類比。讓我們試試玩具的例子：

 $ cd examples
 $ cat toy002-libc.c

 $ make
 gcc -fno-builtin -static -nostdlib -m32  -fomit-frame-pointer  toy001-nostdlib.c  -o toy001-nostdlib
 gcc toy002-libc.c -static -o toy002-libc
 $ cd -

現在像這樣在模擬器下運行它。首先創建3個虛擬檔案來替換虛擬/類比的stdin、stdout和stderr

 $ touch stderr
 $ touch stdout
 $ echo ++++++++++ > stdin

我們將考慮stdin由符號數據填充（標記為“+”（是的，我知道）。此外，我們還需要說明環境的哪一部分應該被視為象徵性的，哪一部分是具體的。我們用--sym'stdin'標記'stdin'檔案assymbolic（它的'+'將是自由的8比特變數），如下所示：

$python system.py——sym stdin examples/toy002 libc

$ python system.py --sym stdin examples/toy002-libc

快速而骯髒的命令列工具將生成這樣的東西。。

 $ python system.py  --sym stdin examples/toy002-libc
 [+] Running examples/toy002-libc
 	with arguments: []
 	with environment: []
 [+] Detected arch: amd64
 starting
 Symbolic PC found, possible detinations are:  ['4005ab', '40059d']
 	Saving state dump_00000000004005ab_8452.pkl PC: 0x4005ab
 Program Finnished correctly
 stdin:  '\xc1\x00\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\x80\n'
 Program Finnished correctly
 stdin:  ' \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n'
 Results dumped in  ./pse_xYhZwA
 10392 3038.59649123

以及一個瘋狂的詳細的system.log檔案。還有一個包含所有中間狀態和結果的資料夾。。。

$ ls ./pse_xYhZwA
dump_000000000040059d_8452.pkl  dump_00000000004005ab_8452.pkl  dump_init.pkl  test_2.txt  test_4.txt

 $ tail -n 12341 ./pse_xYhZwA/test*
 ==> ./pse_xYhZwA/test_2.txt <==
 stdin: '\xc1\x00\x80\x80\x80\x80\x80\x80'
 
 ==> ./pse_xYhZwA/test_4.txt <==
 stdin: '\x20\x00\x00\x00\x00\x00\x00\x00'

使用一些mods，它可以接受任何可以處理（get value）命令的smtlibv2解算器。
在這種情況下，您應該轉到cpu.py或linux.py並添加必要的程式碼！