Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Show HN: Symbolica – Try our symbolic code executor in the browser

news.ycombinator.com

Post reply on HN
Print view View original

21–30 of 37 posts

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#21

Post by tails4e »

SebastianFish wrote: post #10

I think the problem this product is trying to solve, making it easier to implement rigorous testing, is an important one. When I talk to junior developers I compare enterprise software development to painting. When you paint a room, most of your time is actually spent taping out all of the edges and boundaries. The verb painting is a misnomer. Similarly, it isn't a fast or easy for devs to see all of the boundary con…

This is interesting, it seems like it may in fact be testing by looping, given it took a minute, and didn't conclude. For hardware design there are logic equivalence checking tools that work very differently - they essentially work by reducing a function (piece of hardware) to a minimized boolean equation. The method of reduction ensures the same logic, no matter how coded, results in the same boolean equation, and then comparing the equations is direct and does not require testing all input values. Hardware verification also has a higher bar than software, where code coverage analysis can require 100% on line, branch, value, condition, expression, functional, etc. Its a lot of work, but does give very high confidence there are zero bugs.

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#22

Post by xendo »

pag wrote: post #9

Can you explain how your offering compares with open-source alternatives, such as KLEE [1] and DeepState [2]? P.S. your logo is surprisingly similar to that of ForAllSecure [3], which also provides a symbolic execution engine called Mayhem [4]. [1] https://klee.github.io/ (online example: http://klee.doc.ic.ac.uk/ ) [2] https://github.com/trailofbits/deepstate#readme [3] https://forallsecure.com/ [4] https://users.ec…

Their logo is just \forall quantifier, which is pretty much what those products do, so I wouldn't be that surprised.

https://en.wikipedia.org/wiki/Universal_quantification

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#23

Post by hkopp »

Cool. I have a background in IT security and am sometimes doing symbolic (or concolic) execution on binaries instead of source code. So I may not be the target audience.

Nevertheless I think you should do a comprehensive list what your tool can detect and what not, instead of some examples. From the sample programs i learned that it can check two programs for semantical equivalence and can detect undefined behavior. I did not get the example with the memory violation, as symbolica.h is not included in the code. Additionally, your tool could create test cases that trigger the error, afaik.

Regarding the feedback for the user, as multiple others have mentioned, the running time is very long and thus a simple timer may not be sufficient. But I do not have an idea how to improve that.

I am not sure if you are working on the target program directly, or on the compiled binary. In the example with the division by zero, there is a print statement in order to stop the compiler from removing dead code. But I do not understand where you need a compiler, if you are working directly on C. On the other hand, when you are working on the compiled binary, then your tool is very similar to other symbolic execution engines, such as angr.

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#24

Post by BiteCode_dev »

> We've currently got proof of concept implementations for Lisp and Python

So what would be the benefit over something like http://hypothesis.readthedocs.io ?

From the look of it (the mention of "free" on the website), you have some monetization in mind. What form would that take?

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#25

Post by Choc13 »

hkopp wrote: post #23

Cool. I have a background in IT security and am sometimes doing symbolic (or concolic) execution on binaries instead of source code. So I may not be the target audience. Nevertheless I think you should do a comprehensive list what your tool can detect and what not, instead of some examples. From the sample programs i learned that it can check two programs for semantical equivalence and can detect undefined behavior.…

Hey, thanks for the feedback. A more comprehensive list of features is on our todo list, we’ll update the site shortly.

The memory violation one doesn’t include symbolica.h because we don’t need to symbolize any variables for that one. When we run the compiled code through our solver it adds additional constraints such as, “don’t access memory that’s out of bounds”, so we can detect that automatically.

On your final point, we’re working on the LLVM bitcode so we do have to compile the code, hence the print statement. You’re right in that this is similar to other symbolic executors. We built this one as we found others were quite difficult to get started with and were hard to extend with the features we personally wanted as well as not supporting the languages we wanted either. Obviously at this point in time we’ve not achieved these goals yet, but we think we’ve built the foundations to be able to do so.

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#26

Post by Choc13 »

BiteCode_dev wrote: post #24

> We've currently got proof of concept implementations for Lisp and Python So what would be the benefit over something like http://hypothesis.readthedocs.io ? From the look of it (the mention of "free" on the website), you have some monetization in mind. What form would that take?

