Angr与Claripy：如何为输入设置字母数字非连续约束？

• 补全约束条件：你之前的代码只覆盖了大小写字母，未包含数字的约束，这是核心问题之一。完整的字母数字约束需要同时包含三个分支：大写字母、小写字母、数字，代码应修改为：

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

• 确认约束的目标变量：确保k是单个字节的字符变量，比如从符号化输入中提取的单个字符位（input_sym.chars[i]）。如果直接用整个符号化输入变量，约束会作用于整个多字节值而非每个字符，自然无法生效。

• 验证约束有效性：添加约束后，可通过以下方式验证：

  • 用init_state.solver.check()检查约束是否可满足，返回True说明约束逻辑无矛盾；
  • 用init_state.solver.eval(k, 10)生成10个样本值，确认是否均为字母或数字。

• 避免约束冲突：如果之前添加过0x20-0x7f的可打印字符约束，无需删除，Angr会自动取两个约束的交集（字母数字本身就在可打印区间内），不会产生冲突。

• 完整示例代码：

  import angr
  import claripy
  from claripy import Or, And
  
  # 初始化项目和符号化输入
  proj = angr.Project("your_binary", auto_load_libs=False)
  input_len = 8  # 根据实际输入长度调整
  input_sym = claripy.BVS("user_input", input_len * 8)
  init_state = proj.factory.entry_state(stdin=input_sym)
  
  # 遍历每个字符添加约束
  for idx in range(input_len):
      char = input_sym.chars[idx]
      init_state.solver.add(
          Or(
              And(char >= ord('A'), char <= ord('Z')),
              And(char >= ord('a'), char <= ord('z')),
              And(char >= ord('0'), char <= ord('9'))
          )
      )
  
  # 验证并生成样本
  if init_state.solver.satisfiable():
      sample = init_state.solver.eval(input_sym, cast_to=bytes)
      print("合法输入样本:", sample)
  else:
      print("约束不可满足，请检查变量或条件")
  

内容的提问来源于stack exchange，提问作者cips