angr 添加约束条件

约束求解

在 angr 中提供了可以用加入一个约束条件到一个 state 中的方法（state.solver.add），将每一个符号化的布尔值作为一个关于符号变量合法性的断言。之后可以通过使用 state.solver.eval(symbol) 对各个断言进行评测来求出一个合法的符号值（若有多个合法值，返回其中的一个）。简单来说就是通过 .add 对 state 对象添加约束，并使用 .eval 接口求解，得到符号变量的可行解

import angr  
import sys  
import claripy  
  
  
def Go():  
    path_to_binary = "./08_angr_constraints"  
    project = angr.Project(path_to_binary, auto_load_libs=False)  
  
    start_address = 0x8048625  
    buff_addr = 0x0804A050  
    address_to_check_constraint = 0x08048565  
  
    initial_state = project.factory.blank_state(addr=start_address)  
  
    char_size_in_bits = 8  
    passwd_len = 16  
    passwd0 = claripy.BVS('passwd0', char_size_in_bits * passwd_len)  
    initial_state.memory.store(buff_addr, passwd0)  
  
    simulation = project.factory.simgr(initial_state)  
    simulation.explore(find=address_to_check_constraint)  
  
    if simulation.found:  
        solution_state = simulation.found[0]  
        constrained_parameter_address = buff_addr  
        constrained_parameter_size_bytes = 16  
        constrained_parameter_bitvector = solution_state.memory.load(  
            constrained_parameter_address,  
            constrained_parameter_size_bytes  
        )  
        constrained_parameter_desired_value = 'AUPDNNPROEZRJWKB'  
        solution_state.solver.add(constrained_parameter_bitvector == constrained_parameter_desired_value)  
        solution0 = solution_state.solver.eval(passwd0, cast_to=bytes)  
        print("[+] Success! Solution is: {0}".format(solution0))  
    else:  
        raise Exception('Could not find the solution')  
  
  
if __name__ == "__main__":  
    Go()