angr メモ

筆者：友利奈緒（@K_atc）

インストール

angr 7を前提とする。

apt install

以下パッケージをインストールしないとだめかも。ptpythonインストール前提。

### basic commands
sudo apt install asciinema vim curl wget tmux zsh 
### install build requirements
sudo apt install build-essential libpcap-dev libpcap0.8
### python & pip requrements
sudo apt install python python-pip libffi-dev libncurses5-dev
sudo -H pip install --upgrade pip

install on vanilla python2

angr 6を使っている人は更新した方がいいかも。

sudo -H pip install angr ipdb

### to update angr
sudo -H pip install -U angr

pipインストール推奨パッケージ：

• ptpython：pythonよりも扱いが楽な対話的インタプリタ−

install on pypy (Optional)

### instal pypy
sudo apt install pypy pypy-dev

### install pip
cd /tmp
curl -O https://bootstrap.pypa.io/get-pip.py
sudo -H pypy get-pip.py

### install angr, ipdb
sudo -H pypy -m pip install angr ipdb

実行エラー

ImportError: cannot import name arm

Ubuntu 16.04だと必ず起こるエラー。以下対処方法。

see https://github.com/angr/angr/issues/52

### for python2
sudo -H pip install -I --no-use-wheel capstone
### for pypy
sudo -H pypy -m pip install -I --no-use-wheel capstone

参考情報：angr-dev

公式のインストールスクリプト
https://github.com/angr/angr-dev

angr 7に移行するための情報

• Migrating to angr 7

よく参照するangr-doc

• Options: https://github.com/angr/angr-doc/blob/master/docs/appendices/options.md
• Cheatsheet: https://github.com/angr/angr-doc/blob/master/CHEATSHEET.md
• Speed: https://github.com/angr/angr-doc/blob/master/docs/speed.md
• claripy: https://github.com/angr/angr-doc/blob/master/docs/claripy.md

変数名

これらの頻出の変数名は覚えておくとよい。

proj

project。angr.Projectしたインスタンスの変数に付ける名前。

simgr

Simulation Manager。シンボリック実行における実行ループを管理。

lpg

local path group。各stashを保持。

tpg

thread path group。ThreadingのExplore techniqueで出てくる。

FAQ

すぐに（Round 0で）探索が終了する

事前に与えた制約に矛盾があるせいかも。

angr.manager

angr.manager.l

ipdb> filter(lambda x: not x.startswith('_'), dir(angr.manager.l))
['addFilter', 'addHandler', 'callHandlers', 'critical', 'debug', 'disabled', 'error', 'exception', 'fatal', 'filter', 'filters', 'findCaller', 'getChild', 'getEffectiveLevel', 'handle', 'handlers', 'info', 'isEnabledFor', 'level', 'log', 'makeRecord', 'manager', 'name', 'parent', 'propagate', 'removeFilter', 'removeHandler', 'root', 'setLevel', 'warn', 'warning']

angr.manager.logging

ipdb> filter(lambda x: not x.startswith('_'), dir(angr.manager.logging))
['BASIC_FORMAT', 'BufferingFormatter', 'CRITICAL', 'DEBUG', 'ERROR', 'FATAL', 'FileHandler', 'Filter', 'Filterer', 'Formatter', 'Handler', 'INFO', 'LogRecord', 'Logger', 'LoggerAdapter', 'Manager', 'NOTSET', 'NullHandler', 'PlaceHolder', 'RootLogger', 'StreamHandler', 'WARN', 'WARNING', 'addLevelName', 'atexit', 'basicConfig', 'cStringIO', 'captureWarnings', 'codecs', 'collections', 'critical', 'currentframe', 'debug', 'disable', 'error', 'exception', 'fatal', 'getLevelName', 'getLogger', 'getLoggerClass', 'info', 'log', 'logMultiprocessing', 'logProcesses', 'logThreads', 'makeLogRecord', 'os', 'raiseExceptions', 'root', 'setLoggerClass', 'shutdown', 'sys', 'thread', 'threading', 'time', 'traceback', 'warn', 'warning', 'warnings', 'weakref']

デバッグログをファイルに保存する

以下のコードを冒頭に加えると、angr.logというファイルに、上書き（'w'）でログが書き込まれるようになる。追記がよかったらmodeを'a'にすること。

