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

The Z3 theorem prover is now open source

research.microsoft.com

Post reply on HN
Print view View original

41–50 of 77 posts

Re: The Z3 theorem prover is now open source

#41

Post by krenoten »

tptacek wrote: post #39
wiradikusuma wrote: post #15

Earlier quoted context omitted.

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

Solvers are somewhat popular in software security, both for automatically uncovering invariants (and exploitable lack of invariants), and also for modeling program binaries and solving for collections of basic blocks that can executed during a memory corruption attack to accomplish attacker goals.

Things like automatic exploit generation[1] and exploit hardening[2] in particular rely on SMT solvers to accomplish their goals. They allow for some truly remarkable things to be done. Expect skynet to utilize them heavily in its distributed automatic exploit generation (global autopwn) tooling!

1. http://security.ece.cmu.edu/aeg/ 2. http://users.ece.cmu.edu/~ejschwar/bib/schwartz_2011_rop-abs...

Re: The Z3 theorem prover is now open source

#42

Post by PhantomLobe »

seanmcdirmid wrote: post #36
josephlord wrote: post #35

Earlier quoted context omitted.

GPL has no restrictions at all on commercial use and in commercial use places no obligations on you at all. If you distribute GPL code you then become subject to its restrictions and must provide the code.

Sure, I'm aware of this. My point was that GPL is almost as poisonous as a non commercial use restriction in terms of distributing software. GPL works great on the server where this isn't a concern, but doesn't work for almost any other commercial use case. Very arbitrary but at least very clear.

It's not even close. At work I run Python, Eclipse, Coq, various Linux and in general a lot of real Open Source software of a variety of licenses. Apparently I cannot use Z3, be it sources or binary, as my company happens to have commercial intentions.

AFAIK the MS license restricts usage, not only distribution. That's plain wrong.

Re: The Z3 theorem prover is now open source

#43

Post by josephlord »

seanmcdirmid wrote: post #36
josephlord wrote: post #35

Earlier quoted context omitted.

GPL has no restrictions at all on commercial use and in commercial use places no obligations on you at all. If you distribute GPL code you then become subject to its restrictions and must provide the code.

Sure, I'm aware of this. My point was that GPL is almost as poisonous as a non commercial use restriction in terms of distributing software. GPL works great on the server where this isn't a concern, but doesn't work for almost any other commercial use case. Very arbitrary but at least very clear.

You seem to have a VERY narrow definition of commercial use which involves selling software or being a software service provider. There are a vast majority of companies manufacturing/distributing/retailing and providing services for whom the GPL imposes no restriction at all. The MS release seems to prevent all commercial use not just commercial redistribution/binary release making it a FAR broader restriction than the GPL.

For MS and a surprisingly small (in terms of total global economy) number of other businesses selling closed source software (or software dependent on other non-Free software components) the GPL imposes very real restrictions.

I would argue that they are in no way arbitrary but have a clear purpose and objective to further increase the amount of Free software in the world. You may or may not support or want to assist this objective but it certainly doesn't feel arbitrary to me (I've taken the 'capricious; unreasonable; unsupported' definition of arbitrary from Dictionary.com as my interpretation of your meaning).

Edit/reply:

Can't reply to you for some reason. No citation but you have missed my point. I wasn't comparing Open Source Industry to closed source software industry but really the software industry to ALL Other industries (and individuals) in the world. Basically software consumers rather than producers (of which closed source companies like MS form a large part).

Re: The Z3 theorem prover is now open source

#44

Post by ufo »

wiradikusuma wrote: post #15
ot wrote: post #4

This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it! Some context, as not everybody may have heard about it. Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver. You can play with it online using its Lisp-l…

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

Are you familiar on how you can use SAT solvers to solve a wide variety of constraint problems?

https://github.com/hugomg/hexiom

SMT solvers basically extend SAT solvers to allow you to work directly with other theories (linear inequalities, bit arrays, etc) without being forced to encode this as the booloean formulas that basic SAT understand. The idea is that dealing with the higher level details directly instead of having to convert tihngs to a commo low level makes it simpler to express things and can also allow for custumized optimizations and algorithms?

Re: The Z3 theorem prover is now open source

#45

Post by iy56 »

nitrogen wrote: post #37
hermanhermitage wrote: post #16

Earlier quoted context omitted.

No. This is a fantasy. A trademark does not take ownership of general words or phrases from the people.

A trademark does not take ownership of general words or phrases from the people. Except when that trademark is "Windows" or "Office" or "Word".

When you ask your officemate to open the window, does legal tell you to stop saying that Word(TM) because you're not using it according to the way Microsoft defined it?

Re: The Z3 theorem prover is now open source

#46

Post by ot »

