[klee-dev] Is KLEE input only source code, or does it support arbitrary binaries too?

[Jim Lacy]

Thank you.
Then I ran into:  http://blog.trailofbits.com/2014/12/04/close-encounters-with-symbolic-execution-part-2/Apparently with the TRAIL OF BITS https://github.com/trailofbits/mcsema project it's process binary machine codeinto the LLVM IR for KLEE.

  
|  
|   
|   
|   |    |

   |

  |
|  
|   |  
Close Encounters with Symbolic Execution (Part 2)
 This is part two of a two-part blog post that shows how to use KLEE with mcsema to symbolically execute Linux bi...  |   |

  |

  |

 
      From: Chris Hobbs <chobbs at qnx.com>
 To: klee-dev at imperial.ac.uk 
 Sent: Thursday, April 21, 2016 8:19 AM
 Subject: Re: [klee-dev] Is KLEE input only source code, or does it support arbitrary binaries too?
   
 Klee reads and processes the llvm intermediate code. So it's not the C/C++ source per se.
 
 Chris Hobbs
 QNX Software Systems
 
 On 16-04-20 03:38 PM, Jim Lacy wrote:
  
 
 I read a KLEE white paper and it appears the it's intended to work on source code (C or C++).
 Looking at some of the archive posts it looks like it might support arbitrary x86 binaries as well. 
  Can I use KLEE to help me find bugs/problems in binaries? 
  Thanks in advance, 
   
  
 _______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
klee-dev Info Page
 
 
  
|  
|   
|   
|   |    |

   |

  |
|  
|   |  
klee-dev Info Page
   |   |

  |

  |

 

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


  
-------------- next part --------------
HTML attachment scrubbed and removed