angr.manager.l.setLevel("DEBUG")
logging = angr.manager.logging
log_handler = logging.FileHandler("angr.log", mode='w')
log_handler.setLevel(logging.DEBUG)
log_handler.setFormatter(logging.Formatter('%(levelname)-7s | %(asctime)-23s | %(name)-8s | %(message)s'))
angr.manager.l.addHandler(log_handler)

フォーマット

https://github.com/angr/angr/blob/5c53804fa972f93418fea3f21877854ca18df6ad/angr/misc/loggers.py#L11

self.handler.setFormatter(logging.Formatter('%(levelname)-7s | %(asctime)-23s | %(name)-8s | %(message)s'))

SimProcedure

ipdb> angr.SIM_PROCEDURES.keys()
['msvcr', 'ntdll', 'uclibc', 'libc', 'stubs', 'testing', 'win32', 'win_user32', 'linux_loader', 'cgc', 'posix', 'linux_kernel', 'glibc']
ipdb> angr.SIM_PROCEDURES['libc'].keys()
['strncmp', 'rand', 'malloc', 'sscanf', 'snprintf', 'vsnprintf', 'fgetc', 'realloc', 'fread', 'fclose', 'strcat', 'abort', 'fprintf', 'printf', 'fgets', 'fflush', 'fopen', 'feof', 'strncpy', 'getchar', 'strchr', 'fputc', 'puts', 'fwrite', 'scanf', 'fseek', 'system', 'fputs', 'ftell', 'exit', 'sprintf', 'putc', 'memcmp', 'srand', 'strtol', 'memset', 'FormatParser', 'rewind', 'free', 'atoi', 'calloc', 'putchar', 'strlen', 'memcpy', 'perror', 'strstr', 'strcpy', 'tmpnam', 'ungetc', 'strcmp', 'setvbuf']

proj.loader

proj.loader.find_symbol

属性一覧
dir(proj.loader.find_symbol('main'))
['TYPE_FUNCTION', 'TYPE_NONE', 'TYPE_OBJECT', 'TYPE_OTHER', 'TYPE_SECTION', '__class__', '__delattr__', '__dict__', '__doc__', '__format__', '__getattribute__', '__hash__', '__init__', '__module__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__str__', '__subclasshook__', '__weakref__', 'addr', 'binding', 'demangled_name', 'elftype', 'is_common', 'is_export', 'is_extern', 'is_forward', 'is_function', 'is_import', 'is_static', 'is_weak', 'linked_addr', 'name', 'owner_obj', 'rebased_addr', 'relative_addr', 'resolve', 'resolve_forwarder', 'resolved', 'resolvedby', 'section', 'size', 'type', 'warned_addr']

アドレス解決された値を得る

find, avoidにはこちらのアドレスを与える。ラッパー関数を用意すると楽。

rebased_addr = lambda x: proj.loader.find_symbol(x).rebased_addr

使用例）

find, avoid = [], []
find += [rebased_addr('check_passed')]

相対アドレスを得る

ディスアセンブラで表示される方のアドレスを得るならこっち。ラッパー関数を用意すると楽。

relative_addr = lambda x: proj.loader.find_symbol(x).relative_addr

proj.loader.memory

ipdb> dir(proj.loader.memory)
['__class__', '__contains__', '__delattr__', '__dict__', '__doc__', '__format__', '__getattribute__', '__getitem__', '__getstate__', '__hash__', '__init__', '__iter__', '__module__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__setitem__', '__setstate__', '__str__', '__subclasshook__', '__weakref__', '_arch', '_backers', '_cbackers', '_flatten_to_c', '_needs_flattening', '_needs_flattening_personal', '_pointer', '_root', '_stride_repr', '_updates', 'add_backer', 'cbackers', 'get_byte', 'read', 'read_addr_at', 'read_bytes', 'read_bytes_c', 'remove_backer', 'seek', 'stride_repr', 'tell', 'update_backer', 'write_addr_at', 'write_bytes', 'write_bytes_to_backer']

Simulation Manager

https://github.com/angr/angr/blob/master/angr/manager.py
angr/manager.py → Anger Managerのつもり?

シンボリック実行エンジンのコア。Simulation Manager（simgr）は実行状態を管理する。下図はangrの実行ループを表している。

stashについて

Simulation Managerにおいて各探索パスの実行状態を状態別に管理するための配列。

