Threading error in z3

[ocean1]

The following scriptto solve level 6 of the CMU binary bomb causes a segfault in z3 when using more than one thread.
z3 should be thread safe unless the Context object is shared between threads.

import angr
import logging
import claripy
import simuvex
from struct import unpack
from IPython import embed
from ipdb import set_trace

stored_ints_addr = 0
bvs = None


class custom_hook(simuvex.SimProcedure):

    def run(self, s1_addr, int_addr):
        print "read_six_numbers hook"
        global stored_ints_addr
        global bvs
        for i in range(6):
            bvs = self.state.se.BVS(
                "int{}".format(i), 8 * 4, explicit_name=True)
            self.state.add_constraints(bvs >= 1, bvs < 6)
            self.state.memory.store(int_addr + i * 4, bvs,
                                    endness=self.state.arch.memory_endness)
            # let's keep this for later
            stored_ints_addr = int_addr

            return self.state.se.BVV(6, self.state.arch.bits)


def solve_flag_6():

    start = 0x4010f4
    read_num = 0x40145c
    find = 0x4011f7
    avoid = (0x4011e9, 0x401140, 0x401123,)

    p = angr.Project("./bomb", load_options={'auto_load_libs': False})
    p.hook(read_num, custom_hook)
    state = p.factory.blank_state(
        addr=start, remove_options={simuvex.o.LAZY_SOLVES})
    pg = p.factory.path_group(state, threads=4)
    pg.explore(find=find, avoid=avoid)
    found = pg.found[0].state
    set_trace()

    return unpack('IIIIII', found.se.any_str(found.memory.load(stored_ints_addr, 24)))


def main():
    print("Flag 6:" + str(solve_flag_6()))

if __name__ == '__main__':
    # logging.getLogger('angr.path_group').setLevel(logging.DEBUG)
    main()

[zardus]

Dam... Z3's Python wrappers sometime do a poor job with making sure the context gets passed around properly. This might be one of those times. I'll try to check it out...

…

On Dec 21, 2016 8:24 PM, "ocean" ***@***.***> wrote: The following script causes a segfault in z3 when using more than one thread. z3 should be thread safe unless the Context object is shared between threads. import angr import logging import claripy import simuvex from struct import unpack from IPython import embed from ipdb import set_trace stored_ints_addr = 0 bvs = None class custom_hook(simuvex.SimProcedure): def run(self, s1_addr, int_addr): print "read_six_numbers hook" global stored_ints_addr global bvs for i in range(6): bvs = self.state.se.BVS( "int{}".format(i), 8 * 4, explicit_name=True) self.state.add_constraints(bvs >= 1, bvs < 6) self.state.memory.store(int_addr + i * 4, bvs, endness=self.state.arch.memory_endness) # let's keep this for later stored_ints_addr = int_addr return self.state.se.BVV(6, self.state.arch.bits) def solve_flag_6(): start = 0x4010f4 read_num = 0x40145c find = 0x4011f7 avoid = (0x4011e9, 0x401140, 0x401123,) p = angr.Project("./bomb", load_options={'auto_load_libs': False}) p.hook(read_num, custom_hook) state = p.factory.blank_state( addr=start, remove_options={simuvex.o.LAZY_SOLVES}) pg = p.factory.path_group(state, threads=4) pg.explore(find=find, avoid=avoid) found = pg.found[0].state set_trace() return unpack('IIIIII', found.se.any_str(found.memory.load(stored_ints_addr, 24))) def main(): print("Flag 6:" + str(solve_flag_6())) if __name__ == '__main__': # logging.getLogger('angr.path_group').setLevel(logging.DEBUG) main() — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#30>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ADSzlymyQdLhk2GOAYxe_xQ4k1_ualvqks5rKfuLgaJpZM4LToO0> .

[github-actions]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions]

This issue has been closed due to inactivity.