olliesaunders wrote: post #28
ot wrote: post #4

This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it! Some context, as not everybody may have heard about it. Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver. You can play with it online using its Lisp-l…

It seems its only free for non-commercial use, ergo not free.

You are absolutely right. I was excited because I can finally read the code and learn something from it.

But of course the implication "open source -> I can use it anywhere I want" is broken in this case. The author should have been a little more careful in not abusing that term, even if this was posted on his blog.

I am well aware of that licence, I myself had to use it for some code I wrote while at MSR [1]. I was not happy at all about the non-commercial clause, but it was either that or not releasing the code. I guess the same happened here.

[1] https://github.com/ot/path_decomposed_tries/blob/master/LICE...

Re: The Z3 theorem prover is now open source

#47

Post by dagw »

josephlord wrote: post #35
seanmcdirmid wrote: post #12

Earlier quoted context omitted.

Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation. Full disclosure, I work for Microsoft.

GPL has no restrictions at all on commercial use and in commercial use places no obligations on you at all. If you distribute GPL code you then become subject to its restrictions and must provide the code.

However many large companies have a no GPL policy. I did a little bit of work for a large multinational engineering company most of you have heard of and was told in no uncertain terms that I was not allowed to use any GPLed code anywhere in anything I delivered. They also had a large document they made me read which listed dozens of licenses and exacting details over how I was and wasn't allowed to use software under those licenses.

Re: The Z3 theorem prover is now open source

#48

Post by nitrogen »

iy56 wrote: post #45
nitrogen wrote: post #37

Earlier quoted context omitted.

A trademark does not take ownership of general words or phrases from the people. Except when that trademark is "Windows" or "Office" or "Word".

When you ask your officemate to open the window, does legal tell you to stop saying that Word(TM) because you're not using it according to the way Microsoft defined it?

No, but if I hypothetically created and started describing a graphical windowing system as a "Windows," and a word processor as a "Word," Microsoft would surely complain. It seems a bit hypocritical to complain about others' dilution of Microsoft's own marks, but then dilute others' marks in return.

This is a bit of a digression from the original topic, but seems tangentially relevant given that we're talking about Microsoft accidentally misusing or deliberately abusing a term that has an accepted meaning in the marketplace, the very purpose for which trademarks were created.

[Also, I should have added the following disclaimer to the previous comment: Disclaimer: Long ago, in a galaxy far away, I worked for a company that seemed to have a chance at invalidating the Windows trademark, but when Microsoft offered a large settlement, my former employer took the money and ran.]

Re: The Z3 theorem prover is now open source

#49

Post by seanmcdirmid »

josephlord wrote: post #43
seanmcdirmid wrote: post #36

Earlier quoted context omitted.

Sure, I'm aware of this. My point was that GPL is almost as poisonous as a non commercial use restriction in terms of distributing software. GPL works great on the server where this isn't a concern, but doesn't work for almost any other commercial use case. Very arbitrary but at least very clear.

You seem to have a VERY narrow definition of commercial use which involves selling software or being a software service provider. There are a vast majority of companies manufacturing/distributing/retailing and providing services for whom the GPL imposes no restriction at all. The MS release seems to prevent all commercial use not just commercial redistribution/binary release making it a FAR broader restriction than t…

Citation needed on how the open source software industry is so much larger (money wise) than the closed source software industry. I'm sure its much more of a mix, plus closed source software is more often sold, meaning more money is involved in say oracle DB vs. MySQL. Also, most of the OSS industry prefers apache/BSD style licenses that aren't viral.

If RMS was true to his principles, he would make GPL more viral to cover every deployment and co-deployment. But they leave this huge server hole instead. That is what I mean by arbitrary. Why a hole there and not elsewhere?

Re: The Z3 theorem prover is now open source

#50

Post by josephlord »

dagw wrote: post #47
josephlord wrote: post #35

Earlier quoted context omitted.

GPL has no restrictions at all on commercial use and in commercial use places no obligations on you at all. If you distribute GPL code you then become subject to its restrictions and must provide the code.

However many large companies have a no GPL policy. I did a little bit of work for a large multinational engineering company most of you have heard of and was told in no uncertain terms that I was not allowed to use any GPLed code anywhere in anything I delivered. They also had a large document they made me read which listed dozens of licenses and exacting details over how I was and wasn't allowed to use software unde…

But could you use GPL software to produce what you delivered (rather than as part of it)? If not were Linux, Emacs and use of Android phones for any work banned?

If they were banned because of the GPL the company was doing its own stupid rules completely unrelated to the restrictions imposed by the GPL. If they weren't then it shows the difference between the GPL and the non-commercial use term of this particular MS license.

Post reply on HN