I’ve not used Hypothesis, but says it’s inspired by QuickCheck and I’m a regular user of FsCheck which is the F# equivalent. Those tools have a similar goal in mind that we do, but whereas they generate randomised test data (I think FsCheck creates 100 test cases IIRC), we effectively solve the equation so we can actually say that it holds for all inputs. The key difference is that we don’t actually invoke the code with concrete values, but rather treat it like a set of constraints that should always be satisfied. We then check these constraints and if they fail we can reverse engineer a concrete value that would cause the violation. So we effectively run it for all inputs, without actually running it for any inputs.

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#27

Post by Choc13 »

www_harka_com wrote: post #20
Choc13 wrote: post #5

Earlier quoted context omitted.

I’m not quite sure what you meant by this statement “Javascript that runs on back-button mouse over is not where to put your efforts.” Was this something you observed on our site, or just a general point about prioritising the core product over fancy UI effects on the website? Would you mind clarifying?

I might be wrong, but I think he meant that JS runs, a new http request is made, when you hover over the logo. (Which is close to the back button, so it seems like JS is running, when you hover over the back button.)

Ah right yeah that makes sense. We built the website using NextJS so we kinda got this for free with their Image component.

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#28

Post by Choc13 »

Choc13 wrote: post #26
BiteCode_dev wrote: post #24

> We've currently got proof of concept implementations for Lisp and Python So what would be the benefit over something like http://hypothesis.readthedocs.io ? From the look of it (the mention of "free" on the website), you have some monetization in mind. What form would that take?

I’ve not used Hypothesis, but says it’s inspired by QuickCheck and I’m a regular user of FsCheck which is the F# equivalent. Those tools have a similar goal in mind that we do, but whereas they generate randomised test data (I think FsCheck creates 100 test cases IIRC), we effectively solve the equation so we can actually say that it holds for all inputs. The key difference is that we don’t actually invoke the code w…

On the monetisation point we do plan to have a paid version of the product too. We think that one of the limiting factors of using symbolic execution to date has been in the path explosion problem when analysing large programs. A large part of our reasoning behind building a new symbolic executor from scratch was that we wanted to be able to parallelise it to help overcome this issue. We intend to provide a cloud hosted version of Symbolica that makes use of this so that users can get access to this compute power on a pay per use basis.

So our rough plans at the moment are to charge on a consumption basis to use this service.

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#29

Post by Chirono »

Choc13 wrote: post #15
SebastianFish wrote: post #10

I think the problem this product is trying to solve, making it easier to implement rigorous testing, is an important one. When I talk to junior developers I compare enterprise software development to painting. When you paint a room, most of your time is actually spent taping out all of the edges and boundaries. The verb painting is a misnomer. Similarly, it isn't a fast or easy for devs to see all of the boundary con…

Yeah I think that's a great analogy, we noticed the same thing when we used to work together at our last jobs which is what motivated to start this venture. On the implementation side, yes we're using Z3, you can have a poke around at the core symbolic executor at https://github.com/SymbolicaDev/Symbolica In terms of managing the path explosion problem, we have a few techniques that we've prototyped locally. For inst…

I think the surprise comes from how long it takes to get the answer, not that it's incorrect.

By comparison, gcc is able to reduce those two implementations to the same thing and prove them equal in a fraction of the time (https://godbolt.org/z/6oMEd8ebY). If it takes Symbolica a minute for the same tiny example, how does it work on real codebases?

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#30

Post by Choc13 »

tails4e wrote: post #21
SebastianFish wrote: post #10

I think the problem this product is trying to solve, making it easier to implement rigorous testing, is an important one. When I talk to junior developers I compare enterprise software development to painting. When you paint a room, most of your time is actually spent taping out all of the edges and boundaries. The verb painting is a misnomer. Similarly, it isn't a fast or easy for devs to see all of the boundary con…

This is interesting, it seems like it may in fact be testing by looping, given it took a minute, and didn't conclude. For hardware design there are logic equivalence checking tools that work very differently - they essentially work by reducing a function (piece of hardware) to a minimized boolean equation. The method of reduction ensures the same logic, no matter how coded, results in the same boolean equation, and t…

Hey, the reason for the long times on the playground is actually that we’re having to wait for build servers to boot up and then build the code before we can finally ship it off to our backend for analysis. We’ve had quite a bit of feedback on this slowness and we hope to eliminate some of this constant factor boot up and compile time soon, and for what remains make it clear that this is what’s happening in the status box.

So although it might seem like it, we’re not actually doing any looping, we’re doing constraint solving as you’ve mentioned.

Post reply on HN