<s> import reil <EOL> import reil . x86 . translator as x86 <EOL> from concolica . utils import * <EOL> from concolica . vulnerabilities import * <EOL> from smt import bitvector as bv <EOL> def operand_value ( s , o ) : <EOL> output = o <EOL> if isinstance ( o , reil . ImmediateOperand ) : <EOL> output = bv . Constant ( o . size , o . value ) <EOL> elif isinstance ( o , reil . RegisterOperand ) : <EOL> output = s . registers [ o . name ] <EOL> if output . size > o . size : <EOL> output = output . extract ( o . size ) <EOL> elif output . size < o . size : <EOL> output = output . zero_extend_to ( o . size ) <EOL> return output <EOL> def op_add ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a + b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_and ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a & b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_bisz ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> dst = i . output <EOL> result = bv . if_then_else ( <EOL> a == bv . Constant ( a . size , <NUM_LIT:0> ) , <EOL> bv . Constant ( dst . size , <NUM_LIT:1> ) , <EOL> bv . Constant ( dst . size , <NUM_LIT:0> ) ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_bsh ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> if b . value >= <NUM_LIT:0> : <EOL> result = a << b <EOL> else : <EOL> result = a >> bv . Constant ( b . size , abs ( b . value ) ) <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_div ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a // b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_jcc ( i , s ) : <EOL> ss = [ ] <EOL> a = operand_value ( s , i . input0 ) <EOL> dst = operand_value ( s , i . output ) <EOL> branch = a . can_be_nonzero ( ) <EOL> dont_branch = a . can_be_zero ( ) <EOL> if s . solver . check ( branch ) : <EOL> if s . solver . check ( dont_branch ) : <EOL> a = s . fork ( ) <EOL> a . solver . add ( branch ) <EOL> ss += a . branch ( dst ) <EOL> b = s . fork ( ) <EOL> b . solver . add ( dont_branch ) <EOL> ss . append ( b ) <EOL> else : <EOL> ss = s . branch ( dst ) <EOL> else : <EOL> ss = [ s ] <EOL> return ss <EOL> def op_ldm ( i , s ) : <EOL> src = operand_value ( s , i . input0 ) <EOL> dst = i . output <EOL> s . registers [ dst . name ] = s . read ( src , dst . size ) <EOL> if s . registers [ dst . name ] is None : <EOL> import pdb <EOL> pdb . set_trace ( ) <EOL> return [ s ] <EOL> def op_mod ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a % b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_mul ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a * b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_nop ( i , s ) : <EOL> return [ s ] <EOL> def op_or ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a | b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_stm ( i , s ) : <EOL> val = operand_value ( s , i . input0 ) <EOL> dst = operand_value ( s , i . output ) <EOL> s . write ( dst , val ) <EOL> return [ s ] <EOL> def op_str ( i , s ) : <EOL> src = operand_value ( s , i . input0 ) <EOL> dst = i . output <EOL> src = src . resize ( dst . size ) <EOL> s . registers [ dst . name ] = src <EOL> return [ s ] <EOL> def op_sub ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a - b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_undef ( i , s ) : <EOL> reg = i . input0 <EOL> if reg . name in s . registers : <EOL> s . registers [ reg . name ] = None <EOL> return [ s ] <EOL> def op_unkn ( i , s ) : <EOL> raise NotImplementedError ( ) <EOL> def op_xor ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a ^ b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_bisnz ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> dst = i . output <EOL> result = bv . if_then_else ( <EOL> a != bv . Constant ( a . size , <NUM_LIT:0> ) , <EOL> bv . Constant ( dst . size , <NUM_LIT:1> ) , <EOL> bv . Constant ( dst . size , <NUM_LIT:0> ) ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_equ ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> result = bv . if_then_else ( <EOL> a == b , <EOL> bv . Constant ( dst . size , <NUM_LIT:1> ) , <EOL> bv . Constant ( dst . size , <NUM_LIT:0> ) ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_lshl ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a << b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_lshr ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a . logical_shift_right ( b ) <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_ashr ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = a >> b <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_sdiv ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> b = operand_value ( s , i . input1 ) <EOL> dst = i . output <EOL> operation_size = max ( a . size , b . size , dst . size ) <EOL> a = a . resize ( operation_size ) <EOL> b = b . resize ( operation_size ) <EOL> result = bv . BinaryOperation ( a , bv . BinaryOperator . SignedDivide , b ) <EOL> result = result . resize ( dst . size ) <EOL> s . registers [ dst . name ] = result <EOL> return [ s ] <EOL> def op_sex ( i , s ) : <EOL> a = operand_value ( s , i . input0 ) <EOL> dst = i . output <EOL> value = a . sign_extend_to ( dst . size ) <EOL> s . registers [ dst . name ] = value <EOL> return [ s ] <EOL> def op_sys ( i , s ) : <EOL> return s . kernel . dispatch ( s , i ) <EOL> opcode_map = { <EOL> reil . ADD : op_add , <EOL> reil . AND : op_and , <EOL> reil . BISZ : op_bisz , <EOL> reil . BSH : op_bsh , <EOL> reil . DIV : op_div , <EOL> reil . JCC : op_jcc , <EOL> reil . LDM : op_ldm , <EOL> reil . MOD : op_mod , <EOL> reil . MUL : op_mul , <EOL> reil . NOP : op_nop , <EOL> reil . OR : op_or , <EOL> reil . STM : op_stm , <EOL> reil . STR : op_str , <EOL> reil . SUB : op_sub , <EOL> reil . UNDEF : op_undef , <EOL> reil . UNKN : op_unkn , <EOL> reil . XOR : op_xor , <EOL> reil . BISNZ : op_bisnz , <EOL> reil . EQU : op_equ , <EOL> reil . LSHL : op_lshl , <EOL> reil . LSHR : op_lshr , <EOL> reil . ASHR : op_ashr , <EOL> reil . SDIV : op_sdiv , <EOL> reil . SEX : op_sex , <EOL> reil . SYS : op_sys , <EOL> } <EOL> def reil_single_step ( ri , s ) : <EOL> return opcode_map [ ri . opcode ] ( ri , s ) <EOL> _translation_cache = dict ( ) <EOL> _hit_count = dict ( ) <EOL> def fetch_instruction ( s , x86_64 = False ) : <EOL> ip = s . ip <EOL> s . trace . append ( ip ) <EOL> if ip not in _translation_cache : <EOL> bs = [ ] <EOL> for i in range ( <NUM_LIT:0> , <NUM_LIT> ) : <EOL> try : <EOL> bs . append ( s . memory . read_byte ( s , ip + i ) ) <EOL> except IndexError ( ) : <EOL> break <EOL> bs = '<STR_LIT>' . join ( map ( lambda x : chr ( x . value ) , bs ) ) <EOL> for i in x86 . translate ( bs , ip , x86_64 ) : <EOL> _translation_cache [ i . address ] = i <EOL> if ip not in _translation_cache : <EOL> raise InvalidExecution ( s , ip ) <EOL> i = _translation_cache [ ip ] <EOL> s . ip += i . size <EOL> if x86_64 : <EOL> s . registers [ '<STR_LIT>' ] = bv . Constant ( <NUM_LIT:64> , s . ip ) <EOL> return i <EOL> def single_step ( s , x86_64 = False ) : <EOL> i = fetch_instruction ( s , x86_64 ) <EOL> if i is None : <EOL> return [ ] <EOL> if i . address in _hit_count : <EOL> hc = _hit_count [ i . address ] = _hit_count [ i . address ] + <NUM_LIT:1> <EOL> else : <EOL> hc = _hit_count [ i . address ] = <NUM_LIT:1> <EOL> if i . address in s . symbols : <EOL> symbol = s . symbols [ i . address ] <EOL> if s . symbols [ i . address ] in s . function_hooks : <EOL> ss = s . function_hooks [ symbol ] ( s ) <EOL> for s in ss : <EOL> if s . solver . solve_time ( ) > <NUM_LIT:30> : <EOL> s . log . warning ( '<STR_LIT>' , s . solver . solve_time ) <EOL> s . solver . concretise ( ) <EOL> s . clear_il_state ( ) <EOL> return ss <EOL> else : <EOL> s . log . function_call ( None , symbol ) <EOL> s . log . native_instruction ( hc , i , x86_64 ) <EOL> max_il_index = len ( i . il_instructions ) <EOL> states = [ s ] <EOL> exit_states = [ ] <EOL> while len ( states ) > <NUM_LIT:0> : <EOL> s = states . pop ( ) <EOL> if s . il_index >= max_il_index : <EOL> if s . solver . solve_time ( ) > <NUM_LIT:30> : <EOL> s . log . warning ( '<STR_LIT>' . format ( s . solver . solve_time ( ) ) ) <EOL> s . solver . concretise ( ) <EOL> s . clear_il_state ( ) <EOL> exit_states . append ( s ) <EOL> continue <EOL> ri = i . il_instructions [ s . il_index ] <EOL> s . il_index += <NUM_LIT:1> <EOL> s . log . reil_instruction ( ri ) <EOL> states += reil_single_step ( ri , s ) <EOL> return exit_states </s>
