Ah ! When I saw some time ago that there were useable x86_64-to-llvm lifters and rewriters (was it from Trail of Bits also ?) I wondered how hard it would be to plug with KLEE. Good for Trail of Bits !
(off topic: your blog articles and tech are very inspiring. The deepstate paper, articles and slides made me rethink the whole test pipeline of my applications, from manual oracle-based or model-based tests, to PBT, to fuzzing, to Symbolic/Concolic execution...).
By the way I thought remill and mcsema required IDA ?
Back on topic: One of the reasons I asked about industrial use, is that almost everyone in the security community (that works on SE) seems focused on reverse engineering executables. While I understand the interest and the importance of this part (being able to work on binary code without the source code) I think it's an adversarial view of the topic of Symbolic Execution. It's really hard working precisely on binary code, even if you disable optimizations...
Well, what if I have the source code and want to use SE ? Couldn't I be more precise/efficient ? I'm guessing I'm stuck with KLEE if I'm working in C/C++, and to write an frontend to llvm for Ada stuff...
(off topic: your blog articles and tech are very inspiring. The deepstate paper, articles and slides made me rethink the whole test pipeline of my applications, from manual oracle-based or model-based tests, to PBT, to fuzzing, to Symbolic/Concolic execution...).
By the way I thought remill and mcsema required IDA ?
Back on topic: One of the reasons I asked about industrial use, is that almost everyone in the security community (that works on SE) seems focused on reverse engineering executables. While I understand the interest and the importance of this part (being able to work on binary code without the source code) I think it's an adversarial view of the topic of Symbolic Execution. It's really hard working precisely on binary code, even if you disable optimizations...
Well, what if I have the source code and want to use SE ? Couldn't I be more precise/efficient ? I'm guessing I'm stuck with KLEE if I'm working in C/C++, and to write an frontend to llvm for Ada stuff...