Angr 内存符号化 05_angr_symbolic_memory

以你之姓@ 2022-09-12 01:46 19阅读 0赞

# 说明 #

通过查看下面的源码或IDA汇编，可知此例需要输入4个输入字符串，给每个输入字符串赋值给了user\_input数组这块已经开辟的内存空间，我们可以监测user\_input在内存中的值来获取最终的答案。

# 随机生成的源码 #

#include <stdio.h>
    #include <stdlib.h>
    #include <string.h>
    #define USERDEF "YZJGNZSQCRTECQLVJKDHBYEFALOWJXHE"
    
    char padding0[ 59499168 ];
    char user_input[32+1];
    char padding1[ 21264468 ];
    
    char msg[] = "placeholder\n";
    
    void print_msg() {
        
      printf("%s", msg);
    }
    
    int complex_function(int value, int i) {
        
    #define LAMBDA 9
      if (!('A' <= value && value <= 'Z')) {
        
        printf("Try again.\n");
        exit(1);
      }
      return ((value - 'A' + (LAMBDA * i)) % ('Z' - 'A' + 1)) + 'A';
    }
    
    int main(int argc, char* argv[]) {
        
      memset(user_input, 0, sizeof(user_input));
    
      //print_msg();
      printf("Enter the password: ");
      scanf("%8s %8s %8s %8s", user_input, &user_input[8], &user_input[16], &user_input[24]);
    
      for (int i=0; i<32; ++i) {
        
        user_input[i] = (char) complex_function(user_input[i], i);
      }
    
      if (strncmp(user_input, USERDEF, 32)) {
        
        printf("Try again.\n");
      } else {
        
        printf("Good Job.\n");
      }
    }

# IDA查看地址 #

![1][]  
`scanf`的8s表示字符串长度为8，每个字符2个字节，一共`8*2*4=64`个字节。

# pwndbg查看内存数据 #

![1][1 1]

这里测试用的输入字符串是：`aaaaaaaa bbbbbbbb cccccccc dddddddd`，一共32个字符，每个字符2字节，一共64字节。  
每个字符串包含8个字符，每个字符8位，所以设置BVS时，第2个参数为`8*8=64`。

# Angr exp #

import angr
    import claripy
    import sys
    
    def main(argv):
      path_to_binary = argv[1]
      project = angr.Project(path_to_binary)
    
      start_address = 0x08048601
      initial_state = project.factory.blank_state(addr=start_address)
    
      # The binary is calling scanf("%8s %8s %8s %8s").
      # (!)
      password0 = claripy.BVS('password0', 64)
      password1 = claripy.BVS('password1', 64)
      password2 = claripy.BVS('password2', 64)
      password3 = claripy.BVS('password3', 64)
    
      # Determine the address of the global variable to which scanf writes the user
      # input. The function 'initial_state.memory.store(address, value)' will write
      # 'value' (a bitvector) to 'address' (a memory location, as an integer.) The
      # 'address' parameter can also be a bitvector (and can be symbolic!).
      # (!)
      password0_address = 0x0A1BA1C0
      initial_state.memory.store(password0_address, password0)
      password1_address = 0x0A1BA1C8
      initial_state.memory.store(password1_address, password1)
      password2_address = 0x0A1BA1D0
      initial_state.memory.store(password2_address, password2)
      password3_address = 0x0A1BA1D8
      initial_state.memory.store(password3_address, password3)
    
      simulation = project.factory.simgr(initial_state)
    
      def is_successful(state):
        stdout_output = state.posix.dumps(sys.stdout.fileno())
        return b'Good Job' in stdout_output
    
      def should_abort(state):
        stdout_output = state.posix.dumps(sys.stdout.fileno())
        return b'Try again' in stdout_output
    
      simulation.explore(find=is_successful, avoid=should_abort)
    
      if simulation.found:
        solution_state = simulation.found[0]
    
        # Solve for the symbolic values. We are trying to solve for a string.
        # Therefore, we will use eval, with named parameter cast_to=str
        # which returns a string instead of an integer.
        # (!)
        solution0 = solution_state.solver.eval(password0,cast_to=bytes).decode('utf-8')
        solution1 = solution_state.solver.eval(password1,cast_to=bytes).decode('utf-8')
        solution2 = solution_state.solver.eval(password2, cast_to=bytes).decode('utf-8')
        solution3 = solution_state.solver.eval(password3, cast_to=bytes).decode('utf-8')
        solution = "Solution:{} {} {} {}".format(solution0, solution1, solution2, solution3)
    
        print(solution)
      else:
        raise Exception('Could not find the solution')
    
    if __name__ == '__main__':
      main(sys.argv)

# 结果 #

![1][1 2]

[1]: /images/20220828/6258577721b94c17ba6e636b8401748e.png
[1 1]: /images/20220828/747b9b61769c43f8bec0f7352836f9da.png
[1 2]: /images/20220828/5c124644d2b248f4a933cfcb920e568c.png