angr学习与angr_CTF题解（持续更新）

angr基础知识

介绍

angr 是一个支持多处理架构的用于二进制文件分析的工具包，它提供了动态符号执行的能力以及多种静态分析的能力。它可以被使用者扩展，用于自动化逆向工程、漏洞挖掘等多个方面

安装

1. 安装 angr

$sudo pip install angr

2. 安装 angr-utils

$mkdir angr-dev
$cd angr-dev
$git clone https://github.com/axt/bingraphvis
$pip install -e ./bingraphvis
$git clone https://github.com/axt/angr-utils
$pip install -e ./angr-utils

用法

project

project 类是 angr 的主类，也是angr的开始，通过初始化 project 类加载二进制文件

import angr
p = angr.Project('file_path')

其他可选参数

名称	描述	示例
auto_load_libs	是否自动加载程序的依赖（少加载无关结果的库可以提升angr效率）	auto_load_libs　= False
skip_libs	希望避免加载的库	skip_libs = 库名
except_missing_libs	无法解析库时是否抛出异常	True / False
force_load_libs	强制加载的库	force_load_libs = 库名
ld_path	共享库的优先搜索路径	ld_path = 路径名

project 类的方法和属性：

• p.arch : 文件架构

• hex(p.entry) ： 程序入口点

• p.filename ： 加载的文件名

• p.arch.bits ： 字长（32位 / 64位）

• p.arch.memory_endness ： 大小端

factory

project只是加载二进制文件，实际是对simstate对象操作

simstate对象是程序的状态，包含运行时的一切信息，例如寄存器、内存值、文件系统、符号变量

创建状态

state = p.factory.entry_state()

预设状态：

前两个比较常用，blank_state用于跳过一些极大降低angr效率的指令，初始时rax的数据类型都是bit vector

预设状态方式	描述
entry_state	初始化状态为程序运行到程序入口点处的状态
blank_state(addr=)	大多数数据都没有初始化，状态中下一条指令为addr处的指令
full_init_state	共享库和预定义内容已经加载完毕，例如刚加载完共享库
call_state	准备调用函数的状态

factory 类的方法：

• state.regs.rax

simgr

simulation manager（SM）模拟管理器，要分析程序就要让它到达下一个状态

使用 simgr 创建 sm， 需要传入 state 或 state的列表

simgr = p.factory.simgr(state)

sm 有许多被成为 stash 的列表，保存了处于某种状态的 state

stash 是一个列表，可以用 python 方式遍历，angr 也提供了获取方式：stash 名字前加上 one_ 得到第一个状态，加上 mp_ 得到一个 mulpyplexed 版本的stash，例如simgr.one_active

stash	描述
active （默认值）	保存接下来可以执行并且将要执行的状态
deadended	由于某些原因不能继续执行的状态，例如没有合法指令，或者有非法指针
pruned	与 solve 的策略有关，当发现一个不可解的节点后，其后面所有的节点都优化掉放在 pruned 里
unconstrained	如果创建 SM 时启用了 save_unconstrained，则被认定为不受约束的 state 会放在这，不受约束的 state 是指由用户数据或符号控制的指令指针（例如eip）
unsat	如果创建SM时启用了save_unsat，则被认为不可满足的 state 会放在这里

simgr 类的方法：

• 使用 move() 转移state，将 fulter_func 筛选出来的 state 从 from_stash 转移到 to_stash

  state.posix.dumps(0)：到达当前状态对应的程序输入

  state.posix.dumps(1)：到达当前状态对应的程序输出

  #从 'deadended' 状态堆栈中，筛选出那些标准输出中包含字符串 '100' 的状态，并将这些状态移动到 'more_then_50' 状态堆栈中，匿名函数的参数是 s
  simgr.move(from_stash='deadended', to_stash='more_then_50', filter_func=lambda s: '100' in s.posix.dumps(1))

• 使用 step() 方法使处于 active 的 state 执行一个基本块，不会改变 state 本身

  simgr.step()

explorer

用于探索模拟状态直到找到特定条件满足的状态的方法，有 find（目标指令的地址或地址列表） 和 avoid（避免的指令地址或地址列表） 两种参数，找到符合的 find 状态会保存在 simger.found 列表中，可遍历元素获取状态

import angr
project = angr.Project('path_to_binary')
simgr = project.factory.simulation_manager()

find_address = 0x4017c0
avoid_address = 0x401230

simgr.explore(find=find_address, avoid=avoid_address)

if simgr.found:
    solution_state = simgr.found[0]
   #打印出符号条件的状态的输入    
    print(solution_state.posix.dumps(0))

