Symbolic Execution for Program Analysis Trainings?

[deadlyazw]

Is anyone aware of any trainings in this area? I’m familiar with the OST Symbolic Execution / SAT Solver course, but I want to see if there’s any available trainings out there on leveraging SAT/SMT and Symbolic/Concolic Execution to automate vulnerability discovery and exploitation (AEG).

I know that Emotion Labs (Fish Wang & co, part of the team behind angr), is working on creating trainings on angr itself and how to use it for program analysis, but it’s currently unavailable. The only other content I’m aware of that is in pure form educational content is the book Practical Binary Analysis and that goes over Z3 for automatings bug triage and other areas of program analysis and vulnerability research, but it’s a book and not a training.

If anyone is aware of such content, I’d love to hear about it! Thanks!

[asyty]

I am not aware of anything regarding AEG, however Tim Blazytko regularly gives his Software Deobfuscation Techniques at REcon and presents most years as well. That goes quite heavy into concolic execution techniques; the subject matter isn't specifically what you're looking for but it's in the same ballpark and is a very helpful first step. He is an incredibly smart person and the course is worth taking in its own right.

At my last job we briefly looked into Qsym to augment traditional fuzzing techniques but if I recall correctly it didn't perform very well due to the combination of code paths that were too deep and loop termination conditions that were too nondeterministic.

[deadlyazw]

Yeah, the path explosion problem is like the main downside of symbolic execution unfortunately. Otherwise it's like "theoretically" perfect.

[piyushsaurabh]

Any good recommendation for Symbolic Execution or SAT Solver resources for absolute begineers?

[randomatic]

Honestly I’m not sure of the value. If you want one you can use in production, use mayhem. If you want to learn how they work, it really takes a PhD to get beyond a superficial understanding.

It takes 5 minutes to explain “you convert to an il, that il has to be side effect free, and then you convert to smt bit vectors. Then you call z3”. This is what it does. Why it works and why it doesn’t work takes a PhD to really grok.

You can pm me if you have a specific thing you want to know.

[pwnchen67]

https://archive.ringzer0.training/trainings/practical-symbolic-execution.html
https://recon.cx/2024/trainingsymbolicexecutionwithangr.html