7 ms·

The Z3 Theorem Prover

jmartinpetersen 7y ago
I seem to have somehow forgotten or missed the fact that it was MIT re-licensed a couple of years ago, instead of the previous "no commercial use" stuff. Thanks for the submission!
hyper_reality 7y ago
I've used Z3 a lot for CTF challenges, but in my day-to-day work have never encountered any problems that it would be useful for. I'm interested to know how people have used it in the course of their work?
- glangdale 7y ago
  I have a super-optimizer for SIMD coding built out of Z3. It is not yet fit for public consumption, but I've already found some sequences faster than anything I had before, which is nice.
  - jfries 7y ago
    I would be super interested in more details on how that works. What do you actually pass to z3 to solve?
    - hairtuq 7y ago
      I wrote a superoptimizer using z3 here: https://github.com/falk-hueffner/sematrope https://github.com/falk-hueffner/sematrope . The idea is to have variables that encode the program and a giant if-then-else statement that represents program execution. Then for a list of input/output pairs you let the solver find a program encoding that yields correct outputs. Next you let the solver find a counterexample where the current program candidate does not give the correct result. If one is found, it is added to the list of input/output pairs, otherwise you have found a correct program.
      - pron 7y ago
        What if the solver both fails to find a counterexample and fails to conclude there isn't one? (i.e. it times out)
        hairtuq 7y ago
        That's very unlikely to happen, since finding a counterexample or proving there isn't one is much easier than finding a program candidate, so it'll usually time out in that phase.
        pron 7y ago
        OK, so what happens when it fails to find a candidate?
        glangdale 7y ago
        Then you learned something, I guess ("solving is hard"). I see a lot of timeouts with mine. Mine is 'easy' in that I'm looking for SIMD programs so the domain is essentially u8 "in lane only" SIMD code, so the small bit-width makes life easier.
        dhash 7y ago
        I write something similar for my own problems. Usually a single instance alone isn’t going to cut it, so we run a portfolio of solvers and treat it like a multi armed bandit problem as to choose which solver with its specific hyper parameters is finding solutions / counter examples faster. A pretty common trick when you do this is to dynamically resize your portfolio with new solvers introduced with a high likelihood of solving fast based off the parameters of other solvers that are solving fast, a particle filter of sorts. This takes care of setting and handling individual solver timeouts, while allowing the user to specify not only a timeout for the whole portfolio, possibly lengthening when new solvers are introduced, but also a max delay between any two solutions. Either way, you’re still forced to consider if the model can return sat or unsat, or a timeout. If it’s a timeout we don’t swap in the faster code, if it’s unsat then same deal, but if it’s sat we can get some new code to jump to
    - glangdale 7y ago
      User hairtuq gave a good summary. There seems to be a tension between pushing more work into the solver vs breaking up the problem into smaller sets, so there are many different designs. For example, I can pass thousands of candidate programs to the solver with opcodes specified ("please go get me some constants that make this program work for this task") or one completely unspecified program ("find me all the opcodes and all the programs") or some continuum between. My current experience is that partial specialization works well. I have a lot of optimizations I'd like to apply. I'm doing the slightly brain-melting task of trying to get the super-optimizer to cough up its own optimization rules to speed the process, but that's a long topic and I'll be a lot chattier about if I see it ever work properly. I'm also trying to figure out a way to make this pay in some fashion, being between jobs. Love to work on it more but I suspect reality will kick in soon.
  - microcolonel 7y ago
    There's also souper, which is a generic superoptimizing pass for LLVM which can use Z3 (or most other popular SMT solvers).
- pyb 7y ago
  How was Z3 useful for CTFs ?
  - 0xdada 7y ago
    You can solve many keygen type reverse engineering challenges with z3.
    - viraptor 7y ago
      I'd be interested in reading about it. Do you convert the core algorithm into solver rules to find any solution? Or something more complex?
      - 0xdada 7y ago
        Yes. It basically turns a reverse engineering task back into regular "forward" engineering, except you are programming with z3's symbolic variables. Here is an example: https://anee.me/solving-a-simple-crackme-using-z3-68c55af7f7b1 https://anee.me/solving-a-simple-crackme-using-z3-68c55af7f7...
- michael_fine 7y ago
  You can implement pretty powerful type checkers as constraint based systems. I used Z3 in a project called LightDP to verify differential privacy as a property of the type system.
