Angr 操作栈的符号执行 04_angr_symbolic_stack

短命女 2022-09-11 13:28 17阅读 0赞

随机生成的源码：

#include <stdio.h>
    #include <stdlib.h>
    #include <stdint.h>
    #include <string.h>
    
    #define USERDEF0 1127435174
    #define USERDEF1 3502581722
    
    char msg[] = "placeholder\n";
    
    void print_msg() {
        
      printf("%s", msg);
    }
    
    uint32_t complex_function0(uint32_t value) {
        
      value ^= 611337373;value ^= 389713847;value ^= 2674000438;value ^= 3912662653;value ^= 1137673962;value ^= 455195764;value ^= 2453110680;value ^= 1062460266;value ^= 4246336760;value ^= 1324942391;value ^= 1573510015;value ^= 170189229;value ^= 1617668503;value ^= 3672795742;value ^= 3077298468;value ^= 2895552024;value ^= 1586520294;value ^= 2889703051;value ^= 202621568;value ^= 2218210240;value ^= 391099505;value ^= 3790785101;value ^= 583291201;value ^= 3261309589;value ^= 363700575;value ^= 3966842604;value ^= 3130011272;value ^= 2684938037;value ^= 3357819603;value ^= 3251150160;value ^= 2626017393;value ^= 4017044237;
      return value;
    }
    
    uint32_t complex_function1(uint32_t value) {
        
      value ^= 1388253564;value ^= 106836566;value ^= 3880159293;value ^= 2045416916;value ^= 1026501243;value ^= 2494563516;value ^= 112590835;value ^= 2393811250;value ^= 159603376;value ^= 1324653835;value ^= 1691568469;value ^= 1943728476;value ^= 2274061430;value ^= 359326165;value ^= 1976361120;value ^= 1531359048;value ^= 3473336518;value ^= 2524051285;value ^= 3470589958;value ^= 607861481;value ^= 4135383177;value ^= 671779573;value ^= 2685083602;value ^= 3312324601;value ^= 2271234327;value ^= 1556627372;value ^= 321812131;value ^= 2886747042;value ^= 3698677617;value ^= 3787928636;value ^= 795803423;value ^= 1063447371;
      return value;
    }
    
    void handle_user() {
        
      uint32_t user_int0;
      uint32_t user_int1;
      scanf("%u %u", &user_int0, &user_int1);
      user_int0 = complex_function0(user_int0);
      user_int1 = complex_function1(user_int1);
      if ((user_int0 ^ USERDEF0) || (user_int1 ^ USERDEF1)) {
        
        printf("Try again.\n");
      } else {
        
        printf("Good Job.\n");
      }
    }
    
    int main(int argc, char* argv[]) {
        
      //print_msg();
      printf("Enter the password: ");
      handle_user();
    }

Angr不支持多个输入参数，而参数都存入栈中。我们可以跳过输入，直接操作栈，来遍历出想要的结果。那从哪儿开始执行呢？  
![1][]  
此例，可以从scanf输入密码结束之后，把我们的密码注入，也就是sanf的栈注销(`add esp, 10h`)的后面`0x08048697`。  
从IDA汇编看，能计算出padding的大小，也就是所有password的空间大小：创建了0x0C空间大小的栈，去掉push进去的eax空间大小0x4，`0x0C - 0x04 = 0x08`。  
这里我们通过gdb来查看符号执行时，查看padding大小：8字节：  
![1][1 1]  
经过complex\_function0和complex\_function1后，可以看出两个参数值改变了，padding大小也是8字节：  
![1][1 2]