eval

• solver.eval(expression) 将会解出一个可行解
• solver.eval_one(expression)将会给出一个表达式的可行解，若有多个可行解，则抛出异常。
• solver.eval_upto(expression, n)将会给出最多n个可行解，如果不足n个就给出所有的可行解。
• solver.eval_exact(expression, n)将会给出n个可行解，如果解的个数不等于n个，将会抛出异常。
• solver.min(expression)将会给出最小可行解
• solver.max(expression)将会给出最大可行解

符号执行

符号执行就是给程序传递一个符号而不是具体的值

遇到分支时 angr 会保存所有分支以及分支后的所有分支，在分支时保存进入该分支时的判断条件，通常判断条件是对符号的约束

当 angr 运行到目标状态可以调用求解器对一路上收集到的约束求解，最终得到某个符号能够到达当前状态的值

angr 的 state 属性都是状态插件，包括 memory 、regs 、 men 、registers 、solver等，用于控制仿真程序看到的环境，包括如何从环境中引入符号数据

寄存器符号化

跳过输入定位到输入之后，直接改变寄存器，将 state 传入 simgr，solution_state.solver.eval(arg1)获取得到的值，可控制多个寄存器

位向量：BVV(value, size) BVS(name, size)

import angr
import sys
import claripy

project = angr.Project('file_path')
initial_state = project.factory.blank_state(addr=start)

#创建位向量
passwd = claripy.BVS('passwd', 32)
initial_state.regs.eax = passwd

simgr = project.factory.simulation_manager(initial_state)

if simgr.found:
    solution_state = simgr.found[0]
    print(hex(solution_state.solver.eval(arg1)))

栈中的值符号化

通过计算构造，例如 arg1 -> ebp - 0xc; arg2 -> ebp - 0x10

则构造esp = ebp， esp - 0x8， 两个参数入栈（stack_push）

initial_state_regs.ebp = initial_state.regs.esp
arg1 = charipy.BVS('arg1', 32)
arg2 = charipy.BVS('arg2', 32)
initial_state.regs.esp -= 8
initial_state.stack_push(arg1)
initial_state.stack_push(arg2)

内存符号化

initial_state.memory.store(passwd0_address, passwd0)

以字节类型输出

print(solution_state.solver.eval(arg1, cast_to=bytes))

动态内存符号化

由于 angr 并没有真正 运行 二进制文件而只是在模拟运行状态，因此它实际上不需要将内存分配到堆中，实际上可以伪造任何地址，所以将伪造的地址存放到 bss 段的地址中模拟题目的情况即可

initial_state.memory.store(pointer_to_malloc_memory_address0, fake_heap_address0, endness=project.arch.memory_endness)

endness 设置端序，可以直接 project.arch.memory_endness 获取程序端序

LE – 小端序(little endian, least significant byte is stored at lowest address)
BE – 大端序(big endian, most significant byte is stored at lowest address)
ME – 中间序(Middle-endian. Yep.)

文件内容符号化

仿真文件系统并插入文件，blank_state 从打开文件部分地址开始

symbolic_file_size_bytes 是文件中的内容长度，passwd_file 是实际读出的长度

#形成符号化的文件格式
passwd_file = angr.storage.SimFile(filename, content=passwd0, size=symbolic_file_size_bytes)
initial_state.fs.insert(filename, passwd_file)

添加约束条件

在实际的测试生产中符号执行技术存在约束求解问题和路径爆炸问题，当程序存在循环结构的时候即使是简单逻辑也可能产生规模巨大的执行路径导致路径爆炸，所以需要提供更多的约束控制路径爆炸问题

约束求解

用字符串直接比较约束取代循环判断函数， angr 提供加入约束条件的方法 state.solver.add ，将每个符号化的布尔值作为一个关于符号变量合法性的断言

示例

>>> state.solver.add(x - y >= 4)
>>> state.solver.add(y > 0)
>>> state.solver.eval(x)
5
>>> state.solver.eval(y)
1

用法：expolre 的 find 地址设置为比较函数的地址，load 的 size 设置为字符串长度，不需要 * 8

#从地址中加载值
res = solution_state.memory.load(addr, size)
#加入限制：加载值等于固定值
solution_state.solver.add(res == 'AUPDNNPROEZRJWKB')

hook

可以使用 hook 直接改写函数，hook engine 是 angr 使用的引擎 SimEngine 的子类，默认情况下用 SimProcedures 中的符号摘要替换库函数设置 hooking，可以通过 angr.procedures 或 angr.SimProcedures 查看列表