simgr に与えられた初期状態は、 active stash に格納される。active stash は実行可能な状態が格納されるデータ構造である。初期化が終わると、ラウンドと呼ばれる、 active stash から状態を取り出し、個々の状態が指す命令を実行し、状態を更新し、 stash に戻す処理を行う。更新された状態は、状態に応じて active stash の他に、探索成功を意味づけられた状態が入る found stash、探索を中断させた状態が入る avoid stash、実行時エラーが起きた状態が入る errored stash にふるい分けられる。

simgr.explore

find, avoidをベースにした探索戦略。

TODO

find/avoid

TODO

filter_func

simgr.explore(find=[], step_func=lambda x: x.stash(from_stash='errored', to_stash='found', filter_func=explore_filter))

ログから判断すると state を errored stash から found stash に移動できないように見える。

simger.step

痒いところに手が届く良い探索戦略。angrを使い倒すときはこちらがよい。

simgr.step(step_func=your_step_func, until=lambda lpg: len(lpg.errored) > 0)

until

注意：ラムダ式を与える！間違えてbool値に評価されるものを入れないようにする！TypeErrorで落ちて原因をつかむのに時間がかかる。

find/avoid

simgr.stepを使うとexploreのように引数でfind/avoidを与えることができない。以下のようなstep_funcを用意するとよい。

def step_func(lpg):
    global find, avoid
    if find is not []:
        lpg.stash(filter_func=lambda path: path.addr in find, from_stash='active', to_stash='found')
    if avoid is not []:
        lpg.stash(filter_func=lambda path: path.addr in avoid, from_stash='active', to_stash='avoid')
    # lpg.drop(stash='avoid') # memory usage optimization
    return lpg

simgr.step(step_func=step_func, until=lambda x: len(x.found) > 0) 

Claripy

z3ベースの制約ソルバー。

API

https://github.com/angr/angr-doc/blob/master/docs/claripy.md

例

BVSで遊ぶ

0バイト目は下位1バイトの位置。

>>> x = claripy.BVS('x', 32)

>>> x
<BV32 x_0_32>

>>> s = claripy.Solver()

>>> s.add(claripy.Extract(7, 0, x) == 0x41)
(<Bool x_0_32[7:0] == 65>,)

>>> s.eval(x, 4) # 与制約を満たす具体値を４つ得る
(3393L, 1345L, 321L, 65L)

state

state.regs

実際にはユーザーが使っても効果ないAPIがある。annotateとか。

print filter(lambda x: not x.startswith('_'), dir(state.regs.r0))

['Concat', 'Extract', 'FULL_SIMPLIFY', 'LITE_SIMPLIFY', 'LShR', 'SDiv', 'SGE', 'SGT', 'SLE', 'SLT', 'SMod', 'UGE', 'UGT', 'ULE', 'ULT', 'UNSIMPLIFIED', 'ana_load', 'ana_store', 'ana_uuid', 'annotate', 'annotations', 'append_annotation', 'append_annotations', 'args', 'cache_key', 'canonicalize', 'cardinality', 'chop', 'concat', 'concrete', 'dbg_is_looped', 'dbg_repr', 'depth', 'get_byte', 'get_bytes', 'insert_annotation', 'insert_annotations', 'intersection', 'ite_burrowed', 'ite_excavated', 'length', 'make_like', 'make_uuid', 'model', 'multivalued', 'op', 'raw_to_bv', 'raw_to_fp', 'recursive_children_asts', 'recursive_leaf_asts', 'remove_annotation', 'remove_annotations', 'replace', 'replace_annotations', 'replace_dict', 'reversed', 'shallow_repr', 'sign_extend', 'simplifiable', 'singlevalued', 'size', 'split', 'structurally_match', 'swap_args', 'symbolic', 'to_bv', 'to_literal', 'uc_alloc_depth', 'uninitialized', 'union', 'uuid', 'val_to_fp', 'variables', 'widen', 'zero_extend']

### シンボリックかを判定
ipdb> state.regs.r0.symbolic
True

state.arch

### arm 32bits
ipdb> state.arch.name
'ARMEL'
### intel 64bits
ipdb> state.arch
<Arch AMD64 (LE)>
ipdb> state.arch.name
'AMD64'

dir(state)

stateの属性一覧。

