Skip to content

Instantly share code, notes, and snippets.

@RKX1209

RKX1209/s2e-internal.md

Last active February 26, 2024 07:47
Show Gist options
  • Save RKX1209/21c5d614caaef1f1b07af52044f6dd03 to your computer and use it in GitHub Desktop.
Save RKX1209/21c5d614caaef1f1b07af52044f6dd03 to your computer and use it in GitHub Desktop.
Download ZIP
S2E source code internal
Raw
s2e-internal.md

S2E internal

td;al

s2e_qemu_tb_execが中心。tryでパスを実行して、例えばsymbolicなデータへのアクセスがあったりパスのマージ要求があったり、割り込みが入って制御が変わったり、Annotationによって明示的に枝刈り指定(m_doSkip)されるなどの場合、CpuExitExceptionが投げられcpu_execまで戻ってs2e_qemu_finalize_tb_execでTBクリアしてやりなおし(別のパスの実行を始める) これがconcrete->symbolicへの切り替え。 またSymbolic Execution中のパス選択はsearcherがnextStateで気める。stateはrestoreYieldedState->resumeState関数内でsearcher->addStateで追加する。SymDriveはこのsearcherのアルゴリズムを特殊なオペコード挿入などで賢く枝刈りするようにした物。

init_env

S2Eはゲストのどの変数シンボル化するなどの情報を受け取る必要がある。これには2つの方法があり、一つはターゲットのプログラムのソースを変更してs2e_make_symbolicを呼び出す事。２つ目はLD_PRELOADでバイナリ修正無しでフックして通知する。 init_envをLD_PRELOADに指定することでゲスト内でターゲットプログラム実行時の__libc_start_mainをフックしてS2Eに知らせる。 どちらもs2e_make_symbolic(guest/include/s2e-x86.h)でS2E_INSTRUCTION_SIMPLEによりS2Eのみが扱える独自の機械語を吐く。

    switch(b) {

    case 0x13f: /* s2e_op */
        {
#ifdef CONFIG_S2E
            uint64_t arg = ldq_code(s->pc);
            s2e_tcg_emit_custom_instruction(g_s2e, arg);
#else
            /* Simply skip the S2E opcodes when building vanilla qemu */
            ldq_code(s->pc);
#endif
        s->pc+=8;
        break;

    }

この独自の機械語はs2e_tcg_emit_custom_instructionで中間表現を吐く。

void s2e_tcg_custom_instruction_handler(uint64_t arg)
{
    assert(!g_s2e->getCorePlugin()->onCustomInstruction.empty() &&
           "You must activate a plugin that uses custom instructions.");

    try {
        g_s2e->getCorePlugin()->onCustomInstruction.emit(g_s2e_state, arg);
    } catch(s2e::CpuExitException&) {
        s2e_longjmp(env->jmp_env, 1);
    }
}

void s2e_tcg_emit_custom_instruction(S2E*, uint64_t arg)
{
    TCGv_i64 t0 = tcg_temp_new_i64();
    tcg_gen_movi_i64(t0, arg);

    TCGArg args[1];
    args[0] = GET_TCGV_I64(t0);
    tcg_gen_helperN((void*) s2e_tcg_custom_instruction_handler,
                0, 2, TCG_CALL_DUMMY_ARG, 1, args);

    tcg_temp_free_i64(t0);
}

s2e_tcg_custom_instruction_handler(arg)を呼ぶようなTCGを吐く。 s2e_tcg_custom_instruction_handlerはCorePluginのonCustomInstructionコールバックを呼び出すだけ。

g_s2eは(s2e/S2E.h)のS2Eクラスのインスタンスで、基本的にこのクラスを中心にコールバックなどの処理が行われる。getCorePluginはm_corePluginを返す。CorePlugin(s2e/Plugins/CorePlugin.h)は各種基本的なイベントを処理してシグナルを返す。このシグナルを上記ではemit(送信している)このシグナルでイベントを送受信しあうモデルをSignal and slotsと言いlibsigc++を使っている。emitされたシグナルはconnectされてる関数に送られる。

だいたい(qemu/s2e/S2EExecutor.cpp)にある。 switchTo(Symbolic|Concrete)が切り替え処理。Concreteへの切り替えはKLEEのtoConstantに現在の状態 makeSymbolic(s2e/S2EExecutionState.cpp)

ドライバ解析

ModuleExecutionDetectorプラグインがモジュールの実行を検出。

pluginsConfig.ModuleExecutionDetector = { pcntpci5_sys_1 = { moduleName = "pcntpci5.sys", kernelMode = true, }, }

SymbolicHardwareプラグインでハードウェアをシンボル化。readするとsymbol,writeは捨てられる。 Annotationプラグインはsymbolic executionのコントロールを行う。 function annotation_example(state, plg) -- Write custom Lua code here (e.g., to inject symbolic values) end

pluginsConfig.Annotation = { init1 = { active=true, module="pcntpci5_sys_1", address=0x169c9, instructionAnnotation="annotation_example" } } pcntpci5.sysがoffset:0x169c9を呼び出す際にannotaion_example()が実行される。

concrete -> symbolicの切り替え動作

Annotationがconfigを読んでsymbolic executionへの切り替えを行う処理を見ていく。

void Annotation::initialize()
{
if (m_moduleExecutionDetector) {
        m_moduleExecutionDetector->onModuleLoad.connect(
            sigc::mem_fun(
                *this,
                &Annotation::onModuleLoad
            )
        );
    }
}

ModuleExecutionDetectorのonModuleLoadが呼ばれたらAnnotation::onModuleLoadを実行する。

//Activate all the relevant rules for each module
void Annotation::onModuleLoad(
        S2EExecutionState* state,
        const ModuleDescriptor &module
        )
{
    foreach2(it, m_entries.begin(), m_entries.end()) {
    	const AnnotationCfgEntry &cfg = **it;
        const std::string *s = m_moduleExecutionDetector->getModuleId(module);
        if (!s || (cfg.module != *s)) {
            continue;
        }

        if (!cfg.isCallAnnotation && !m_translationEventConnected) {
            m_moduleExecutionDetector->onModuleTranslateBlockStart.connect(
                    sigc::mem_fun(*this, &Annotation::onTranslateBlockStart)
                    );

            m_moduleExecutionDetector->onModuleTranslateBlockEnd.connect(
                    sigc::mem_fun(*this, &Annotation::onModuleTranslateBlockEnd)
                    );

            m_translationEventConnected = true;
            continue;
        }

モジュールがロードされると該当モジュール内のブロックが変換された時のコールバック (onModuleTranslateBlockStart,End)を登録する。 例えばBlockStartの方が呼ばれると、

/**
 *  Instrument only the blocks where we want to count the instructions.
 */
void Annotation::onTranslateBlockStart(
        ExecutionSignal *signal,
        S2EExecutionState* state,
        const ModuleDescriptor &module,
        TranslationBlock *tb,
        uint64_t pc)
{
    m_tb = tb;

    m_tbConnectionStart = plg->onTranslateInstructionStart.connect(
            sigc::mem_fun(*this, &Annotation::onTranslateInstructionStart)
    );

    m_tbConnectionEnd = plg->onTranslateInstructionEnd.connect(
            sigc::mem_fun(*this, &Annotation::onTranslateInstructionEnd)
    );
}

onTranslateInstructionStartが登録されるようになる。

void Annotation::onTranslateInstructionStart(
        ExecutionSignal *signal,
        S2EExecutionState* state,
        TranslationBlock *tb,
        uint64_t pc)
{
    onTranslateInstruction(signal, state, tb, pc, true);
}
void Annotation::onTranslateInstruction(
        ExecutionSignal *signal,
        S2EExecutionState* state,
        TranslationBlock *tb,
        uint64_t pc, bool isStart)
{

    e.isCallAnnotation = false;
    e.module = *m_moduleExecutionDetector->getModuleId(*md);
    e.address = md->ToNativeBase(pc);

    CfgEntries::const_iterator it = m_entries.find(&e); [*]
    ...
    signal->connect(
        sigc::mem_fun(*this, &Annotation::onInstruction)
    );

}

ModuleExecutionDetectorで検知した実行中のモジュールのCfgFileを取得する。onInstructionをExecutionSignalにつなぐ。

void Annotation::onInstruction(S2EExecutionState *state, uint64_t pc)
{
    const ModuleDescriptor *md = m_moduleExecutionDetector->getModule(state, pc, true);
    ...
    if ((*it)->switchInstructionToSymbolic) {
       state->jumpToSymbolicCpp(); [*]
    }
}

*でシンボリック実行に切り替える。(switchInstructionToSymbolic=Trueの場合)

jumpToSymbolicCppはシンボリック実行キューに現在のPC,PIDを追加するだけ。

void S2EExecutionState::jumpToSymbolicCpp()
{
    if (!isRunningConcrete()) {
        return;
    }
    m_toRunSymbolically.insert(std::make_pair(getPc(), getPid()));
    m_startSymbexAtPC = getPc();
    // XXX: what about regs_to_env ?
    throw CpuExitException();
}

このm_toRunSymbolicallyはs2e_qemu_tb_exec()からexecuteTranslationBlockでブロックが実行される時に走査する。s2e_qemu_tb_exec()というのは、QEMUのcpu-exec.cから本来はtcg_qemu_tb_execが実行される所を、S2Eのconfigが有効になっているとs2e_qemu_tb_exec()が実行される。

uintptr_t s2e_qemu_tb_exec(CPUArchState* env1, struct TranslationBlock* tb)
{
    /*s2e->getDebugStream() << "icount=" << std::dec << s2e_get_executed_instructions()
            << " pc=0x" << std::hex << state->getPc() << std::dec
            << '\n';   */
    env = env1;
    g_s2e_state->setRunningExceptionEmulationCode(false);

    try {
        uintptr_t ret = g_s2e->getExecutor()->executeTranslationBlock(g_s2e_state, tb);
        return ret;
    } catch(s2e::CpuExitException&) {
        g_s2e->getExecutor()->updateStates(g_s2e_state); [*]
        s2e_longjmp(env->jmp_env, 1); [*]
    }
}

1パスのブロックを実行していって、

uintptr_t S2EExecutor::executeTranslationBlock(
        S2EExecutionState* state,
        TranslationBlock* tb)

{
	if(state->m_startSymbexAtPC != (uint64_t) -1) {
            executeKlee |= (state->getPc() == state->m_startSymbexAtPC);
            state->m_startSymbexAtPC = (uint64_t) -1; [*]
        }

        if (state->m_toRunSymbolically.size() > 0 &&  state->m_toRunSymbolically.find(std::make_pair(state->getPc(), state->getPid()))
            != state->m_toRunSymbolically.end()) {
            executeKlee = true;
            state->m_toRunSymbolically.erase(std::make_pair(state->getPc(), state->getPid()));
        }
if(executeKlee) {
        if(state->m_runningConcrete) {
            TimerStatIncrementer t(stats::concreteModeTime);
            switchToSymbolic(state);
        }
        return executeTranslationBlockKlee(state, tb); 

    } else {
        //g_s2e_exec_ret_addr = 0;
        if(!state->m_runningConcrete)
            switchToConcrete(state);

        return executeTranslationBlockConcrete(state, tb);
    }
}

[*]はSymbolicなメモリへのアクセスがあった場合。(実際はConcrete実行中に、アクセスがldであるとm_startSymbexAtPCにその時のPCが設定されてlongjmpでcpu_execまで戻り、またここにくる) CpuExitExceptionが呼ばれるとcpu_execまで戻ってやり直し。ようは1パスの実行が終了したか m_toRunSymbolicallyがあってその指定アドレスが実行される、もしくは実行しようとしているTB内にシンボリックなレジスタがある場合、KLEEで実行する必要があるためexecuteKleeがtrueになる。

executeKleeによってexecuteTranslationBlock(Klee|Concrete)に分岐する。

concrete実行時はsymbolicなメモリアドレスへのアクセスがあるかどうかのチェックを行っている。これは(qemu/softmmu-template.h)内の各メモリアクセスヘルパー関数内でS2E_FORK_AND_CONCRETIZE_ADDRでチェックされ

#define S2E_FORK_AND_CONCRETIZE(val, max) \
    tcg_llvm_fork_and_concretize(val, 0, max)

#define S2E_FORK_AND_CONCRETIZE_ADDR(val, max) \
    (g_s2e_fork_on_symbolic_address ? S2E_FORK_AND_CONCRETIZE(val, max) : val)
||<

tcg_llvm_fork_and_concretizeは(qemu/s2e/S2EExecutor.cpp)でhandleForkAndConcretizeと定義されている。

void S2EExecutor::handleForkAndConcretize(Executor* executor,
                                     ExecutionState* state,
                                     klee::KInstruction* target,
                                     std::vector< ref<Expr> > &args)
{
    ref<Expr> address = args[0];

    address = state->constraints.simplifyExpr(address);
    klee::ref<klee::Expr> concreteAddress;

    if (ConcolicMode) {
        concreteAddress = state->concolics.evaluate(address);
        assert(dyn_cast<klee::ConstantExpr>(concreteAddress) && "Could not evaluate address");
    } else {
        //Not in concolic mode, will have to invoke the constraint solver
        //to compute a concrete value
        klee::ref<klee::ConstantExpr> value;
        bool success = s2eExecutor->getSolver()->getValue(
                Query(state->constraints, address), value); [*]

        concreteAddress = value;
    }

    klee::ref<klee::Expr> condition = EqExpr::create(concreteAddress, address);

    if (!state->forkDisabled) { [*]
        //XXX: may create deep paths!
        StatePair sp = executor->fork(*state, condition, true);

        s2eExecutor->bindLocal(target, *state, concreteAddress);
        s2eExecutor->notifyFork(*state, condition, sp);
    } else {
        state->addConstraint(condition);
        s2eExecutor->bindLocal(target, *state, concreteAddress);
    }
    
}

[]で現状のconstraintsを解いて、concreateなアドレスを設定。[]のforkする処理はoverconstrainingを回避するために、concreateな値(ex. x=4)にしてみて後でやり直すためにforkしておく(論文2.2参照)

また(qemu/softmmu-template.h)内でs2e_trace_memory_accessがコールバックも行っている。

(qemu/s2e/Plugins/CorePlugin.cpp)

|c| static void s2e_trace_memory_access_slow( uint64_t vaddr, uint64_t haddr, uint8_t* buf, unsigned size, int isWrite, int isIO) { uint64_t value = 0; unsigned copy_size = (size > sizeof value) ? sizeof (value) : size; memcpy(&value, buf, copy_size);

try {
    g_s2e->getCorePlugin()->onDataMemoryAccess.emit(g_s2e_state,
        klee::ConstantExpr::create(vaddr, 64),
        klee::ConstantExpr::create(haddr, 64),
        klee::ConstantExpr::create(value, copy_size << 3),
        isWrite, isIO);
} catch(s2e::CpuExitException&) {
    s2e_longjmp(env->jmp_env, 1);
}

}

/**

  • We split the function in two parts so that the common case when
  • there is no instrumentation is as fast as possible. / void s2e_trace_memory_access( uint64_t vaddr, uint64_t haddr, uint8_t buf, unsigned size, int isWrite, int isIO) { if(unlikely(!g_s2e->getCorePlugin()->onDataMemoryAccess.empty())) { s2e_trace_memory_access_slow(vaddr, haddr, buf, size, isWrite, isIO); } } ||<

またメモリの読み込み時はs2e_read_ram_concrete_check(S2EExecutionState.cpp)でシンボルメモリをチェックして m_startSymbexAtPCでその時PCを保存し、s2e_longjmpで飛ぶ。ちなみにs2e_longjmpはsetjmpされた時の状態(s2e_jmpbuf)にレジスタが全て戻る。(RIPも戻るので結果的に実行もそこに戻る。setjmpはs2e_setjmpから戻る先のアドレスを保存するので、結果的にs2e_setjmpの直後にlongjmpで戻る事になる。) (qemu/s2e/x64.asmを参照) 飛ぶ先はs2e_cpuExitJmpBuf(executeTranslationBlockConcreteを指している)で、executeTranslationBlockConcreteのs2e_setjmpの直後すなわちif文の中に飛ぶ。そこでjmpenvをexecuteTranslationBlockConcreteの始まりに設定しなおして、CpuExitExceptionをthrowする。これをs2e_qemu_tb_execがキャッチしてさらにlongjmp。すると

[参照: http://www.lai18.com/content/8806128.html]

EPT violationでフックする時、read flagだけ落とすとwriteは無視できる。

KLEEはブランチでforkする時notifyBranch(S2EExecutor.cpp)を呼ぶ。このnotifyBranchにs2eState->getDeviceState()->saveDeviceState();でデバイスの状態をスナップショットで保存。

KLEE

[Interpreter] 基本はklee::InterprterがLLVM bitcodeを実行する。klee::Executorがインスタンス。 各パスに一つklee::ExecutionStateがあってレジスタやメモリの状態を保持してる。 分岐点でklee::Executor::forkがStatePairsを返す。

[Memory model] MemoryObjectはアロケートされたメモリの場所を示す。実際にある具体値はObjectState。 各ExecutionStateはMemoryObjects->ObjectStateの対応マップを持っている。マップはAddressSpace構造体でimmutable tree。各AddressSpaceはObjectStateをいくつか保持しているが、AddreesSpace自体が増えた場合は、ObjectStateは最初はコピーせず書き込みがあったらコピーする(COW) この仕組み上基本的にスタック,ヒープ,bssなどの違いは無いが、スタックだけMemoryObjectがisLocalになってStackFrameというリストに繋がれる。

[Expression] 多くのExprクラスはllvm命令列に従う。refが式への参照カウンタ(?)を持つ。 Exprには種類がある。ConcatExpr,ExtractExpr,ReadExprなど。 ちなみに配列アクセスは、具体値のindexへの書きこみはObjectStateがキャッシュしておく。シンボリックなindexへのアクセスは(書き込む場所が決まらないため)UpdateListとして更新値をキャッシュしておく。

[Searcher] klee::Searcherで次のどのstateを実行するかを選ぶ。

#LLVM IR変換,KLEE実行の流れ 上記のexecuteTranslationBlockKleeがcpu_gen_llvm(qemu/translate-all.c)を最初に呼び出して、与えれたTranslationBlockに対してLLVMコードを生成している。cpu_gen_llvmはゲストのバイナリ->TCG->LLVMへの変換を一括で行う関数。TCG->LLVMはtcg_llvm_gen_code(tcg/tcg-llvm.cpp)が担う。 またQEMUのバイナリ変換のメインループであるcpu_gen_code(translate-all.c)中でもgenerate_llvmフラグが立っていると、tcg_llvm_gen_codeでllvmコードを生成している。

(qemu/s2e/S2EExecutor.cpp)

|cpp| uintptr_t S2EExecutor::executeTranslationBlockKlee( S2EExecutionState* state, TranslationBlock* tb) { tb_function_args[0] = env; tb_function_args[1] = 0; tb_function_args[2] = 0;

++state->m_stats.m_statTranslationBlockSymbolic;

/* Generate LLVM code if necessary */
if(!tb->llvm_function) {
    cpu_gen_llvm(env, tb); [*]
    assert(tb->llvm_function);
}
/* Prepare function execution */
prepareFunctionExecution(state,
        tb->llvm_function, std::vector<ref<Expr> >(1,
            Expr::createPointer((uint64_t) tb_function_args))); [*]

if (executeInstructions(state)) { [*]
    throw CpuExitException();
}

/* Get return value */
ref<Expr> resExpr =
        getDestCell(*state, state->pc).value;
assert(isa<klee::ConstantExpr>(resExpr));

return cast<klee::ConstantExpr>(resExpr)->getZExtValue();

} ||<

[]生成されたLLVMコードはtb->llvm_functionに保存されて、[]で準備をして [*]のexecuteInstructionsで実行。この関数はKLEEで命令を実行途中にそのパスが何らかの理由で終了するとtrueを返す。

inline bool S2EExecutor::executeInstructions(S2EExecutionState *state, unsigned callerStackSize) { try { while(state->stack.size() != callerStackSize) { ++state->m_stats.m_statInstructionCountSymbolic;

        KInstruction *ki = state->pc;

        stepInstruction(*state); [*]
        executeInstruction(*state, ki); [*]

        updateStates(state); [*]

        //Handle the case where we killed the current state inside processFork
    }
}
return false;

} stepInstruction,executeInstructionはKLEEの関数(klee/lib/Core/Executor.cpp) executeInstructionは渡されてきたExecutionState(1パスを表す状態)とKInstructionのオペコードをエミュレートする。 (これはbr,call,retあたりのブランチ命令だけエミュレートでは駄目なの？ -> 駄目。 各Stateはパスごとに違い、そのstateによって通常の命令実行にも影響がでるのでその影響を見つつ全命令インタプリトする必要あり) 例えばAdd命令だと

|cpp| case Instruction::Add: { ref left = eval(ki, 0, state).value; ref right = eval(ki, 1, state).value; bindLocal(ki, state, AddExpr::create(left, right)); break; } ||<

このleft,rightがシンボリックだったら？ よってKLEEはただちに命令列をインタプリトするのではなく、各式をbindLocalで追加していく設計。

stateの切り替えはstateSwitchTimerCallbackで行う。この関数はQEMUのタイマーで定期的に呼ばれる。

|cpp| void S2EExecutor::stateSwitchTimerCallback(void *opaque) { S2EExecutor c = (S2EExecutor)opaque;

if (g_s2e_state) {
    c->doLoadBalancing(); [*]
    S2EExecutionState *nextState = c->selectNextState(g_s2e_state); [*]
    if (nextState) {
        g_s2e_state = nextState;
    } else {
        //Do not reschedule the timer anymore
        return;
    }
}

qemu_mod_timer(c->m_stateSwitchTimer, qemu_get_clock_ms(host_clock) + 100);

} ||< [*]のselectNextStateでsearcherから選んだ次のstateに切り替える

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment