4 ms·

Symbolic execution with SymCC: Don't interpret, compile

albertzeyer 6y ago
I think the paper provides maybe the best introduction and overview of the approach: http://www.s3.eurecom.fr/docs/usenixsec20_symcc.pdf 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 6y 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/ http://www.cprover.org/cprover-manual/test-suite/
- touisteur 6y 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 6y 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 6y 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 6y ago
What are some use cases for symbolic execution? Is it only for fuzzing?
- aidenn0 6y 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 6y 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.

I think the paper provides maybe the best introduction and overview of the approach: http://www.s3.eurecom.fr/docs/usenixsec20_symcc.pdf 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 6y 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/ http://www.cprover.org/cprover-manual/test-suite/
touisteur 6y 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 6y 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 6y 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 6y ago

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

aidenn0 6y 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 6y 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.