#pysymemu internal #system 1パスを表すStateクラス。StateクラスごとにSolverがあってそのパスの制約を解く。 Executorが最初のstateを作る。 state = State(args.program, args.argv, env ) executor = Executor(workspace=args.workspace) executor.putState(state)
Stateは__init__でargumentやenvを見て、そのデータの中にWILDCARD('+')が入っていたらmakeSymbolicでその部分をシンボルとして扱う。os.exeで初期レジスタ諸々の設定。 シンボルはsolver.mkArrayで生まれたSymbolオブジェクトをそのまま使い続ける。つまりargvなども実はSymbolオブジェクトを指している事になる。ちなみにsolver.mk***系は裏でz3にコマンドを投げてz3内にも適時対応する変数などを作っている。 system.pyからcurrent_state.executeでインタプリト開始。capstoneでinsn_nameでオペランド名を取得して、応じたメソッドを呼び出す方式。この実行中に例えばJNB命令のようなcpu.PCが条件によって移る(分岐する)ケースがあれば、ITEBVでその条件とtrue/falseの時の分岐先をBitVecとしてまとめてPCに保存する。これで次にexecuteを実行するとBitVecのインスタンスなので
|py| def execute(cpu): ''' Decode, and execute one intruction pointed by register PC''' if not isinstance(cpu.PC, (int,long)): raise SymbolicPCException(cpu.PC) ||<
でSymbolicPCExceptionが飛ぶ。またPCだけでなく条件付きmovzなども同様になる。
|py| def CMOVZ(cpu, dest, src): ''' Conditional move - Equal/zero.
Tests the status flags in the EFLAGS register and moves the source operand
(second operand) to the destination operand (first operand) if the given
test condition is true.
@param cpu: current CPU.
@param dest: destination operand.
@param src: source operand.
'''
dest.write(ITE(dest.size, cpu.ZF, src.read(), dest.read()))
||<
つまりこれはmovの先の値がcpu.ZFによって変わりうるというBitVecになっている。 このwrite(store)はメモリモデルへの書きこみ。 またread(load)は具体値かBitVecを返す。
ProgramがFinishedするとテストケースを生成する。これはgenerate_testcaseでsolver.getvalue(input_symbol[i])で解の候補を一つ得る。 ちなみにSolverクラスはPopen('z3 -t:120 -smt2 -in', shell=True, stdin=PIPE, stdout=PIPE)とかでz3を実行して_sendでコマンドを送ってる。コマンドはSMT-LIB2.0に準拠。つまり実質SATを解いてるのはz3。
SymbolicPCExceptionを受け取るとそのPCからあり得るパスをgetallvaluesで見つけ、その中から一つ(val[0])選ぶ。残りはfork(branch関数)してexecutorに追加しておく。 getallvaluesは与えれたシンボルx
#まとめ つまりpysymemuは完全なSymbolic Executionを行っていて、インタプリトで実行して、例えばメモリから読んで計算して書き込むような命令があれば、それらメモリの値は具体値(int)かBitVecになっている。BitVec+具体値とかはBitVec+BitVec.cast(具体値)になる。