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

31–37 of 37 posts

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

#31

Post by BiteCode_dev »

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…

Thank you.

> 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

How does that work with a dynamic language such as Python?

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

#32

Post by Choc13 »

Chirono wrote: post #29
Choc13 wrote: post #15

Earlier quoted context omitted.

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?

Ah right, makes sense, thanks. Most of the time on the playground is spent booting a build server (we're using GitHub actions behind the scenes just for this part of the playground) and then building the code. I just ran this example myself and the build part took around 50 seconds before it actually sent the bitcode off to be analysed.

We need to add some more detailed diagnostic outputs to the actual execution part so that we can see the timings more clearly, but as a rough approximation from looking at the logs the execution API took about 10 seconds to run and some of that time would be in waiting for the message to be dequeued and for the function to wake up and process the job. So it's taking maybe around 5 seconds right now to analyse this one.

I know that's still quite slow, but we've not yet spent any real time on optimisations to the execution part so we're quite confident we can make this bit faster. As for the constant build overhead, this is something that's only really applicable to our playground, as users would likely build their code locally or have already built it as part of a CI run. Given all the feedback on this slowness though we are planning to make some improvements to this build part of the playground too to help reduce this constant overhead, or at least make it more obvious that this is what is causing the initial part of the waiting time.

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

#33

Post by Choc13 »

BiteCode_dev wrote: post #31
Choc13 wrote: post #26

Earlier quoted context omitted.

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…

Thank you. > 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 How does that work with a dynamic language such as Python?

The static type information isn't actually too important to us, what our tool cares about is being able to interpret branching conditions in the code in order to turn them into constraints. We currently do this at the LLVM IR level, so as long as we can compile the code down into this form then we can analyse it. With Python a lot of the work we had to do in order to get a prototype working was in being able to handle all of the system calls that the Python interpreter needs to make when booting up. These aren't always straight forward to treat symbolically because they interact with the file system etc, but it's possible to provide mock implementations that don't affect the analysis of the users code.

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

#34

Post by hkopp »

Choc13 wrote: post #25
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…

Thank you for the answer and a big kudos for the project.

Regarding the memory violation, could symbolica deal with symbolic memory? Can it deal with symbolic files as input? How about syscalls with symbolic inputs? These are the main problems I had when I worked on my toy symbolic execution engine. If yes, you should definitely market these features.

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

#35

Post by Choc13 »

buitreVirtual wrote: post #14

Most code nowadays consists of calling third party libraries and your system's other modules. How do you build the models of those components for symbolic execution?

Great question. This obviously isn't exposed through the playground right now as that's just a single file demo.

Our backend software does integrate with larger build systems. So the way you would handle third party deps is to link them during the build and then analyse the whole built module. We plan to make it easier to integrate with toolchains for specific languages in the future.

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

#36

Post by Choc13 »

hkopp wrote: post #34
Choc13 wrote: post #25

Earlier quoted context omitted.

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…

Thank you for the answer and a big kudos for the project. Regarding the memory violation, could symbolica deal with symbolic memory? Can it deal with symbolic files as input? How about syscalls with symbolic inputs? These are the main problems I had when I worked on my toy symbolic execution engine. If yes, you should definitely market these features.

Yeah it can deal with symbolic memory. As long as the memory allocation is fixed size the contents can be fully or partially symbolic. We also support symbolic addresses for allocations to ensure that pointer arithmetic is fully tested.

We're currently simulating a lot of the underlying system at the C std library level. For a number of reasons we'd like to lower this to the raw syscall and assembly level. This would allow any lib C implementation to be tested along with the application code, and we may even be able to simulate threading and the file system. Syscalls could be made symbolic along with files by treating the entire system symbolically, but obviously this is a lot of work so it's something that we're gradually building towards.

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

#37

Post by Choc13 »

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…

Yeah sure. We initially wanted to build something to compare the equivalence of two programs written in different languages and for this we started out using KLEE. Unfortunately, we found it didn't quite satisfy our needs and then changes we wanted to make didn't really fit with their architectural model. We also felt like it wasn't as amenable to parallelisation as we would have liked. The core technology is using an SMT solver just like KLEE, but our hope is that Symbolica will be more scalable and easier to use for larger problems.

DeepState looks interesting, we had seen this before and other stuff from trail of bits, but admittedly we haven't used it ourselves. Our impression is that it seems like more of a frontend to various symbolic execution / fuzzing backends. So maybe it's something we should consider integrating with too.

We hadn't come across ForAllSecure before, so thanks for pointing them out. They do appear to be similar, but their focus seems to be on large commercial/enterprise projects in sectors like defence and aerospace. So maybe I'm wrong, but I don't think they have an offering for individuals / smaller teams.

On the logo point, as another commenter pointed out it's the mathematical forall symbol, so I guess we just both had the same thought when it came to coming up with a logo.

Post reply on HN