# This challenge will be more challenging than the previous challenges that you
    # have encountered thus far. Since the goal of this CTF is to teach symbolic
    # execution and not how to construct stack frames, these comments will work you
    # through understanding what is on the stack.
    #   ! ! !
    # IMPORTANT: Any addresses in this script aren't necessarily right! Dissassemble
    #            the binary yourself to determine the correct addresses!
    #   ! ! !
    
    import angr
    import claripy
    import sys
    
    def main(argv):
      path_to_binary = argv[1]
      project = angr.Project(path_to_binary)
    
      # For this challenge, we want to begin after the call to scanf. Note that this
      # is in the middle of a function.
      #
      # This challenge requires dealing with the stack, so you have to pay extra
      # careful attention to where you start, otherwise you will enter a condition
      # where the stack is set up incorrectly. In order to determine where after
      # scanf to start, we need to look at the dissassembly of the call and the
      # instruction immediately following it:
      #   sub    $0x4,%esp
      #   lea    -0x10(%ebp),%eax
      #   push   %eax
      #   lea    -0xc(%ebp),%eax
      #   push   %eax
      #   push   $0x80489c3
      #   call   8048370 <__isoc99_scanf@plt>
      #   add    $0x10,%esp
      # Now, the question is: do we start on the instruction immediately following
      # scanf (add $0x10,%esp), or the instruction following that (not shown)?
      # Consider what the 'add $0x10,%esp' is doing. Hint: it has to do with the
      # scanf parameters that are pushed to the stack before calling the function.
      # Given that we are not calling scanf in our Angr simulation, where should we
      # start?
      # (!)
      start_address = 0x08048697
      initial_state = project.factory.blank_state(addr=start_address)
    
      # We are jumping into the middle of a function! Therefore, we need to account
      # for how the function constructs the stack. The second instruction of the
      # function is:
      #   mov    %esp,%ebp
      # At which point it allocates the part of the stack frame we plan to target:
      #   sub    $0x18,%esp
      # Note the value of esp relative to ebp. The space between them is (usually)
      # the stack space. Since esp was decreased by 0x18
      #
      #        /-------- The stack --------\
      # ebp -> |                           |
      #        |---------------------------|
      #        |                           |
      #        |---------------------------|
      #         . . . (total of 0x18 bytes)
      #         . . . Somewhere in here is
      #         . . . the data that stores
      #         . . . the result of scanf.
      # esp -> |                           |
      #        \---------------------------/
      #
      # Since we are starting after scanf, we are skipping this stack construction
      # step. To make up for this, we need to construct the stack ourselves. Let us
      # start by initializing ebp in the exact same way the program does.
      initial_state.regs.ebp = initial_state.regs.esp
    
      # scanf("%u %u") needs to be replaced by injecting two bitvectors. The
      # reason for this is that Angr does not (currently) automatically inject
      # symbols if scanf has more than one input parameter. This means Angr can
      # handle 'scanf("%u")', but not 'scanf("%u %u")'.
      # You can either copy and paste the line below or use a Python list.
      # (!)
      password0 = claripy.BVS('password0', 32)
      password1 = claripy.BVS('password1', 32)
    
      # Here is the hard part. We need to figure out what the stack looks like, at
      # least well enough to inject our symbols where we want them. In order to do
      # that, let's figure out what the parameters of scanf are:
      #   sub    $0x4,%esp
      #   lea    -0x10(%ebp),%eax
      #   push   %eax
      #   lea    -0xc(%ebp),%eax
      #   push   %eax
      #   push   $0x80489c3
      #   call   8048370 <__isoc99_scanf@plt>
      #   add    $0x10,%esp 
      # As you can see, the call to scanf looks like this:
      # scanf(  0x80489c3,   ebp - 0xc,   ebp - 0x10  )
      #      format_string    password0    password1
      #  From this, we can construct our new, more accurate stack diagram:
      #
      #            /-------- The stack --------\
      # ebp ->     |          padding          |
      #            |---------------------------|
      # ebp - 0x01 |       more padding        |
      #            |---------------------------|
      # ebp - 0x02 |     even more padding     |
      #            |---------------------------|
      #                        . . .               <- How much padding? Hint: how
      #            |---------------------------|      many bytes is password0?
      # ebp - 0x0b |   password0, second byte  |
      #            |---------------------------|
      # ebp - 0x0c |   password0, first byte   |
      #            |---------------------------|
      # ebp - 0x0d |   password1, last byte    |
      #            |---------------------------|
      #                        . . .
      #            |---------------------------|
      # ebp - 0x10 |   password1, first byte   |
      #            |---------------------------|
      #                        . . .
      #            |---------------------------|
      # esp ->     |                           |
      #            \---------------------------/
      #
      # Figure out how much space there is and allocate the necessary padding to
      # the stack by decrementing esp before you push the password bitvectors.
      padding_length_in_bytes = 8  # :integer 
      initial_state.regs.esp -= padding_length_in_bytes
    
      # Push the variables to the stack. Make sure to push them in the right order!
      # The syntax for the following function is:
      #
      # initial_state.stack_push(bitvector)
      #
      # This will push the bitvector on the stack, and increment esp the correct
      # amount. You will need to push multiple bitvectors on the stack.
      # (!)
      initial_state.stack_push(password0)  # :bitvector (claripy.BVS, claripy.BVV, claripy.BV)
      initial_state.stack_push(password1)
    
      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]
    
        solution0 = solution_state.se.eval(password0)
        solution1 = solution_state.se.eval(password1)
    
        solution = "Solutions:{} {}".format(solution0, solution1)
        print(solution)
      else:
        raise Exception('Could not find the solution')
    
    if __name__ == '__main__':
      main(sys.argv)

![1][1 3]

[1]: /images/20220828/7f64466e4d094654b8bd93da40c9441c.png
[1 1]: /images/20220828/43745e42c1ee4c62acb1e9c1dd823f5e.png
[1 2]: /images/20220828/462f8ee42bce45b3a354b3f330c23823.png
[1 3]: /images/20220828/5d6a8fb2542f429a93fd7a73f948bd5f.png