print filter(lambda x: not x.startswith('_'), dir(state))

['actions', 'add_constraints', 'addr', 'addr_trace', 'ana_load', 'ana_store', 'ana_uuid', 'arch', 'block', 'cgc', 'copy', 'dbg_print_stack', 'downsize', 'events', 'gdb', 'get_plugin', 'globals', 'guards', 'has_plugin', 'history', 'history_iterator', 'inspect', 'ip', 'ip_constraints', 'jumpkind', 'jumpkinds', 'last_actions', 'length', 'libc', 'log', 'make_concrete_int', 'make_uuid', 'mem', 'mem_concrete', 'memory', 'merge', 'mode', 'options', 'os_name', 'plugins', 'posix', 'prepare_callsite', 'project', 'reachable', 'reg_concrete', 'register_plugin', 'registers', 'regs', 'release_plugin', 'satisfiable', 'scratch', 'se', 'set_mode', 'simplify', 'solver', 'stack_pop', 'stack_push', 'stack_read', 'state', 'step', 'targets', 'thumb', 'to_literal', 'trace', 'trim_history', 'uc_manager', 'unicorn', 'uninitialized_access_handler', 'widen', 'with_condition']

simgr.found[0]

属性一覧
['actions', 'add_constraints', 'addr', 'addr_trace', 'ana_load', 'ana_store', 'ana_uuid', 'arch', 'block', 'cgc', 'copy', 'dbg_print_stack', 'downsize', 'events', 'gdb', 'get_plugin', 'globals', 'guards', 'has_plugin', 'history', 'history_iterator', 'inspect', 'ip', 'ip_constraints', 'jumpkind', 'jumpkinds', 'last_actions', 'length', 'libc', 'log', 'make_concrete_int', 'make_uuid', 'mem', 'mem_concrete', 'memory', 'merge', 'mode', 'options', 'os_name', 'plugins', 'posix', 'prepare_callsite', 'project', 'reachable', 'reg_concrete', 'register_plugin', 'registers', 'regs', 'release_plugin', 'satisfiable', 'scratch', 'se', 'set_mode', 'simplify', 'solver', 'stack_pop', 'stack_push', 'stack_read', 'state', 'step', 'targets', 'thumb', 'to_literal', 'trace', 'trim_history', 'uc_manager', 'unicorn', 'uninitialized_access_handler', 'widen', 'with_condition']

simgr.deadended[0]

属性一覧

['actions', 'add_constraints', 'addr', 'addr_trace', 'ana_load', 'ana_store', 'ana_uuid', 'arch', 'block', 'cgc', 'copy', 'dbg_print_stack', 'downsize', 'events', 'gdb', 'get_plugin', 'globals', 'guards', 'has_plugin', 'history', 'history_iterator', 'inspect', 'ip', 'ip_constraints', 'jumpkind', 'jumpkinds', 'last_actions', 'length', 'libc', 'log', 'make_concrete_int', 'make_uuid', 'mem', 'mem_concrete', 'memory', 'merge', 'mode', 'options', 'os_name', 'plugins', 'posix', 'prepare_callsite', 'project', 'reachable', 'reg_concrete', 'register_plugin', 'registers', 'regs', 'release_plugin', 'satisfiable', 'scratch', 'se', 'set_mode', 'simplify', 'solver', 'stack_pop', 'stack_push', 'stack_read', 'state', 'step', 'targets', 'thumb', 'to_literal', 'trace', 'trim_history', 'uc_manager', 'unicorn', 'uninitialized_access_handler', 'widen', 'with_condition']

simgr.errored[0]

属性一覧

['debug', 'error', 'state', 'traceback']

errored.error

print "error: %r" % (errored.error)
for k, v in vars(errored.error).items():
    print "\t%s: %r" % (k, v)