- brians 7y ago
  I use it for running LARPs: characterize the roles to play, survey players to elicit constraints and preferences, and meet constraints while optimizing preferences. https://github.com/briansniffen/autocaster https://github.com/briansniffen/autocaster I did something similar for reassigning seats in my office—loud people together, someone who needs it near the restroom, people generally near their team leads, that sort of thing. Too much personal information to share here.
  - thanatropism 7y ago
    I've been wanting to write a DSL for solving room scheduling problems (and similar) with SAT (i.e. translate to DPLL). Put up a simple front-end, receives text that gets added to the constraint base. Your thing seems so much more powerful. I wonder if this UI idea would make it more usable. (Wait, are we reinventing expert systems?)
JohnStrangeII 7y ago
This is not really meant as a critique, more of a general suggestion for implementers to improve their docs. As someone who teaches logic and works with standard logics from time to time (HOL with Lambek Calculus, normal and classical modal logics, and plain old FOL), I've found it unnecessarily hard to figure out from the docs with what logics you can implement in them, whether you can just load these and use them, how to enter formulas, how to prove things, how to construct models, etc. This all seems overcomplicated in these tools, and almost all of them seem to mix up completely unrelated programming languages with logic. Couldn't this all be simpler? I understand that the typical use cases for these solvers are different. Still, I often wish there was a tool that I can just fire up, choose modal logic EMC from a menu and check whether a certain formula is a theorem. So far, it has always turned out easier for me to do this by hand than using a theorem prover.
- IvanK_net 7y ago
  "I often wish there was a tool that I can just fire up, choose modal logic EMC from a menu and check whether a certain formula is a theorem." We would not need any mathematicians then :D
- dhash 7y ago
  Yeah I wish there was a better logic chart than [1], or at least one that I can give it something in MSOL and it can internally compile it to a representation in one of those logics. [1] http://smtlib.cs.uiowa.edu/logics.shtml http://smtlib.cs.uiowa.edu/logics.shtml
siswoyo 7y ago
tokyo in kill godzila asksesseus in I tander in I godzila in I tokyo in godzila vs king kong
tiredneurons 7y ago
read this it's seriously good https://exhaustedneurons.github.io/abstractions/ https://exhaustedneurons.github.io/abstractions/
- gjm11 7y ago
  It's OK, I guess, but it has rather little to do with the subject here. If you want to publicize your blog here, please do it by submitting a link rather than by barging into a largely unrelated discussion to shout about how good your own blogpost is.
  - deleted 7y ago
    [deleted]
  - tiredneurons 7y ago
    okay

I seem to have somehow forgotten or missed the fact that it was MIT re-licensed a couple of years ago, instead of the previous "no commercial use" stuff. Thanks for the submission!

hyper_reality 7y ago

I've used Z3 a lot for CTF challenges, but in my day-to-day work have never encountered any problems that it would be useful for. I'm interested to know how people have used it in the course of their work?

glangdale 7y ago
I have a super-optimizer for SIMD coding built out of Z3. It is not yet fit for public consumption, but I've already found some sequences faster than anything I had before, which is nice.
- jfries 7y ago
  I would be super interested in more details on how that works. What do you actually pass to z3 to solve?
  - hairtuq 7y ago
    I wrote a superoptimizer using z3 here: https://github.com/falk-hueffner/sematrope https://github.com/falk-hueffner/sematrope . The idea is to have variables that encode the program and a giant if-then-else statement that represents program execution. Then for a list of input/output pairs you let the solver find a program encoding that yields correct outputs. Next you let the solver find a counterexample where the current program candidate does not give the correct result. If one is found, it is added to the list of input/output pairs, otherwise you have found a correct program.
    - pron 7y ago
      What if the solver both fails to find a counterexample and fails to conclude there isn't one? (i.e. it times out)
      - hairtuq 7y ago
        That's very unlikely to happen, since finding a counterexample or proving there isn't one is much easier than finding a program candidate, so it'll usually time out in that phase.
        pron 7y ago
        OK, so what happens when it fails to find a candidate?
        glangdale 7y ago
        Then you learned something, I guess ("solving is hard"). I see a lot of timeouts with mine. Mine is 'easy' in that I'm looking for SIMD programs so the domain is essentially u8 "in lane only" SIMD code, so the small bit-width makes life easier.
      - dhash 7y ago
        I write something similar for my own problems. Usually a single instance alone isn’t going to cut it, so we run a portfolio of solvers and treat it like a multi armed bandit problem as to choose which solver with its specific hyper parameters is finding solutions / counter examples faster. A pretty common trick when you do this is to dynamically resize your portfolio with new solvers introduced with a high likelihood of solving fast based off the parameters of other solvers that are solving fast, a particle filter of sorts. This takes care of setting and handling individual solver timeouts, while allowing the user to specify not only a timeout for the whole portfolio, possibly lengthening when new solvers are introduced, but also a max delay between any two solutions. Either way, you’re still forced to consider if the model can return sat or unsat, or a timeout. If it’s a timeout we don’t swap in the faster code, if it’s unsat then same deal, but if it’s sat we can get some new code to jump to
  - glangdale 7y ago
    User hairtuq gave a good summary. There seems to be a tension between pushing more work into the solver vs breaking up the problem into smaller sets, so there are many different designs. For example, I can pass thousands of candidate programs to the solver with opcodes specified ("please go get me some constants that make this program work for this task") or one completely unspecified program ("find me all the opcodes and all the programs") or some continuum between. My current experience is that partial specialization works well. I have a lot of optimizations I'd like to apply. I'm doing the slightly brain-melting task of trying to get the super-optimizer to cough up its own optimization rules to speed the process, but that's a long topic and I'll be a lot chattier about if I see it ever work properly. I'm also trying to figure out a way to make this pay in some fashion, being between jobs. Love to work on it more but I suspect reality will kick in soon.
