I have come across many pentesting labs using these tools to deal with obfuscated binaries. You can check Quakslab's blog, they have articles on this [0]. Another interesting project is of cracking Tigress VM using Symbolic execution [1]. The use has dramatically increased in past few years as many new tools are available and also hardware is more performant now. I am also using these tools in my day-to-day job to deal with obfuscated binaries and reverse engineering. I use Miasm [2].

PS: My company is hiring for such roles https://www.reddit.com/r/netsec/comments/b90hep/rnetsecs_q2_...

[0] https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm... [1] https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm... [2] https://github.com/cea-sec/miasm

Yeah, this is it. Security firms specializing in static/dynamic analysis are going to be using this stuff. Vulnerability hunting, things like that.

Doing exactly that, and hiring: https://news.ycombinator.com/item?id=19797601

Funny that none of your posts mention that it's (I think) Raytheon. Do you think you get less responses if you mention it's a major defense contractor?

Multiple reasons:

Big companies are frequently composed of components with distinct culture, benefits, legal entity, and so on. People get to know one part, then assume that all parts are that way. I'm in a component with compensation that is better than average for the big company. The association isn't beneficial.

Using the big company name means adhering to corporate branding requirements. People could somehow imagine me to be issuing official corporate communications, which is far from the truth.

I might get more responses, but would I want them? We're fighting to keep out the toxic people who want to focus on politics. We have important work to do.

There is an absurd Glassdoor review out there. If that is to be believed, we pay highly experienced cleared specialists about as much as they'd make cooking food at In-N-Out or Chick-Fil-A. Our office would be empty if that were the pay being offered.

lol, fighting to keep out "toxic people" who "want to focus on politics" means you hire people cool with making weapons of war. I for one am glad the person who asked you that did so, because I do not work for defense contractors, and I don't need to waste my time looking into a place that would filter out anyone with conscience.

That is a different sort of "toxic" and a different sort of "politics", but yeah we don't want that either. I was referring to the sort of people you'd find in Google or even HP, backstabbing and undermining to jockey for position in the corporate hierarchy.

People with a conscience can feel that it is wrong to devote their efforts to tracking people all across the internet to sell ads and other junk. (Facebook, Google, etc.) They can feel that it is important to support their country, and that it would be wrong to pass up a reasonable opportunity to do so. With a better conscience, you would feel guilty about how you benefit from the nation without contributing much, and of course you would stop supporting violent hate groups that pretend to be otherwise.

My experience about any area I've specialized in is that for every one that is talked about publicly there are maybe ten things that are not being talked about.

This is particularly the case when the new technology is a particular competitive advantage.

One firm that I worked for developed a highly competitive product using a deep neural net (back when the Restricted Boltzmann Machine was a thing!) and the "deep learning" hype was just starting. They sent a marketing person to my office to interview me about what things we could say about the product that would make it sound impressive and I told him all about it, but his superiors didn't let him use the material because they didn't want competitors to know how it worked.

This is my guess also. Even in large engineering-driven companies, you often discover during your very proud (internal) talk about Shiny New Tech that other people in the group have been doing it for some time...

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.

I've seen some rare papers with CBMC and I know the tech has been ported to Java, javascript and apparently something is in progress for Ada ?

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...

We at Trail of Bits are also working on "klee-native," a port of KLEE using Remill to dynamically lift and emulate binaries. This project is very early on, though.

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...

There are a number of lifters. The McSema repo has a table detailing the features of most of them.

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.

Thanks pag for the correction on remill. And I didn't know about mcsema/dyninst, great !

Do you have something written somewhere on how you would do different from KLEE ?

Nope :-P

if you're interested in lifters, this research is a pretty eye opening peek into the guts of several, and how one goes about actually testing their accuracy

https://softsec.kaist.ac.kr/~soomink/paper/ase17main-mainp49...

By the way, did you know that DeepState is actually pure C, and that all the C++ is just window dressing on top? This means that you could feasibly integrate components of it in Ada, or call to those components in Ada, assuming that you haven't already produced your own variants of things.

Tried to connect DeepState ans Ada through C indeed, but since I can't make angr work with Ada yet, it's not really useful right now. For fuzzing I think DeepState was limited to libfuzzer ? Which needs clang or someone to port this to gcc-gnat (humpf) and I'm not sure DeepState supported AFL yet (EDIT: just looked at the repo now, and I see support for AFL and eclipser, Nice !) ... Will retry all this soon though. Thanks for the reminder !

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...

Hopefully we'll have a Dockerfile soon that gets things all set up :-D

Symbolic Execution [SE] is a subset of Abstract Interpretation [AI] (Cousot et Cousot, '70+something), which we use in our product, which is in turn used by industrial customers. While this goes primarily in the safety direction, I'd dare to say "yes, this kind of stuff is actually used". Though maybe our customers wouldn't say "we use AI/SE in our process", since they're usually not that deep into the theory behind it - in the end, the results are what matters most.

I didn't bother proving it, but I think that some of our techniques could be interpreted as some kind of SE; but the general case is that they're AI.

I've used Klee and Triton in industrial settings, but had to abandon Klee due to the many headaches of packaging and distributing it.

I'm curious about what are the difficulties of packaging KLEE. Isn't there a docker image you can use ?

I know installing it from source is a pain, but a scriptable pain.

I'm also wondering (curiosity) why you'd have to package and deliver it (to customers ?). I always saw it as a developer tool. Seems you're working on very interesting stuff :-)

Yeah, it isn't literally impossible to build-- but the fact that it's enough of a pain to do so that they distribute a docker image should sort of tell the story :). Unfortunately, for IT policy reasons we couldn't use that, and our platform was a bit unusual anyway.

In terms of packaging, it's nothing exciting-- we just had to produce a .deb if we wanted to install something on a build or test server.

I believe people who develop critical softwares do software verifications which should involve Symbolic Execution.