25 ms·

A Survey of Symbolic Execution Techniques (2018)

117 points by kachnuv_ocasek 7y ago

touisteur 7y ago
I'm curious, HN. Apart from Fujitsu, do any of you use Symbolic Execution in an Industrial setting or in your day-to-day job ? I'm starting to see fuzzing 'largely' adopted, and an uptick of interest in proof (see recent partnership between Nvidia and AdaCore on Spark2014 for firmware), but not much on Symbolic Execution ? Apart from Trail of Bits, University Research teams, and automatic patching competitions ? Anyone using cbmc, Klee, angr, s2e ?
- PaulHoule 7y ago
  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.
  - touisteur 7y ago
    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 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...
    - pag 7y ago
      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.
      - touisteur 7y ago
        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...
        dtornabene 7y ago
        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-mainp491-p.pdf https://softsec.kaist.ac.kr/~soomink/paper/ase17main-mainp49...
        pag 7y ago
        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.
- archi42 7y ago
  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.
- RockmanX 7y ago
  I believe people who develop critical softwares do software verifications which should involve Symbolic Execution.
- jor-el 7y ago
  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_2019_information_security_hiring/ek374i0 https://www.reddit.com/r/netsec/comments/b90hep/rnetsecs_q2_... [0] https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm-protected-program.html https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm... [1] https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm-protected-program.html https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm... [2] https://github.com/cea-sec/miasm https://github.com/cea-sec/miasm
  - dtornabene 7y ago
    Yeah, this is it. Security firms specializing in static/dynamic analysis are going to be using this stuff. Vulnerability hunting, things like that.
    - souprock 7y ago
      Doing exactly that, and hiring: https://news.ycombinator.com/item?id=19797601 https://news.ycombinator.com/item?id=19797601
      - departure 7y ago
        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?
        souprock 7y ago
        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.
- debatem1 7y ago
  I've used Klee and Triton in industrial settings, but had to abandon Klee due to the many headaches of packaging and distributing it.
  - touisteur 7y ago
    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 :-)
    - debatem1 7y ago
      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.