- microcolonel 7y ago
  There's also souper, which is a generic superoptimizing pass for LLVM which can use Z3 (or most other popular SMT solvers).
pyb 7y ago
How was Z3 useful for CTFs ?
- 0xdada 7y ago
  You can solve many keygen type reverse engineering challenges with z3.
  - viraptor 7y ago
    I'd be interested in reading about it. Do you convert the core algorithm into solver rules to find any solution? Or something more complex?
    - 0xdada 7y ago
      Yes. It basically turns a reverse engineering task back into regular "forward" engineering, except you are programming with z3's symbolic variables. Here is an example: https://anee.me/solving-a-simple-crackme-using-z3-68c55af7f7b1 https://anee.me/solving-a-simple-crackme-using-z3-68c55af7f7...
michael_fine 7y ago
You can implement pretty powerful type checkers as constraint based systems. I used Z3 in a project called LightDP to verify differential privacy as a property of the type system.
brians 7y ago
I use it for running LARPs: characterize the roles to play, survey players to elicit constraints and preferences, and meet constraints while optimizing preferences. https://github.com/briansniffen/autocaster https://github.com/briansniffen/autocaster I did something similar for reassigning seats in my office—loud people together, someone who needs it near the restroom, people generally near their team leads, that sort of thing. Too much personal information to share here.
- thanatropism 7y ago
  I've been wanting to write a DSL for solving room scheduling problems (and similar) with SAT (i.e. translate to DPLL). Put up a simple front-end, receives text that gets added to the constraint base. Your thing seems so much more powerful. I wonder if this UI idea would make it more usable. (Wait, are we reinventing expert systems?)

JohnStrangeII 7y ago

This is not really meant as a critique, more of a general suggestion for implementers to improve their docs. As someone who teaches logic and works with standard logics from time to time (HOL with Lambek Calculus, normal and classical modal logics, and plain old FOL), I've found it unnecessarily hard to figure out from the docs with what logics you can implement in them, whether you can just load these and use them, how to enter formulas, how to prove things, how to construct models, etc. This all seems overcomplicated in these tools, and almost all of them seem to mix up completely unrelated programming languages with logic. Couldn't this all be simpler? I understand that the typical use cases for these solvers are different. Still, I often wish there was a tool that I can just fire up, choose modal logic EMC from a menu and check whether a certain formula is a theorem. So far, it has always turned out easier for me to do this by hand than using a theorem prover.

IvanK_net 7y ago
"I often wish there was a tool that I can just fire up, choose modal logic EMC from a menu and check whether a certain formula is a theorem." We would not need any mathematicians then :D
dhash 7y ago
Yeah I wish there was a better logic chart than [1], or at least one that I can give it something in MSOL and it can internally compile it to a representation in one of those logics. [1] http://smtlib.cs.uiowa.edu/logics.shtml http://smtlib.cs.uiowa.edu/logics.shtml

siswoyo 7y ago

tokyo in kill godzila asksesseus in I tander in I godzila in I tokyo in godzila vs king kong

tiredneurons 7y ago

read this it's seriously good https://exhaustedneurons.github.io/abstractions/ https://exhaustedneurons.github.io/abstractions/

gjm11 7y ago
It's OK, I guess, but it has rather little to do with the subject here. If you want to publicize your blog here, please do it by submitting a link rather than by barging into a largely unrelated discussion to shout about how good your own blogpost is.
- deleted 7y ago
  [deleted]
- tiredneurons 7y ago
  okay