Symbolic execution with SymCC: Don't interpret, compile

http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html

55 8 6 years ago

s3.eurecom.fr

I think the paper provides maybe the best introduction and overview of the approach: http://www.s3.eurecom.fr/docs/usenixsec20_symcc.pdf

To me, it was also not clear initially why symbolic execution is useful anyway. But this is for testing. The paper introduction explains it. "Symbolic execution was conceived more than 40 years ago to aid in software testing." The goal is to cover all possible execution paths in all possible conditions, which is hard or impossible with traditional testing.

The new approach here (SymCC) improves a lot on the runtime of the symbolic execution over previous approaches.

rurban• 6 years ago

We use cbmc to generate all possible testcases for that. Also with symbolic execution in C, and much better than Klee.

http://www.cprover.org/cprover-manual/test-suite/

touisteur• 6 years ago

You can do a lot with Symbolic Execution. Bug-reproduction for example. Say your customer remarks on a weird state if the system. You put a 'stop condition' as 'the system is in the state the customer described' and ask 'how'? You get a list of input & their values. Aaaaah that's how :-). Also if you record/print intermediate values you can use them as complexity reduction for your search.

Also, for minimal log/trace placement it's actually fun to use.

algo_trader• 6 years ago

If i understand, this is a one time performance improvement, which reduces the overhead of symbolic execution by emitting final assembly instructions into the final binary.

Great

But i dont see any algorithmic improvement on the exponential explosion of states?

Is this "outsourced" to a fuzzer that has to generate coverage test cases ?

rjeli• 6 years ago

Wow, talk about Baader Meinhof. I’ve spent the last few days hacking out a FOSS Mathematica impl + jupyter kernel, and I’m trying to keep as much of the semantics and stdlib as possible defined inside the interpreted runtime, so I can have a small Haskell core and avoid the verbosity of defining builtins in the interpreter.

However... it’s slow as hell, and I was wondering if I could implement some kind of bytecode compiler to cache results. It looks like this does exactly that, by tagging cells as symbolic or constant, and replacing them on the fly. Hmmm.

The_rationalist• 6 years ago

What are some use cases for symbolic execution? Is it only for fuzzing?

aidenn0• 6 years ago

It's arguably distinct from fuzzing since symbolic execution is deterministic, while fuzzing implies a stochastic process.

Even smarter fuzzing tools like AFL which use branches taken as feedback to the fuzzer are randomized.

PeCaN• 6 years ago

It's actually the exact opposite of fuzzing; with symbolic execution you aim to prove, symbolically, that all possible code paths have some desired behavior (e.g. not crashing,). With fuzzing you just try code paths (guided) randomly and see if any of them crash.

Symbolic execution with SymCC: Don't interpret, compile

Related Stories