tempguy9999 7y ago
Oh heck yes, this is interesting to me. In part answer to touisteur, I don't use it and can't see myself ever using it in industry where it's just 'get stuff done' and if it's not too buggy it goes into production. Which is a real downer.
dtornabene 7y ago
This is a solid paper if you want to learn something about SymbEx. If it really interests you and you want something more tutorial oriented, pick up a copy of Practical Binary Analysis, out recently from nostarch. The last chapters are a tutorial intro to it using Triton. If you're a functional programmer and already know some Haskell or Ocaml or are able to pick it up quickly, check out BAP, the binary analysis platform, its got a bunch of tools/analysis built in already for this stuff and there's a fair amount of fascinating research done using or on the platform itself. https://practicalbinaryanalysis.com/ https://practicalbinaryanalysis.com/ https://github.com/BinaryAnalysisPlatform/bap https://github.com/BinaryAnalysisPlatform/bap Cool fact about BAP, there's a really weird but very cool embedded lisp that allows you to drive execution of single instructions via meta programming. It works via a term rewriting system. Seriously one of the coolest lisps I've found out in the wild. http://binaryanalysisplatform.github.io/bap/api/master/Bap_primus.Std.Primus.Lisp.html http://binaryanalysisplatform.github.io/bap/api/master/Bap_p... Also, the docs for the project are borderline decadent in their completeness and the team responsible are quite active via gitter. For real, if you're interested in binary analysis, check it out.
- tempguy9999 7y ago
  No offence intended I don't really see the value of this book WRT to this paper. The paper seems to be about HLLs where the book, great as it surely is, is 90% about, well, binaries. Given that I won't have time to learn binary analysis (there's no payback for me), is it really worth getting the book just for the final chapter, which I presume is not going to cover HLLs anyway?
  - dtornabene 7y ago
    I mean, my comment was pretty straight forward as to the relation? The book has full, detailed code listings and provides a vm with runnable code, you end the book building an automatic exploitation engine for a C++ program, so it does cover HLLs? The binaries in the book are all C/C++ programs. I guess I don't really get the comment(no offense taken), given that techniques like symbex are used on binaries written in HLLs. The paper itself is a survey of the tradeoffs inherent in different implementations of symbex. So, if you want to get a sense of what symbex is, read the paper and follow up with some of the endnotes, if you want to build an application that actually uses symbex buy the book and work through it. Hope this helps!
some_random 7y ago
"Sometimes you can’t see how important something is in its moment, even if it seems kindof important. This is probably one of those times.” > Cyber Grand Challenge highlights from DEF CON 24, August 6, 2016
derefr 7y ago
Is anyone here using Symbolic Execution for something besides source code verification? I’m attempting to use the technique right now in the context of writing an execution tracer for a bytecode VM runtime, where I want to “recover” ABI types for arbitrary bytecode (that I don’t have the source to), in order to emit traces that describe what’s going on in high-level terms (e.g. “foo[x][y].z = 3” rather than “$329f = ($329f & (~(1 << 32) << 8)) | (%r25 & 0xff)”.) So I’m doing a static-analysis pass of the bytecode (essentially a decompilation pass) which symbolically executes math ops to build up symbolic formulae representing the math being done, and to associate program-counter positions in the bytecode with value bindings in the formulae; and then I’m feeding those associations to the runtime tracer, so that it can notice when it’s on an “interesting” PC position and feed its current register/stack value into an instance of the associated formula, for me to emit once I get all the bindings of the formula filled in. So far I haven’t found any texts or papers talking about using symbolic execution in this context (to recover information lost due to previous compilation, in a pass “within” a tracer, JIT, transpiler, or anything else that starts with bytecode or IR), which is kind of annoying. Anyone have any resources? Projects that use this technique? (I’m thinking that this is something you’d see done in sufficiently-advanced game-console emulators, as a “deoptimization” pass to recover structure to help dynamic recompilation optimize better.) Also, related question: if I’ve got a stack machine, and all the jumps in the ISA are indirect jumps (but with literal values pushed on the stack), is there any way to recover the edges between basic blocks without doing a symbolic exec over the stack ops (i.e. to discover, among all the DUPs and SWAPs and such, which constant stack-slot the jump op is actually receiving)? I’m pretty sure there is a “weaker” method, but I’m stymied here by my lack of compiler-theory education; everything I google about dominance hierarchies and such assumes you’re starting with a model of a register machine with direct jumps (where the edges are context-free extractable from the jump ops).
- kolinko 7y ago
  That's roughly how I do it for Eveem.org (Ethereum VM decompiler) - what you see there is essentially an output from the symbolic execution trace.
kolinko 7y ago
Oh oh, a room for a shameless plug! :) I managed to use symbolic execution to build a smart contract decompiler - Eveem.org. What you see there is essentially a trace from a symbolic execution of an Ethereum contract, plus some postprocessing.
deleted 7y ago
[deleted]
deleted 7y ago
[deleted]
deleted 7y ago
[deleted]
srfilipek 7y ago
> Soundness prevents false negatives, i.e., all possible unsafe inputs are guaranteed to be found, while completeness prevents false positives, i.e., input values deemed unsafe are actually unsafe. I really dislike this definition. It is confusing and backwards from normal math/logic parlance.
- smallnamespace 7y ago
  Isn't this the normal definition for, say, type systems? A sound type system will never accept an invalid program (no false negatives) but may reject correct programs.
  - deleted 7y ago
    [deleted]
  - deleted 7y ago
    [deleted]
  - srfilipek 7y ago
    The problem is really this: > all possible unsafe inputs are guaranteed to be found A sound system can reject all programs and still be sound. Therefore, it does not follow that all possible unsafe inputs are guaranteed to be found. In my view, focusing on program acceptance or rejection is not really helpful.

