问题

Sure, here's the translated code snippet you provided:

我正在使用 angr 并尝试将输入限制为可打印字符。我使用了如下“众所周知”的方式：

```python
import angr
import claripy

base_addr = 0x800000 
proj = angr.Project("binary", main_opts={'base_addr': base_addr})

flag_chars = [claripy.BVS('%d' % i, 8) for i in range(16)]
flag = claripy.Concat( *flag_chars + [claripy.BVV(b'\n')]) 

state = proj.factory.full_init_state(
        args=['binary'],
        add_options=angr.options.unicorn,
        stdin=flag,
)

for k in flag_chars:
     init_state.solver.add(k <= 0x7f)
     init_state.solver.add(k >= 0x20)

simgr = proj.factory.simulation_manager(state)
find_addr  = 0x807bf5 
avoid_addr = 0x807c55 
simgr.explore(find=find_addr, avoid=avoid_addr)

if (len(simgr.found) > 0):
    for found in simgr.found:
        print(found.posix.dumps(0))

至此，一切都正常。但现在我需要做一些不同的事情：我的输入应该仅限于字母和数字。这显然不会起作用，因为在这个区间内还有其他字符（斜杠、反斜杠、点等）。

我在尝试让这个工作方面感到困难。我尝试了类似以下的东西：

init_state.solver.add(Or(And(k >= ord('A'), k <= ord('Z')), And(k >= ord('a'), k <= ord('z'))))

以及其他几种变化，但没有成功。对此有什么建议吗？

谢谢！

<details>
<summary>英文:</summary>

I&#39;m playing with angr and I&#39;m trying to constraint my input to printable chars. I did it in the &quot;well-known&quot; way like this:

```python
import angr
import claripy

base_addr = 0x800000 
proj = angr.Project(&quot;binary&quot;, main_opts={&#39;base_addr&#39;: base_addr})

flag_chars = [claripy.BVS(&#39;%d&#39; % i, 8) for i in range(16)]
flag = claripy.Concat( *flag_chars + [claripy.BVV(b&#39;\n&#39;)]) 

state = proj.factory.full_init_state(
        args=[&#39;binary&#39;],
        add_options=angr.options.unicorn,
        stdin=flag,
)

for k in flag_chars:
     init_state.solver.add(k &lt;= 0x7f)
     init_state.solver.add(k &gt;= 0x20)

simgr = proj.factory.simulation_manager(state)
find_addr  = 0x807bf5 
avoid_addr = 0x807c55 
simgr.explore(find=find_addr, avoid=avoid_addr)

if (len(simgr.found) &gt; 0):
    for found in simgr.found:
        print(found.posix.dumps(0))

So far, so good, this is working. But now I need to do something different: my input should be constrained only to letters and numbers. This is not going to work obviously, because in this interval we have also other chars (slash, backslash, dot, etc).

I'm struggling in getting this working. I tried something like

init_state.solver.add(Or(And(k >= ord('A'),k <= ord('Z')),And(k >= ord('a'),k <= ord('z'))))

and several other variations, but no luck. Any suggestion on this?

Thanks!

答案1

得分: 0

I found the solution:

  for byte in flag.chop(8):
    initial_state.solver.add(And(byte >= ord('A'), byte <= ord('Z')) | \
                             And(byte >= ord('a'), byte <= ord('z')) )

A small change to the script is required, this:

flag_chars = [claripy.BVS('%d' % i, 8) for i in range(16)]
flag = claripy.Concat( *flag_chars + [claripy.BVV(b'\n')]) 

must be replaced with:

flag = claripy.BVS("flag", 16 * 8)

  for byte in flag.chop(8):
    initial_state.solver.add(And(byte >= ord('A'), byte <= ord('Z')) | \
                             And(byte >= ord('a'), byte <= ord('z')) )

flag_chars = [claripy.BVS('%d' % i, 8) for i in range(16)]
flag = claripy.Concat( *flag_chars + [claripy.BVV(b'\n')]) 

flag = claripy.BVS("flag", 16 * 8)