Hacker News Reader

Comment by tptacek | Hacker News Reader

If people are using this for interesting projects, I'd love some details.

Last week I wrote a fun tool using it (actually, any SMT-LIB 2 compatible solver, of which Z3 seems to be the only open-source-ish one that works out of the box) to search for optimal branch-free load-free C implementations of small integer lookup tables (i.e. something the compiler should do but doesn't). It's really a minimal use of an SMT solver, but it saved me from having to think of a more clever algorithm than brute force.

Did you publish the source anywhere, and if not, are you willing and able to? I'd love to see it.

Sure, I see no reason to keep it private: http://hub.darcs.net/squirrel/luts

(Note: it's a very hacked-together Prolog script. I wrote it in about 15 minutes in a fit of inspiration and free time. If it's useful to anyone I'll clean it up and add the features I enumerated in the README.)

How it works:

The input to the algorithm is the look-up table you want to optimize. I've mostly tested with a half-dozen or so pairs of small (1 or 2 digit) integers, as that is my use case. (Anything else is probably better served by an actual look-up table or binary branch tree.) Input values left out of the this table are considered "don't care" (i.e. there's no "default" output).

The Prolog portion just generates, via iterative-deepening, bit-arithmetic expressions. These expressions have as terminals the input variable (in theory, there could be multiple input variables; haven't tried this) and arbitrary (i.e. symbolic) named constants.

The expressions are, in turn, fed as-is to Z3 as a function over bit-vectors (note the constants are still arbitrary). The look-up table is fed to Z3 as a set of assertions about this function. Z3 is asked to prove (un)satisfiability; if the problem is satisfiable, (this is the important part!) it returns the values of the constants which make it satisfiable. These values are substituted in the original expression, which is then returned by the Prolog script as a solution.

I'd also love to see this; or, if it would be easier for you, I'd love to see a longer comment where you explain it in more detail.

See my reply to throwaway812 (which I'm updating with an explanation).

In case you or someone else is still looking, CVC4 [1] is a competitive open source alternative to Z3 or Yices.

[1] http://cvc4.cs.nyu.edu/

Thanks! Last I checked (maybe a year back), something-or-other about CVC4 didn't work for me (I wholly forget what it was). I will try it out again.

I don't know if you are associated with CVC4 at all, but unfortunately the hashes of the amd64 Debian stable packages (cvc4, libcvc4-1, and libcvc4parser1) don't seem to match? It is probably just a package error however it makes me hesitant to install the packages…

I am not associated with CVC4 directly (or Z3 for that matter). Something that is true for all these tools is that they evolve very quickly. As a result, you're better off building from source. In both cases, that means running `make` and nothing else.

You could start by quickly browsing through the huge list of papers that cite Z3 [1].

Microsoft uses Z3 extensively for bug finding for all sort of products, notably through the SAGE tool. There is a great write up on its impact. [2]

From that paper:

"Finding all these bugs has saved millions of dollars to Microsoft, as well as to the world in time and energy, by avoiding expensive security patches to more than 1 billion PCs. The software running on your PC has been affected by SAGE. Since 2008, SAGE has been running 24/7 on an average of 100-plus machines/cores automatically fuzzing hundreds of applications in Microsoft security testing labs. This is more than 300 machine- years and the largest computational usage ever for any SMT (Satisfiability Modulo Theories) solver, with more than 1 billion constraints processed to date. SAGE is so effective at finding bugs that, for the first time, we faced “bug triage” issues with dynamic test generation."

[1] http://scholar.google.com/scholar?cites=4828743947843773221&...

[2] http://dl.acm.org/citation.cfm?id=2094081

I'm definitely familiar with Z3 and with solvers used offensively and defensively in software security. I'm just curious as to how widespread it's become with generalist software developers as a problem solving tool.

These are great links; thanks for posting them.

Do you have any links for using Z3 in security proofs?

Not about Z3 in particular, but a very interesting application of solvers:

This weblog talks about procedural content generation (PCG) for games: http://www.gamesbyangelina.org/

It's used in some roguelike games to make sure the procedurally generated levels/rooms are playable/winnable.

It's also used in puzzle games where constraints are set for a certain puzzle level to exhibit certain characteristics in the puzzle solution, but the puzzle itself is randomly generated according to these constraints.

There's a couple of articles about constraint solvers on that site, but I remember this one was most striking: http://www.gamesbyangelina.org/2013/06/the-saturday-paper-go...

Another reply (can't edit my original reply now): what I have not done, though will if I ever have the chance again, is to prove correctness of bit-arithmetic libraries (e.g. for use with symbolic execution).

So long as you can represent your function in the SMT-LIB language (easy for this class of problem), you can prove properties of your code by asserting their respective negations in Z3 and asking it to prove satisfiability. If one of these properties doesn't hold, Z3 will tell you, and it will give you an example.

http://bugchecker.net is a site that does automated testing (dynamic analysis). We use STP.

The small project i'm developing for my Phd, "Symbolic Exploit Assistant" [1] (SEA) is using it.

[1] https://github.com/neuromancer/sea

There's a stack of software verification projects, most probably using Z3, here - http://www.rise4fun.com/

Reply on news.ycombinator.com