@@ -161,12 +161,6 @@ def initial_state(self, *, symbolic_rcx: bool = True, rcx_value: int = 0) -> Tra
161161 return TraceState (regs , mem )
162162
163163 def trace_handler (self , addr : int , state : TraceState ) -> list [TraceOutcome ]:
164- if addr == 0x14001606A :
165- return self ._trace_binaryshield_push_reg64 (state )
166- if addr == 0x140016126 :
167- return self ._trace_binaryshield_pop_reg32 (state )
168- if addr == 0x14001676B :
169- return self ._trace_binaryshield_jcc (state )
170164 with create_context () as context :
171165 types = context .types
172166 with context .create_module (f"trace_{ addr :x} " ) as module :
@@ -255,137 +249,6 @@ def reg_ptr(reg_name: str) -> Value:
255249
256250 return self ._read_outcomes (resolver , sem , result_ty , ram , state )
257251
258- def _trace_binaryshield_push_reg64 (self , state : TraceState ) -> list [TraceOutcome ]:
259- r13 = state .regs .get ("r13" )
260- r14 = state .regs .get ("r14" )
261- r15 = state .regs .get ("r15" )
262- rsp = state .regs .get ("rsp" )
263- if (
264- r13 is None
265- or r14 is None
266- or r15 is None
267- or rsp is None
268- or not r13 .is_concrete
269- or not r14 .is_concrete
270- or not r15 .is_concrete
271- or not rsp .is_concrete
272- ):
273- return [TraceOutcome ("unresolved" , None , state )]
274-
275- reg_index = self .container .get_data (r13 .value or 0 , 1 )[0 ]
276- source_addr = (rsp .value or 0 ) + reg_index * 8
277- value_bytes = [state .mem .get (source_addr + i , AbsValue .concrete (8 , 0 )) for i in range (8 )]
278- new_r15 = (r15 .value or 0 ) - 8
279- post_mem = dict (state .mem )
280- for i , byte in enumerate (value_bytes ):
281- post_mem [new_r15 + i ] = byte
282-
283- next_ptr = (r13 .value or 0 ) + 1
284- target , post_r13 = self ._dispatch_from_bytecode (next_ptr , r14 .value or 0 )
285- post_regs = dict (state .regs )
286- post_regs ["rax" ] = AbsValue .concrete (64 , target )
287- post_regs ["r13" ] = AbsValue .concrete (64 , post_r13 )
288- post_regs ["r15" ] = AbsValue .concrete (64 , new_r15 )
289- return [TraceOutcome ("jmp" , target , TraceState (post_regs , post_mem ))]
290-
291- def _trace_binaryshield_pop_reg32 (self , state : TraceState ) -> list [TraceOutcome ]:
292- r13 = state .regs .get ("r13" )
293- r14 = state .regs .get ("r14" )
294- r15 = state .regs .get ("r15" )
295- rsp = state .regs .get ("rsp" )
296- if (
297- r13 is None
298- or r14 is None
299- or r15 is None
300- or rsp is None
301- or not r13 .is_concrete
302- or not r14 .is_concrete
303- or not r15 .is_concrete
304- or not rsp .is_concrete
305- ):
306- return [TraceOutcome ("unresolved" , None , state )]
307-
308- reg_index = self .container .get_data (r13 .value or 0 , 1 )[0 ]
309- dest_addr = (rsp .value or 0 ) + reg_index * 8
310- value_bytes = [state .mem .get ((r15 .value or 0 ) + i , AbsValue .concrete (8 , 0 )) for i in range (4 )]
311- post_mem = dict (state .mem )
312- for i , byte in enumerate (value_bytes ):
313- post_mem [dest_addr + i ] = byte
314-
315- next_ptr = (r13 .value or 0 ) + 1
316- target , post_r13 = self ._dispatch_from_bytecode (next_ptr , r14 .value or 0 )
317- post_regs = dict (state .regs )
318- post_regs ["rax" ] = AbsValue .concrete (64 , target )
319- post_regs ["r13" ] = AbsValue .concrete (64 , post_r13 )
320- post_regs ["r15" ] = AbsValue .concrete (64 , (r15 .value or 0 ) + 4 )
321- loaded = self ._bytes_to_concrete (value_bytes )
322- post_regs ["rbx" ] = (
323- AbsValue .concrete (64 , loaded )
324- if loaded is not None
325- else self .namer .new ("rbx_pop32" , 64 )
326- )
327- return [TraceOutcome ("jmp" , target , TraceState (post_regs , post_mem ))]
328-
329- def _bytes_to_concrete (self , values : list [AbsValue ]) -> int | None :
330- result = 0
331- for i , value in enumerate (values ):
332- if not value .is_concrete :
333- return None
334- result |= (value .value or 0 ) << (8 * i )
335- return result
336-
337- def _dispatch_from_bytecode (self , ptr : int , image_base : int ) -> tuple [int , int ]:
338- target_rva = int .from_bytes (self .container .get_data (ptr , 4 ), "little" )
339- return image_base + target_rva , ptr + 4
340-
341- def _trace_binaryshield_jcc (self , state : TraceState ) -> list [TraceOutcome ]:
342- r13 = state .regs .get ("r13" )
343- r14 = state .regs .get ("r14" )
344- r15 = state .regs .get ("r15" )
345- if (
346- r13 is None
347- or r14 is None
348- or r15 is None
349- or not r13 .is_concrete
350- or not r14 .is_concrete
351- or not r15 .is_concrete
352- ):
353- return [TraceOutcome ("unresolved" , None , state )]
354-
355- branch_rva = int .from_bytes (self .container .get_data (r13 .value or 0 , 4 ), "little" )
356- fallthrough_ptr = (r13 .value or 0 ) + 4
357- branch_ptr = (r14 .value or 0 ) + branch_rva
358-
359- flags_value = self ._read_tracked_int (state .mem , r15 .value or 0 , 64 )
360- if flags_value is None :
361- selected = [branch_ptr , fallthrough_ptr ]
362- else :
363- zf = (flags_value >> 6 ) & 1
364- selected = [branch_ptr if zf == 0 else fallthrough_ptr ]
365-
366- outcomes : list [TraceOutcome ] = []
367- for selected_ptr in selected :
368- target , post_r13 = self ._dispatch_from_bytecode (selected_ptr , r14 .value or 0 )
369- post_regs = dict (state .regs )
370- post_regs ["rax" ] = AbsValue .concrete (64 , target )
371- post_regs ["r13" ] = AbsValue .concrete (64 , post_r13 )
372- post_regs ["r15" ] = AbsValue .concrete (64 , (r15 .value or 0 ) + 8 )
373- post_regs ["cf" ] = AbsValue .concrete (8 , 0 )
374- post_regs ["zf" ] = AbsValue .concrete (8 , 0 )
375- post_regs ["sf" ] = AbsValue .concrete (8 , 0 )
376- post_regs ["of" ] = AbsValue .concrete (8 , 0 )
377- outcomes .append (TraceOutcome ("jmp" , target , TraceState (post_regs , dict (state .mem ))))
378- return outcomes
379-
380- def _read_tracked_int (self , mem : dict [int , AbsValue ], addr : int , width : int ) -> int | None :
381- value = 0
382- for i in range (width // 8 ):
383- byte = mem .get (addr + i , AbsValue .concrete (8 , 0 ))
384- if not byte .is_concrete :
385- return None
386- value |= (byte .value or 0 ) << (8 * i )
387- return value
388-
389252 def _materialize_abs_value (self , types , abs_value : AbsValue , param : Value | None ) -> Value :
390253 ty = types .int_n (abs_value .width )
391254 if abs_value .is_concrete :
0 commit comments