SimProcedure 就是 hook 机制，可以通过 project.hook(addr, hook) 设置，其中 hook 是一个 SimProcedure 实例，通过 .is_hooked / .unhook / .hook_py 进行管理，将 project.hook(addr) 作为函数装饰器可以编写自己的 hook 函数，还可以通过 project.hook_symbol(name, hook) hook 函数

用法：一参是需要 hook 的调用函数的地址，二参是调用函数 call func 到下一条指令之间的长度，函数参数是 state

>>> @project.hook(0x1234, length=5)
... def set_rax(state):
...     state.regs.rax = 1

返回值用 claripy.BVV(value, size) ，例如：

state.regs.eax = claripy.If(
            user_input_string == check_against_string, 
            claripy.BVV(1, size), 
            claripy.BVV(0, size)
        )

利用函数名hook

在函数被多次调用的时候利用函数名 hook 而不需要使用函数调用地址

每个程序都有一个符号表，angr 可以使用 Project.hook_symbol 解析出每个导入符号的地址，用自己的代码替换函数

用法：project.hook_symbol 一参是函数名，二参是自定义的类，类参数是 angr.SimProcedure，类中定义 run 函数的一参是 self，其他参数可以直接用参数的参数，例如这里 check_equals_symbol 函数有参数 to_check 和 length，加载内存的 state 用 self.state，最后不需要设置 rax 直接 return 即可

class ReplacementCheckEquals(angr.SimProcedure):
        def run(self, to_check, length):
            user_input_buffer_address = to_check
            user_input_buffer_length = length
            user_input_string = self.state.memory.load(
                user_input_buffer_address,
                user_input_buffer_length
            )
            check_against_string = 'ORSDDWXHZURJRBDH'
            return claripy.If(
                user_input_string == check_against_string, 
                claripy.BVV(1, 32), 
                claripy.BVV(0, 32)
            )
    
    check_equals_symbol = 'check_equals_ORSDDWXHZURJRBDH'
    project.hook_symbol(check_equals_symbol, ReplacementCheckEquals())

hook scanf应对复杂输入

用法：调用带有全局状态的 globals 插件，保存对符号值的引用

class func(angr.SimProcedure):
    def run(self, format_string, param0, param1):
        arg1 = claripy.BVS('arg1', 32)
        arg2 = claripy.BVS('arg2', 32)

        self.state.memory.store(param0, arg1, endness = 'LE')
        self.state.memory.store(param1, arg2, endness = 'LE')

        self.state.globals['solutions'] = (arg1, arg2)

project.hook_symbol('__isoc99_scanf', func())

...

if simgr.found:
    solution_state = simgr.found[0]
    stored_solutions = solution_state.globals['solutions']
    scanf0_solution = solution_state.solver.eval(stored_solutions[0])
    scanf1_solution = solution_state.solver.eval(stored_solutions[1])
    print(scanf0_solution)
    print(scanf1_solution)

angr_ctf 题解

项目地址：https://github.com/jakespringer/angr_ctf

00_angr_find

目标地址是输出good job，输出能够到达目标地址的第一个输入

import angr
project = angr.Project('./00_angr_find')
simgr = project.factory.simulation_manager()

find_address = 0x8048675
avoid_address = 0x8048666

simgr.explore(find=find_address, avoid=avoid_address)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.posix.dumps(0))
#JXWVXRKX

01_angr_avoid

有很多分支会调用 avoid_me 函数，放到 avoid 参数里

import angr
project = angr.Project('./01_angr_avoid')
simgr = project.factory.simulation_manager()

find_address = 0x80485E0
avoid_address = 0x80485A8

simgr.explore(find=find_address, avoid=avoid_address)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.posix.dumps(0))
#HUJOZMYS

02_angr_find_condition

程序中出现多次 Try again 和 Good job，避免记录所有的 Good job地址，将对两种情况的判断写成函数作为 find 和 avoid 的参数

import angr
project = angr.Project('./02_angr_find_condition')
simgr = project.factory.simulation_manager()

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.posix.dumps(0))
    
#HETOBRCU

03_angr_symbolic_registers

本题使用 scanf 输入了三个十六进制数，angr 对 scanf 的复杂输入处理的不是很好，

__isoc99_scanf("%x %x %x", &v1, &v2, v3);

而输入后的参数会传递给寄存器 eax ebx edx

.text:08048937                 mov     ecx, [ebp+var_18]
.text:0804893A                 mov     eax, ecx
.text:0804893C                 mov     ecx, [ebp+var_14]
.text:0804893F                 mov     ebx, ecx
.text:08048941                 mov     ecx, [ebp+var_10]