error: SimSegfaultException(0x609060 (read-miss, original <BV64 0x609060>)
    addr: 6328416L
    bbl_addr: 4196067L
    original_addr: <BV64 0x609060>
    reason: 'read-miss'
    ins_addr: 4196090L
    executed_instruction_count: 5
    guard: <Bool True>
    stmt_idx: 28

errored.state

print "state: %s" % (errored.state)
for k, v in vars(errored.state).items():
    if k == "plugins":
        print "\t%s:" % (k)
        for k2, v2 in v.items(): # type of errored.state.plugins is dictinary
            print "\t\t%s: %r" % (k2, v2)
    else:
        print "\t%s: %r" % (k, v)

state: <SimState @ 0x4006e3>
    _special_memory_filler: None
    os_name: 'Linux'
    ip_constraints: []
    _global_condition: None
    _satisfiable: True
    project: <Project ./segv>
    mode: 'symbolic'
    plugins:
        callstack: <CallStack (depth 3)>
        solver_engine: <angr.state_plugins.solver.SimSolver object at 0x7f870c75f7d0>
        mem: <SimMemView>
        scratch: <angr.state_plugins.scratch.SimStateScratch object at 0x7f870c75f850>
        regs: <angr.state_plugins.view.SimRegNameView object at 0x7f870c75f890>
        libc: <angr.state_plugins.libc.SimStateLibc object at 0x7f870c75f8d0>
        registers: <angr.state_plugins.symbolic_memory.SimSymbolicMemory object at 0x7f870c75f950>
        posix: <angr.state_plugins.posix.SimStateSystem object at 0x7f870c75fbd0>
        memory: <angr.state_plugins.symbolic_memory.SimSymbolicMemory object at 0x7f870c75fc50>
        inspector: <angr.state_plugins.inspect.SimInspector object at 0x7f870c75fc90>
        history: <StateHistory @ 0x4006e3>
    arch: <Arch AMD64 (LE)>
    options: set(['TRACK_CONSTRAINT_ACTIONS', 'SIMPLIFY_REGISTER_WRITES', 'DO_STORES', 'DO_GETS', 'SYMBOLIC', 'TRACK_CONSTRAINTS', 'EXTENDED_IROP_SUPPORT', 'COMPOSITE_SOLVER', 'OPTIMIZE_IR', 'DO_PUTS', 'SIMPLIFY_MEMORY_WRITES', 'COW_STATES', 'SYMBOLIC_INITIAL_VALUES', 'SUPPORT_FLOATING_POINT', 'DO_OPS', 'DO_LOADS', 'DO_CCALLS', 'TRACK_MEMORY_MAPPING', 'STRICT_PAGE_ACCESS'])
    uninitialized_access_handler: None

error.state.plugins

dict型。

errored.state.plugins['solver_engine'].eval(argv1, cast_to=str)

errored.traceback

ipdb> dir(errored.traceback)
['__class__', '__delattr__', '__doc__', '__format__', '__getattribute__', '__hash__', '__init__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__sizeof__', '__str__', '__subclasshook__', 'tb_frame', 'tb_lasti', 'tb_lineno', 'tb_next']

state.se

claripyと同等。なのでmainの引数をシンボル化しないときはimport claripyしなくても事足る。

https://github.com/angr/angr-doc/blob/master/MIGRATION.md#changes-to-the-solver-interface

We cleaned up the menagerie of functions present on state.solver (if you're still referring to it as state.se you should stop) and simplified it into a cleaner interface

seはstate engineの略？

state.se.BVS, state.se.BVV

シンボル変数の作成。BVはZ3のBit Vectorと同じ。なので第二引数はビット単位。

symvar_x = state.se.BVS('x', 2 * 8)

BVの属性

dir(symvar_BV)
['Concat', 'Extract', 'FULL_SIMPLIFY', 'LITE_SIMPLIFY', 'LShR', 'SDiv', 'SGE', 'SGT', 'SLE', 'SLT', 'SMod', 'UGE', 'UGT', 'ULE', 'ULT', 'UNSIMPLIFIED', '__a_init__', '__abs__', '__add__', '__and__', '__class__', '__delattr__', '__dict__', '__div__', '__divmod__', '__doc__', '__eq__', '__floordiv__', '__format__', '__ge__', '__getattr__', '__getattribute__', '__getitem__', '__gt__', '__hash__', '__init__', '__invert__', '__iter__', '__le__', '__len__', '__lshift__', '__lt__', '__mod__', '__module__', '__mul__', '__ne__', '__neg__', '__new__', '__nonzero__', '__or__', '__pos__', '__pow__', '__radd__', '__rand__', '__rdiv__', '__rdivmod__', '__reduce__', '__reduce_ex__', '__repr__', '__rfloordiv__', '__rlshift__', '__rmod__', '__rmul__', '__ror__', '__rpow__', '__rrshift__', '__rshift__', '__rsub__', '__rtruediv__', '__rxor__', '__setattr__', '__slots__', '__str__', '__sub__', '__subclasshook__', '__truediv__', '__weakref__', '__xor__', '_all_slots', '_ana_getliteral', '_ana_getstate', '_ana_setstate', '_ana_uuid', '_any_to_literal', '_apply_to_annotations', '_burrow_ite', '_burrowed', '_cache_key', '_calc_hash', '_check_replaceability', '_depth', '_eager_backends', '_errored', '_excavate_ite', '_excavated', '_first_backend', '_from_BVV', '_from_int', '_from_long', '_from_str', '_get_hashables', '_hash', '_hash_cache', '_identify_vars', '_recursive_leaf_asts', '_relocatable_annotations', '_rename', '_replace', '_self_to_literal', '_simplified', '_stored', '_type_name', '_uc_alloc_depth', '_uneliminatable_annotations', '_uninitialized', 'ana_load', 'ana_store', 'ana_uuid', 'annotate', 'annotations', 'append_annotation', 'append_annotations', 'args', 'cache_key', 'canonicalize', 'cardinality', 'chop', 'concat', 'concrete', 'dbg_is_looped', 'dbg_repr', 'depth', 'get_byte', 'get_bytes', 'insert_annotation', 'insert_annotations', 'intersection', 'ite_burrowed', 'ite_excavated', 'length', 'make_like', 'make_uuid', 'model', 'multivalued', 'op', 'raw_to_bv', 'raw_to_fp', 'recursive_children_asts', 'recursive_leaf_asts', 'remove_annotation', 'remove_annotations', 'replace', 'replace_annotations', 'replace_dict', 'reversed', 'shallow_repr', 'sign_extend', 'simplifiable', 'singlevalued', 'size', 'split', 'structurally_match', 'swap_args', 'symbolic', 'to_bv', 'to_literal', 'uc_alloc_depth', 'uninitialized', 'union', 'uuid', 'val_to_fp', 'variables', 'widen', 'zero_extend']

シンボル／コンクリートかの判定

symvar_BV.symbolic # => bool
symvar_BV.concrete # => bool

コンクリート化

デフォルトの返り値はlong型。

ipdb> state.se.any_int(symvar_BV)
Deprecation warning: Use eval() instead of any_int
128L
ipdb> state.se.eval(symvar_BV)
128L
ipdb> state.se.any_str(symvar_BV)
Deprecation warning: Use eval(expr, cast_to=str) instead of any_str
'\x00\x80'
ipdb> state.se.eval(symvar_BV, cast_to=str)
'\x00\x80'
ipdb> state.solver.eval(symvar_BV, cast_to=str)
'\x00\x80'

state.se.Extract

angr-doc非掲載API。

### Extract(end, start, BV)
### extracts {x | start <= x <= end}
state.se.Extract(32 * 2 + 15, 32 * 2 + 8, payload)

エンディアン変換

Extractで出てくるバイト列はビッグエンディアンなので、エンディアンの変換関数があると混乱しない。

Extract = lambda x: state.se.Extract(x)
BigEndian = lambda x: state.se.Reverse(x)
LittleEndian = lambda x: x

使用例：

state.add_constraints(LittleEndian(Extract(8 * 4 - 1, 8 * 0, symvar_pbuf_payload)) == 0x80810000)

state.se.Reverse

angr-doc非掲載API。

バイトオーダーをひっくり返す。state.memory.store前のエンディアンの変換に便利。

state.se.constraints

配列。なので引数不要。

使用例：

constraint_expr = simgr.errored[0].state.plugins['solver_engine'].constraints
for s in simgr.active:
    s.add_constraints(s.se.Or(*[s.se.Not(x) for x in constraint_expr]))

state.solver

state.solverに同じ。state.seを使うのをやめよう！

https://github.com/angr/angr/blob/master/angr/state_plugins/solver.py

### 充足可能性の判定
### @return     bool
def satisfiable(self, extra_constraints=(), exact=None):

state.solver.add

制約を追加

https://github.com/angr/angr-doc/blob/master/docs/claripy.md

ipdb> state.solver.satisfiable([state.regs.r0 == 0])
False
ipdb> state.solver.satisfiable([state.regs.r0 != 0])
True

state.se.Andとか使えばいいかな？

state.solver.add vs. state.add_constraints

機能は同じだと思う。

state.solver.eval

BV変数をコンクリート化する。

ret_long_int = state.solver.eval(state.memory.load(addr, 0x8))
ret_bytes = state.solver.eval(state.memory.load(addr, 0x100), case_to=bytes)

case_toで文字列に変換するときにodd-lengthで例外吐くことがあるのでラッパー関数を用意するとよい。

import hexdump ### needs `pip install hexdump`
def memory_dump(begin, length):
    ret = ""
    for i in range(0, length):
        val = found.solver.eval(state.memory.load(begin + i, 1))
        ret += chr(val)
    return ret
hexdump.hexdump(v)

state.memory

ipdb> dir(state.memory)
['STRONGREF_STATE', '_CONCRETIZATION_STRATEGIES', '_SAFE_CONCRETIZATION_STRATEGIES', '__class__', '__contains__', '__delattr__', '__dict__', '__doc__', '__format__', '__getattribute__', '__getstate__', '__hash__', '__init__', '__module__', '__new__', '__reduce__', '__reduce_ex__', '__repr__', '__setattr__', '__str__', '__subclasshook__', '__weakref__', '_abstract_backer', '_apply_concretization_strategies', '_changes_to_merge', '_constrain_underconstrained_index', '_convert_to_ast', '_copy_contents', '_create_default_read_strategies', '_create_default_write_strategies', '_fill_missing', '_find', '_generic_region_map', '_is_uninitialized', '_load', '_maximum_concrete_size', '_maximum_symbolic_size', '_maximum_symbolic_size_approx', '_merge', '_merge_strategies', '_merge_values', '_read_address_range', '_read_address_range_approx', '_read_from', '_resolve_location_name', '_resolve_size_range', '_stack_region_map', '_store', '_store_cases', '_store_with_merge', '_temp_generic_region_map', '_temp_stack_region_map', '_write_address_range', '_write_address_range_approx', 'addrs_for_hash', 'addrs_for_name', 'category', 'changed_bytes', 'concrete_parts', 'concretize_read_addr', 'concretize_write_addr', 'copy', 'copy_contents', 'dbg_print', 'endness', 'find', 'get_unconstrained_bytes', 'id', 'init_state', 'load', 'make_symbolic', 'map_region', 'mem', 'memory_objects_for_hash', 'memory_objects_for_name', 'merge', 'normalize_address', 'permissions', 'read_strategies', 'register_default', 'replace_all', 'replace_memory_object', 'set_stack_address_mapping', 'set_state', 'set_strongref_state', 'stack_id', 'state', 'store', 'store_cases', 'unconstrain_byte', 'unconstrain_differences', 'unmap_region', 'unset_stack_address_mapping', 'was_written_to', 'widen', 'write_strategies']

state.memory.load

第一引数は読み込み元のアドレス。第二引数は読み込むバイト数。

state.memory.store

第一引数がBVのときは第二引数で長さを指定しなくてもよい。
勝手にリトルエンディアンで格納するので要注意。

定数値を入れる時はstate.memの方が安全。エンディアンを気にしたい時は、

state.memory.store(addr, state.se.BVV(0x114514, 64)) # store 0x114514 with Big endian
state.memory.store(addr, state.se.Reverse(state.se.BVV(0x114514, 64))) # store 0x114514 with Little endian

エンディアンの注意点

state.se.BVVとstate.se.BVSの内部表現はビッグエンディアン。memory.storeは対象番地にリトルエンディアンで書き込む。storeの第二引数を数値で直書きしても、内部ではビッグエンディアンで、それをリトルエンディアンで書き込む挙動をするので注意。

state.memory.store(buf_ptr, buf, 8) # store memory with BIG endian

リトルエンディアンで確実に数値を書き込みたかったら、state.memを使うとよい。64ビットでの挙動が怪しい場面に直面した。怖い。

buf_ptr = 0x200000
state.mem[buf_ptr].qword = 0x114514 # 無言の死を遂げる？
state.mem[buf_ptr].uint64_t = 0x114514 # 無言の死を遂げる？
state.mem[buf_ptr].uint64_t = 0x114514
state.mem[buf_ptr].dword = 0x114514

または、

state.memory.store(buf_ptr, state.se.Reverse(buf), 0x100) 

state.memory.mem

state.memory.mem.map_region

state.memory.mem.map_region(MY_SYMVAR_REGION_BEGIN, MY_SYMVAR_REGION_LENGTH, 0b111) # begin, len, permissions (exec, read, write)

http://angr.io/api-doc/angr.html#angr.storage.paged_memory.BasePage

permissions (claripy.AST) – A 3-bit bitvector setting specific permissions for EXEC, READ, and WRITE

state.inspect

state.inspect.b

メモリのリードアクセス前にフックを追加。

new_state.inspect.b('mem_read', when=angr.BP_AFTER, action=debug_funcRead)
def debug_funcRead(state):
    print 'Read', state.inspect.mem_read_expr, 'from', state.inspect.mem_read_address

dir(state.inspect)

ipdb> filter(lambda x: not x.startswith('_'), dir(state.inspect))
['BP_AFTER', 'BP_BEFORE', 'BP_BOTH', 'STRONGREF_STATE', 'action', 'add', 'add_breakpoint', 'added_constraints', 'address', 'address_concretization_action', 'address_concretization_add_constraints', 'address_concretization_expr', 'address_concretization_memory', 'address_concretization_result', 'address_concretization_strategy', 'b', 'backtrace', 'clear', 'copy', 'difference', 'difference_update', 'discard', 'downsize', 'exit_guard', 'exit_jumpkind', 'exit_target', 'expr', 'function_address', 'init_state', 'instruction', 'intersection', 'intersection_update', 'isdisjoint', 'issubset', 'issuperset', 'make_breakpoint', 'mem_read_address', 'mem_read_expr', 'mem_read_length', 'mem_write_address', 'mem_write_expr', 'mem_write_length', 'merge', 'pop', 'reg_read_expr', 'reg_read_length', 'reg_read_offset', 'reg_write_expr', 'reg_write_length', 'reg_write_offset', 'register_default', 'remove', 'remove_breakpoint', 'set_state', 'set_strongref_state', 'sim_engine', 'sim_successors', 'simprocedure', 'simprocedure_addr', 'simprocedure_name', 'state', 'statement', 'symbolic_expr', 'symbolic_name', 'symbolic_size', 'symmetric_difference', 'symmetric_difference_update', 'syscall_name', 'tmp_read_expr', 'tmp_read_num', 'tmp_write_expr', 'tmp_write_num', 'union', 'update', 'widen']

state.mem

https://github.com/angr/angr/blob/6d88622e3e8825083d55ac0e15a4ae304fc2b0e2/angr/state_plugins/view.py#L82
数値でのアクセスはこれを使うのが楽。返り値を比較できない（state.add_constraintの文脈でも不可っぽい）謎仕様なので使いみちがあまりない。

state.mem[addr].uint64_t # => <BV ...>
state.mem[addr].uint64_t.concrete # => long int

NOTE: uint, intの打ち間違いに注意！

angr.exploration_techniques

探索アルゴリズムをカスタマイズすることができる。標準で用意されているテクニックを使うのが楽。

DFS

https://github.com/angr/angr/blob/master/angr/exploration_techniques/dfs.py

simgr.use_technique(angr.exploration_techniques.DFS())

深さ優先探索（Depth First Search?）を行う。デフォルトは幅優先探索。

activeが空になったときに探索を終了してしまう不都合な挙動をするので、以下のようにstep_funcをうまく実装しないとだめ。

def step_func(lpg):
    global find, avoid
    if find is not []:
        lpg.stash(filter_func=lambda path: path.addr in find, from_stash='active', to_stash='found')
    lpg.stash(filter_func=lambda path: path.addr in avoid, from_stash='active', to_stash='avoid')

    lpg.drop(stash='avoid') # memory usage optimization

    # print "[*] len(lpg.active) = %d, len(lpg.deferred) = %d" % (len(lpg.active), len(lpg.deferred))
    if len(lpg.active) == 0 and len(lpg.deferred) > 0:
        lpg.active.append(lpg.deferred.pop())
    return lpg

Threading

https://github.com/angr/angr/blob/master/angr/exploration_techniques/threading.py

simgr.use_technique(angr.exploration_techniques.Threading())

冒頭で import している current.features は並列実行用のPython標準モジュール。
非並列で実行したときに解が求まる事前制約を与えると、Threadingのときは解が求まらないっぽい？