Блог

Я пытаюсь использовать angr для проверки поведения функции путем получения правильного ввода для заданного результата. Функция изменяет буфер, в этом случае она просто копирует в него входные данные, поэтому я настраиваю символьные переменные в куче, к которым применяю ограничение равенства. Затем я создаю символьную переменную для ввода в функцию. Я намеревался сделать так, чтобы angr по существу запускал функцию до тех пор, пока входные данные не будут найдены таким образом, чтобы при их копировании в буфер они удовлетворяли наложенному на них ограничению. Однако, когда он запускается, я получаю только одну заблокированную ветвь, где вывод имеет правильное значение, а ввод-нет. Я прикрепил решатель и исходный код тестовой программы ниже. Является ли это провалом моей реализации? Или такой подход к решению проблемы недействителен

решатель

 import angr import claripy import angr.sim_type as T  if __name__ == '__main__':  path = './test'  target = 'test_fn'   target_buf = 'buffer'     word = b'hello'    program = angr.Project(path)  fn = program.loader.find_symbol(target)  buf = program.loader.find_symbol(target_buf)   fn_addr = fn.rebased_addr  buf_addr = buf.rebased_addr   cc = program.factory.cc(func_ty=T.SimTypeFunction(  args=[T.parse_type('char*')],  returnty=T.parse_type('void')  ))   str_in = claripy.BVS('input', 8 * len(word))  fn_call_state = program.factory.call_state(fn_addr, angr.calling_conventions.PointerWrapper(str_in), cc=cc)  ptr_out = fn_call_state.heap.allocate(len(word))   chars = []  for i, v in enumerate(word):  ch = claripy.BVS('char_{}'.format(i), 8)  chars.append(ch)  fn_call_state.solver.add(ch == int(v))  word_sym = claripy.Concat(*chars)  fn_call_state.memory.store(buf_addr, ptr_out)  fn_call_state.memory.store(ptr_out, word_sym)   simgr = program.factory.simgr(fn_call_state, save_unsat=True)  simgr.run()  print(simgr)  for s in simgr.deadended:  print(s.solver.eval(str_in, cast_to=bytes))  print(s.solver.eval(word_sym, cast_to=bytes))   

программа тестирования

 #include lt;string.hgt; #include lt;stdlib.hgt; #include lt;stdio.hgt;  char* buffer;  void test_fn(char* input) {  strcpy(buffer, input);  return; }  int main(int argc, char** argv) {  buffer = (char*) malloc(100);  test_fn("hello"); }   

когда я запускаю решатель, я получаю вывод, подобный следующему, хотя первое значение, входное значение, изменяется, по-видимому, случайным образом. ЕСТЬ ли способ применить это ограничение, чтобы побочные эффекты программы имели приоритет? Я не понимаю, как эти две ценности могут отличаться. Является ли это ошибкой в том, как я готовлю память?

 b'x01x01x01x04x01x02' b'hellox00'