Close Encounters with Symbolic Execution

Summary: At THREADS 2014, Trail of Bits demonstrated a new capability of mcsema that enables KLEE, a symbolic execution framework, to run on software available only in binary form, using it to learn an unknown protocol and the steps through a maze. The post explains that KLEE works on LLVM bitcode and that mcsema lets it analyze arbitrary binaries without source code, a capability the team's DARPA Cyber Grand Challenge reasoning system requires to learn inputs for dozens, hundreds, or thousands of binaries with no prior knowledge or human guidance.
Key Takeaway: The same technique that finds all valid maze paths can automatically generate high-coverage tests or find security bugs in binary programs, meaning attackers and defenders can both reason about software they have no source for.

Read the original at Trail of Bits Blog ↗