I'm curious, HN. Apart from Fujitsu, do any of you use Symbolic Execution in an Industrial setting or in your day-to-day job ? I'm starting to see fuzzing 'largely' adopted, and an uptick of interest in proof (see recent partnership between Nvidia and AdaCore on Spark2014 for firmware), but not much on Symbolic Execution ? Apart from Trail of Bits, University Research teams, and automatic patching competitions ? Anyone using cbmc, Klee, angr, s2e ?

PaulHoule 7y ago
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.
- touisteur 7y ago
  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 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...
  - pag 7y ago
    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.
    - touisteur 7y ago
      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...
      - dtornabene 7y ago
        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-mainp491-p.pdf https://softsec.kaist.ac.kr/~soomink/paper/ase17main-mainp49...
      - pag 7y ago
        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.
archi42 7y ago
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.
RockmanX 7y ago
I believe people who develop critical softwares do software verifications which should involve Symbolic Execution.
jor-el 7y ago
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_2019_information_security_hiring/ek374i0 https://www.reddit.com/r/netsec/comments/b90hep/rnetsecs_q2_... [0] https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm-protected-program.html https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm... [1] https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm-protected-program.html https://blog.quarkslab.com/deobfuscation-recovering-an-ollvm... [2] https://github.com/cea-sec/miasm https://github.com/cea-sec/miasm
- dtornabene 7y ago
  Yeah, this is it. Security firms specializing in static/dynamic analysis are going to be using this stuff. Vulnerability hunting, things like that.
  - souprock 7y ago
    Doing exactly that, and hiring: https://news.ycombinator.com/item?id=19797601 https://news.ycombinator.com/item?id=19797601
    - departure 7y ago
      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?
      - souprock 7y ago
        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.
debatem1 7y ago
I've used Klee and Triton in industrial settings, but had to abandon Klee due to the many headaches of packaging and distributing it.
- touisteur 7y ago
  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 :-)
  - debatem1 7y ago
    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.

tempguy9999 7y ago

Oh heck yes, this is interesting to me. In part answer to touisteur, I don't use it and can't see myself ever using it in industry where it's just 'get stuff done' and if it's not too buggy it goes into production. Which is a real downer.

dtornabene 7y ago

This is a solid paper if you want to learn something about SymbEx. If it really interests you and you want something more tutorial oriented, pick up a copy of Practical Binary Analysis, out recently from nostarch. The last chapters are a tutorial intro to it using Triton. If you're a functional programmer and already know some Haskell or Ocaml or are able to pick it up quickly, check out BAP, the binary analysis platform, its got a bunch of tools/analysis built in already for this stuff and there's a fair amount of fascinating research done using or on the platform itself. https://practicalbinaryanalysis.com/ https://practicalbinaryanalysis.com/ https://github.com/BinaryAnalysisPlatform/bap https://github.com/BinaryAnalysisPlatform/bap Cool fact about BAP, there's a really weird but very cool embedded lisp that allows you to drive execution of single instructions via meta programming. It works via a term rewriting system. Seriously one of the coolest lisps I've found out in the wild. http://binaryanalysisplatform.github.io/bap/api/master/Bap_primus.Std.Primus.Lisp.html http://binaryanalysisplatform.github.io/bap/api/master/Bap_p... Also, the docs for the project are borderline decadent in their completeness and the team responsible are quite active via gitter. For real, if you're interested in binary analysis, check it out.