输入函数返回后通过这三个寄存器传递给栈

.text:0804897B                 call    get_user_input
.text:08048980                 mov     [ebp+var_14], eax
.text:08048983                 mov     [ebp+var_10], ebx
.text:08048986                 mov     [ebp+var_C], edx

所以可以将三个寄存器符号化注入，从传递寄存器参数给栈的位置开始执行，避开 scanf 输入

import angr
import sys
import claripy

project = angr.Project('./03_angr_symbolic_registers')
initial_state = project.factory.blank_state(addr=0x8048980)

arg1 = claripy.BVS('arg1', 32)
arg2 = claripy.BVS('arg2', 32)
arg3 = claripy.BVS('arg3', 32)

initial_state.regs.eax = arg1
initial_state.regs.ebx = arg2
initial_state.regs.edx = arg3

simgr = project.factory.simulation_manager(initial_state)
#simgr = project.factory.simgr(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    print(hex(solution_state.solver.eval(arg1)))
    print(hex(solution_state.solver.eval(arg2)))
    print(hex(solution_state.solver.eval(arg3)))
#0xb9ffd04e
#0xccf63fe8
#0x8fd4d959

04_angr_symbolic_stack

栈符号化，不能直接使用regs，通过计算构造esp和ebp在合适的位置 stack_push 入栈

import angr
import sys
import claripy

project = angr.Project('./04_angr_symbolic_stack')
initial_state = project.factory.blank_state(addr=0x8048697)

arg1 = claripy.BVS('arg1', 32)
arg2 = claripy.BVS('arg2', 32)

initial_state.regs.esp = initial_state.regs.ebp
initial_state.regs.esp -= 8

initial_state.stack_push(arg1)
initial_state.stack_push(arg2)

simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.solver.eval(arg1))
    print(solution_state.solver.eval(arg2))
    
#1704280884
#2382341151

05_angr_symbolic_memory

主要是用到initial_state.memory.store(addr, arg)，将指定位置的变量符号化

%8s -> 8 字符，一个字符 8 字节，所以长度是 64

import angr
import sys
import claripy

project = angr.Project('./05_angr_symbolic_memory')
initial_state = project.factory.blank_state(addr=0x8048601)

arg1 = claripy.BVS('arg1', 64)
arg2 = claripy.BVS('arg2', 64)
arg3 = claripy.BVS('arg3', 64)
arg4 = claripy.BVS('arg4', 64)
addr = 0xA1BA1C0

initial_state.memory.store(addr, arg1)
initial_state.memory.store(addr + 0x8, arg2)
initial_state.memory.store(addr + 0x10, arg3)
initial_state.memory.store(addr + 0x18, arg4)

simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.solver.eval(arg1, cast_to=bytes))
    print(solution_state.solver.eval(arg2, cast_to=bytes))
    print(solution_state.solver.eval(arg3, cast_to=bytes))
    print(solution_state.solver.eval(arg4, cast_to=bytes))
#b'NAXTHGNR'
#b'JVSFTPWE'
#b'LMGAUHWC'
#b'XMDCPALU'

06_angr_symbolic_dynamic_memory

动态内存符号化， malloc 创建的地址未知，直接随便设置一个地址作为堆地址即可，堆地址存储在 bss 段的一个地址中，所以给 bss 段的变量一个自定义地址，往自定义地址里写输入位向量

import angr
import sys
import claripy

project = angr.Project('./06_angr_symbolic_dynamic_memory')
initial_state = project.factory.blank_state(addr=0x8048699)

arg1 = claripy.BVS('arg1', 64)
arg2 = claripy.BVS('arg2', 64)
addr1 = 0xABCC8A4
addr2 = 0xABCC8AC
heap_ptr1 = 0x12340
heap_ptr2 = 0x12350

initial_state.memory.store(addr1, heap_ptr1, endness = 'LE')
initial_state.memory.store(addr2, heap_ptr2, endness = 'LE')
initial_state.memory.store(heap_ptr1, arg1)
initial_state.memory.store(heap_ptr2, arg2)

simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.solver.eval(arg1, cast_to=bytes))
    print(solution_state.solver.eval(arg2, cast_to=bytes))
#b'UBDKLMBV'
#b'UNOERNYS'

07_angr_symbolic_file

%64s 64字符，每个字符 8 字节，长度是 8 * 64

从文件中读字符串进行对比，需要将文件内容符号化进行仿真文件系统，并且插入这个文件

blank_state 的起始地址是从 open 开始

import angr
import sys
import claripy

project = angr.Project('./07_angr_symbolic_file')
initial_state = project.factory.blank_state(addr=0x80488ED)

