But you never know, maybe I looked in the wrong parts of the Internet.
I'm genuinely curious though: since most of those projects are open-source you'd expect to see some traces of some activity/problems on GitHub or on mailing-lists, and... well... Not much to be seen.
angr I tried very hard to use on Ada programs but it seems the VEX lifter and CFG builder couldn't handle simple Ada programs (wasn't patient enough to submit this on GitHub...). But for C programs it's very fun and all scriptable ! There is also this nice of a 'pluggable test environment' (deepstate from Trail of Bits https://github.com/trailofbits/deepstate) that allows to switch between hand-written unit tests, fuzzers, and symbolic execution (letting you decide which variables are Symbolic, which are concrete...) with angr. Also some cool stuff mixing AFL and angr (driller) and another project mixing Intel PT and angr.
KLEE seems to have the most papers (quantity and quality), just landed support for C++ and upgraded to a recent llvm...
(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...
Glad that DeepState had an impact on you :-D We continue to evolve DeepState, both in the direction of better fuzzing, and better test case reduction.
Remill is instruction granularity, and so all it requires is raw bytes. McSema uses Remill in conjunction with a disassembly frontend (IDA Pro, Binary Ninja, or Dyninst).
If you have source code you can likely be more precise/efficient. Sometimes you may have access to source but not the ability to change/influence the build.
I think there's a lot of room for improvement with KLEE. If I were to write an LLVM symbolic executor from scratch then I think I would do some things differently.
Do you have something written somewhere on how you would do different from KLEE ?
What I was thinking was some improvements to gnattest (https://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ug...) but also a way to add some quickcheck-like generator features (Ada already has the property description language through contracts) with Libadalang... One can dream !
But the whole "Let the developer write one test harness and use it almost as-is with different testing/validation techs" (I'm not explaining it well) was some kind of revelation.
When you say 'adding a fuzzing test harness is only 2-3 days work' you still get complaints: that's too much (but I then found dozens of bugs), it's /another/ test harness to maintain, we'll have to rebuild an input corpus for every interface break (true...). Anything that could alleviate the pain would be great...