tempguy9999 7y ago
No offence intended I don't really see the value of this book WRT to this paper. The paper seems to be about HLLs where the book, great as it surely is, is 90% about, well, binaries. Given that I won't have time to learn binary analysis (there's no payback for me), is it really worth getting the book just for the final chapter, which I presume is not going to cover HLLs anyway?
- dtornabene 7y ago
  I mean, my comment was pretty straight forward as to the relation? The book has full, detailed code listings and provides a vm with runnable code, you end the book building an automatic exploitation engine for a C++ program, so it does cover HLLs? The binaries in the book are all C/C++ programs. I guess I don't really get the comment(no offense taken), given that techniques like symbex are used on binaries written in HLLs. The paper itself is a survey of the tradeoffs inherent in different implementations of symbex. So, if you want to get a sense of what symbex is, read the paper and follow up with some of the endnotes, if you want to build an application that actually uses symbex buy the book and work through it. Hope this helps!

some_random 7y ago

"Sometimes you can’t see how important something is in its moment, even if it seems kindof important. This is probably one of those times.” > Cyber Grand Challenge highlights from DEF CON 24, August 6, 2016

derefr 7y ago

Is anyone here using Symbolic Execution for something besides source code verification? I’m attempting to use the technique right now in the context of writing an execution tracer for a bytecode VM runtime, where I want to “recover” ABI types for arbitrary bytecode (that I don’t have the source to), in order to emit traces that describe what’s going on in high-level terms (e.g. “foo[x][y].z = 3” rather than “$329f = ($329f & (~(1 << 32) << 8)) | (%r25 & 0xff)”.) So I’m doing a static-analysis pass of the bytecode (essentially a decompilation pass) which symbolically executes math ops to build up symbolic formulae representing the math being done, and to associate program-counter positions in the bytecode with value bindings in the formulae; and then I’m feeding those associations to the runtime tracer, so that it can notice when it’s on an “interesting” PC position and feed its current register/stack value into an instance of the associated formula, for me to emit once I get all the bindings of the formula filled in. So far I haven’t found any texts or papers talking about using symbolic execution in this context (to recover information lost due to previous compilation, in a pass “within” a tracer, JIT, transpiler, or anything else that starts with bytecode or IR), which is kind of annoying. Anyone have any resources? Projects that use this technique? (I’m thinking that this is something you’d see done in sufficiently-advanced game-console emulators, as a “deoptimization” pass to recover structure to help dynamic recompilation optimize better.) Also, related question: if I’ve got a stack machine, and all the jumps in the ISA are indirect jumps (but with literal values pushed on the stack), is there any way to recover the edges between basic blocks without doing a symbolic exec over the stack ops (i.e. to discover, among all the DUPs and SWAPs and such, which constant stack-slot the jump op is actually receiving)? I’m pretty sure there is a “weaker” method, but I’m stymied here by my lack of compiler-theory education; everything I google about dominance hierarchies and such assumes you’re starting with a model of a register machine with direct jumps (where the edges are context-free extractable from the jump ops).

kolinko 7y ago
That's roughly how I do it for Eveem.org (Ethereum VM decompiler) - what you see there is essentially an output from the symbolic execution trace.

kolinko 7y ago

Oh oh, a room for a shameless plug! :) I managed to use symbolic execution to build a smart contract decompiler - Eveem.org. What you see there is essentially a trace from a symbolic execution of an Ethereum contract, plus some postprocessing.

deleted 7y ago

[deleted]

deleted 7y ago

[deleted]

deleted 7y ago

[deleted]

srfilipek 7y ago

> Soundness prevents false negatives, i.e., all possible unsafe inputs are guaranteed to be found, while completeness prevents false positives, i.e., input values deemed unsafe are actually unsafe. I really dislike this definition. It is confusing and backwards from normal math/logic parlance.

smallnamespace 7y ago
Isn't this the normal definition for, say, type systems? A sound type system will never accept an invalid program (no false negatives) but may reject correct programs.
- deleted 7y ago
  [deleted]
- deleted 7y ago
  [deleted]
- srfilipek 7y ago
  The problem is really this: > all possible unsafe inputs are guaranteed to be found A sound system can reject all programs and still be sound. Therefore, it does not follow that all possible unsafe inputs are guaranteed to be found. In my view, focusing on program acceptance or rejection is not really helpful.