arg1 = claripy.BVS('arg1', 64 * 8)

passwd_file = angr.storage.SimFile('OJKSQYDP.txt', content=arg1, size=64)
initial_state.fs.insert('OJKSQYDP.txt', passwd_file)

simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.solver.eval(arg1, cast_to=bytes))
#b'AZOMMMZM\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x04\x80\x08\x00\x00\x00\x00\x01\x00\x00\x00\x10\x01\x00\x00\x00\x04@\x01\x01\x01\x08\x80 \x00\x00\x10\x00\x00\x04\x01\x00\x00\x00\x00'

08_angr_constraints

比较函数使用了循环造成路径爆炸，直接 explore 运行到比较函数，通过添加约束来模拟比较过程而不实际执行比较过程

import angr
import sys
import claripy

project = angr.Project('./08_angr_constraints')
initial_state = project.factory.blank_state(addr=0x8048625)

arg1 = claripy.BVS('arg1', 16 * 8)

initial_state.memory.store(0x804A050, arg1)
simgr = project.factory.simulation_manager(initial_state)

simgr.explore(find=0x8048565)

if simgr.found:
    solution_state = simgr.found[0]

    res = solution_state.memory.load(0x804A050, 16)
    solution_state.solver.add(res == 'AUPDNNPROEZRJWKB')

    print(solution_state.solver.eval(arg1, cast_to=bytes))
#b'LGCRCDGJHYUNGUJB'

09_angr_hooks

写 hook 函数，程序的 scanf 不复杂，直接从头开始，hook 函数中获取输入值与固定值进行比较，程序中比较函数的逻辑是比较成功就返回 1 失败返回 0 ，这里也是同理成功就用位向量 BVV 表示返回 1，hook 的起始是 call 比较函数的地址，长度是 call 指令与下一条指令的距离

import angr
import sys
import claripy

project = angr.Project('./09_angr_hooks')
initial_state = project.factory.entry_state()

@project.hook(0x80486B3, length=5)
def func(state):
    res = state.memory.load(0x804A054, 16)
    state.regs.eax = claripy.If(res == 'XYMKBKUHNIQYNQXE', claripy.BVV(1, 32), claripy.BVV(0, 32))

simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.posix.dumps(0))
#ZXIDRXEORJOTFFJNWUFAOUBLOGLQCCGK

10_angr_simprocedures

判断函数调用了很多次，所以不能直接通过设置地址来 hook，而需要通过函数名来 hook，也就是使用 hook_symbol 通过函数名 hook 到类中的 run 函数，run 一参是 self，其他参数可以直接用判断函数的参数，加载地址也需要用 self.state

import angr
import sys
import claripy

project = angr.Project('./10_angr_simprocedures')
initial_state = project.factory.entry_state()

class func(angr.SimProcedure):
    def run(self, a1, a2):
        res = self.state.memory.load(a1, a2)
        return claripy.If(res == 'ORSDDWXHZURJRBDH', claripy.BVV(1, 32), claripy.BVV(0, 32))

project.hook_symbol('check_equals_ORSDDWXHZURJRBDH', func())

simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    print(solution_state.posix.dumps(0))
#MSWKNJNAVTTOZMRY

11_angr_sim_scanf

hook scanf函数来应对复杂格式的输入，向scanf的参数中存入内容，并且将值存到 globals 全局变量插件中

import angr
import sys
import claripy

project = angr.Project('./11_angr_sim_scanf')
initial_state = project.factory.entry_state()

class func(angr.SimProcedure):
    def run(self, format_string, param0, param1):
        arg1 = claripy.BVS('arg1', 32)
        arg2 = claripy.BVS('arg2', 32)

        self.state.memory.store(param0, arg1, endness = 'LE')
        self.state.memory.store(param1, arg2, endness = 'LE')

        self.state.globals['solutions'] = (arg1, arg2)

project.hook_symbol('__isoc99_scanf', func())

simgr = project.factory.simulation_manager(initial_state)

def right(state):
    if b'Good' in state.posix.dumps(1):
        return True
    else:
        return False

def wrong(state):
    if b'Try' in state.posix.dumps(1):
        return True
    else:
        return False

simgr.explore(find=right, avoid=wrong)

if simgr.found:
    solution_state = simgr.found[0]
    stored_solutions = solution_state.globals['solutions']
    scanf0_solution = solution_state.solver.eval(stored_solutions[0])
    scanf1_solution = solution_state.solver.eval(stored_solutions[1])
    print(scanf0_solution)
    print(scanf1_solution)
#1448564819
#1398294103