5 ms·

Co-author here. We're planning to turn this into a series, with additional posts on how symbolic execution works at a lower level, how to present counterexample

Co-author here. We're planning to turn this into a series, with additional posts on how symbolic execution works at a lower level, how to present counterexamples to users, and ideas for future programming tools built on symbolic execution.

CalChris 7y ago
Seriously helpful article. Looking forward to the sequels. we can map each syntax tree to an interpreter Maybe I'm being dense but I'm not sure what you mean by map here. A map is from set to set. I'm not thinking of an interpreter as a set.
- Xophmeister 7y ago
  The set of interpreters.
- joelburget 7y ago
  I'll use a bit of Haskell in my response, since that's what I'm most comfortable with and what we actually use for our work. Hopefully that's okay. We can define a data type of expressions in our language, with addition, multiplication, etc. data Expr = Addition Expr Expr | Multiplication Expr Expr | ... Then we need the type of an interpreter which consumes program inputs and produces an output. I'll leave this abstract for now. data Interpreter = ... By map, we just mean that we can write a Haskell function with this type interpret :: Expr -> Interpreter interpret (Addition a b) = (+) <$> interpret a <*> interpret b interpret (Multiplication a b) = (*) <$> interpret a <*> interpret b If you're curious, here's some real symbolic evaluation code I wrote doing the same https://github.com/kadena-io/pact/blob/234ba3dd01f0df8b4e462a33c1e711482e03ca99/src/Pact/Analyze/Eval/Numerical.hs#L72-L89 https://github.com/kadena-io/pact/blob/234ba3dd01f0df8b4e462...
  - CalChris 7y ago
    Well, I'm glad I asked. I get this now. It really is a mapping. But this was a bit of shorthand that I didn't get in the post. You might want to add that.
dfabulich 7y ago
One piece of feedback: I've often wished to work on static analysis tools, but too much of the work in this area is focused on Haskell or Lisp. (All of the code in this article is in Haskell or Lisp.) Does any of this stuff work on Java, Python, or JavaScript? I want to improve the quality of real-world programs written in industry-standard languages. This "gentle introduction" makes it seem like the first step of the process is "port your app to a homoiconic language," -- or, in other words, "you can prove the correctness of any language you want, as long as it's Haskell or Lisp."
- nickpsecurity 7y ago
  https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis https://en.wikipedia.org/wiki/List_of_tools_for_static_code_...
  - dfabulich 7y ago
    That's static analysis, but not symbolic execution. Looking at the JavaScript section, you can't do any of the stuff described in the article with JSLint.
    - tluyben2 7y ago
      Abstract interpretation is a wider concept than symbolic execution; check the post in the top thread answered by user mjn to get more info; the fb and mozilla ones seem to focus on more mainstream languages.
    - nickpsecurity 7y ago
      The parent said "static analysis" tools. That's what I gave them.
- sophiebits 7y ago
  Prepack is an example of a (not production ready) tool to do abstract evaluation of JS.

CalChris 7y ago

Seriously helpful article. Looking forward to the sequels. we can map each syntax tree to an interpreter Maybe I'm being dense but I'm not sure what you mean by map here. A map is from set to set. I'm not thinking of an interpreter as a set.

Xophmeister 7y ago
The set of interpreters.
joelburget 7y ago
I'll use a bit of Haskell in my response, since that's what I'm most comfortable with and what we actually use for our work. Hopefully that's okay. We can define a data type of expressions in our language, with addition, multiplication, etc. data Expr = Addition Expr Expr | Multiplication Expr Expr | ... Then we need the type of an interpreter which consumes program inputs and produces an output. I'll leave this abstract for now. data Interpreter = ... By map, we just mean that we can write a Haskell function with this type interpret :: Expr -> Interpreter interpret (Addition a b) = (+) <$> interpret a <*> interpret b interpret (Multiplication a b) = (*) <$> interpret a <*> interpret b If you're curious, here's some real symbolic evaluation code I wrote doing the same https://github.com/kadena-io/pact/blob/234ba3dd01f0df8b4e462a33c1e711482e03ca99/src/Pact/Analyze/Eval/Numerical.hs#L72-L89 https://github.com/kadena-io/pact/blob/234ba3dd01f0df8b4e462...
- CalChris 7y ago
  Well, I'm glad I asked. I get this now. It really is a mapping. But this was a bit of shorthand that I didn't get in the post. You might want to add that.

dfabulich 7y ago

One piece of feedback: I've often wished to work on static analysis tools, but too much of the work in this area is focused on Haskell or Lisp. (All of the code in this article is in Haskell or Lisp.) Does any of this stuff work on Java, Python, or JavaScript? I want to improve the quality of real-world programs written in industry-standard languages. This "gentle introduction" makes it seem like the first step of the process is "port your app to a homoiconic language," -- or, in other words, "you can prove the correctness of any language you want, as long as it's Haskell or Lisp."

nickpsecurity 7y ago
https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis https://en.wikipedia.org/wiki/List_of_tools_for_static_code_...
- dfabulich 7y ago
  That's static analysis, but not symbolic execution. Looking at the JavaScript section, you can't do any of the stuff described in the article with JSLint.
  - tluyben2 7y ago
    Abstract interpretation is a wider concept than symbolic execution; check the post in the top thread answered by user mjn to get more info; the fb and mozilla ones seem to focus on more mainstream languages.
  - nickpsecurity 7y ago
    The parent said "static analysis" tools. That's what I gave them.
sophiebits 7y ago
Prepack is an example of a (not production ready) tool to do abstract evaluation of JS.