search

DonggeLiu / Legion

A coverage-based software testing tool
MIT License
29 stars 4 forks source link

White nodes do not match with symbolic states with the same addresses during symbolic execution #13

Closed gernst closed 4 years ago

DonggeLiu commented 4 years ago
  1. Background 1: Legion only tries to match a symbolic state with tree nodes if that state has at least one sibling. We designed this because, “having a sibling” indicates the symbolic execution tree splits, which implies a conditional jump in the code.
  2. Background 2: ANGR only returns the feasible states during symex.
  3. Hence the failure occurs because ANGR thinks that state is the only feasible child of its parent. Then Legion intentionally does not match that state with the corresponding tree node.
  4. This behaviour is correct and ideal, because simulating from that state/node is the same as simulating from its parent.