#use "c:\\paframework\\framework.ml";; #use "c:\\paframework\\Incubator\\Emulator.ml";; (* Phase 1: Generate trace *) let mk_initial_state eip = { mem = (fun a -> raise (MemoryContentsUnknown(a))); regs = Hashtbl.create 50; eip = eip; ssa = Hashtbl.create 50; z3 = Z3.mk_context_x [|("MODEL", "true")|]; instrs = []; } let kao_initialize_memory_and_registers () = let open Z3SymbolicExecute in let open IR in let assert_and_store_reg32 state r32 i32 = Hashtbl.replace state.regs r32 (Const(Int64.of_int32 i32,TypeReg_32)); instr_to_z3 state.z3 (Assert(IRUtil.mk_eq (IRUtil.mk_evar r32) (Const(Int64.of_int32 i32,TypeReg_32)))) in (* 00401105 is the EIP of the start of the serial checking loop *) let state = mk_initial_state 0x00401105l in let z3mem = Z3SymbolicExecute.mk_z3var state.z3 X86ToIRUtil.vMem in (* We need to point esi to the raw hex version of the activation code, which we will store at location 0x0 *) assert_and_store_reg32 state X86ToIRUtil.vEsi 0x00l; (* We need to point edi to the 32-byte output buffer, which we will store at location 0x20 *) assert_and_store_reg32 state X86ToIRUtil.vEdi 0x20l; (* We need to set ecx to 0x20 *) assert_and_store_reg32 state X86ToIRUtil.vEcx 0x20l; state;; (* Cram the state into the emulator's global state variable *) state := (kao_initialize_memory_and_registers ());; (* Emulate until EIP = 0x401111 (the end of the serial loop) *) take_steps (None) (Some(0x401111l));; (* Define a function that prints a list of IR instructions; used in the video for demonstrative purposes, not germane to the task of generating and solving constraint systems.*) let pp = List.iter (fun i -> IDA.msg "%s\n" (PpIR.ppInstr i));;