The Z3 theorem prover is now open source | Hacker News Reader

The Z3 theorem prover is now open source

research.microsoft.com

137 pointstaocp74 comments

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-like native language [2] or using the Python bindings [3]

The reason SMT is important is that several static analysis tools work by encoding the program constraints (such as pre/post conditions, invariants, ...) into a big formula. The satisfiability of this formula determines the correctness of the program, and sometimes assignments can be translated back to counterexamples to program correctness.

[1] http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories

[2] http://rise4fun.com/Z3/bit-count

[3] http://rise4fun.com/Z3Py/nonlinear

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

Planning problems can be encoded as SAT problems, for instance.

another example: package dependencies resolution on Linux distributions.

This can far more easily be done by topological sorting.

That's not actually sufficient when you consider version requirements; for example requiring a specific range of libc or the like.

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...

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?

I have only made light contact with SMTs in my explorations but SMT solvers have massive applicability. They're used in theorem proving - verification, dependent typing, contracts - scheduling, planning, and for understanding/modelling cell regulatory networks in biology.

Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (just as linear programming shows just cause something is in P doesn't mean it is 'easy' - for large values of easy). To ground the concept you can roughly categorize it with logic programming, answer set programming, constraint satisfaction and integer programming. I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.

> I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.

I suppose it depends on what you mean by flexible. I would say that ASP is more flexible as a modeling language—you can specify all sorts of logic and constraints in it in a fairly expressive logical formalism, with both generative (Prolog-like) and constraint-oriented (CSP-like) language constructs. Particularly with the extensions the Potassco people have been making in their version: http://potassco.sourceforge.net/

However, current ASP solvers ground to variable-free (propositional) programs before solving, which means they blow up on large-ish integer domains, since you end up propositionalizing the whole integer range. I've had some examples where just grounding out the problem takes ages, but then it's nearly instant to solve once the grounding is done. SMT avoids that by providing a way to ground "modulo" a domain theory, rather than fully grounding, with a theory of integers being a common example.

Awesome response thanks. The increased ease of use for modeling is part of why I decided on it rather than an SMT solver. One should prefer ASP wherever the assumptions hold. I use(d) DLV-Complex but will check your link.

But right, by more flexible I meant the availability of quantifiers in SMT solvers.

They can be used for program synthesis. That is, given some high-level specification, you can use an SMT solver to generate code fitting that specification. You can also use them to verify that some code does fit a specification and, if it doesn't, to find the part of the code causing the actual problem (the minimal unsat core).

A particular example would be to take some existing code with holes (just parts left out) and some assertions about the code's behavior, encode both as logic formulas and try to find a satisfying assignment for the holes. When you have a possible assignment, you can verify it with the same encoding. You can then use the satisfying assignment to fill in the holes in the initial program, which are ideally very tedious to code by hand.

Various forms of program analysis/verification. Some examples of applications where SMT is heavily used are automated theorem provers, symbolic execution engines, model checking tools.

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...

> When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it!

It has already been pointed out that they didn't open-source Z3, they just made the source code available under the same license the binary already was. I would add that they have been selling Z3 for a long time:

http://www.microsoftstore.com/store/msstore/en_US/pd/product...

It has been there since 2011 according to my “archives”:

http://blog.frama-c.com/index.php?post/2011/12/23/Z3-in-Micr...

The limitation to non-commercial use means it's not quite 'open source' in the common meaning established by the Open Source Initiative. (Discrimination against a 'field of endeavor', such as business use, is not allowable under their definition.)

The no commercial use thing is Microsoft speak for "We couldn't figure out how to make money with it, but if you do, give it to me."

cough http://creativecommons.org/licenses/by-nc/2.0/

It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.

Thanks both for pointing this out - I've left a comment on the blog post asking him to change "open source" to "shared source" (which is what I thought Microsoft call such visible but not open code).

I'll give Leonardo the benefit of the doubt that he's just made an error for now...

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.

Open Source a term with a single, specific definition.

It is damaging to the ideas of FLOSS to allow stuff like "shared source" to be called open source.

EDIT: Removed reference to "open source" being trademarked, it is in fact not, apologies for the confusion.

No. This is a fantasy.

A trademark does not take ownership of general words or phrases from the people.

Correct. A trademark is just that: a mark used in trade. It does not come with the ability to define a standard definition for the mark's meaning, other than "~ is a trademark of $ORGANISATION".

Also, is "open source" really trademarked? Wtf? That's like a beef promo organisation trademarking "well done".

The problem with this idea when applied to this case is the motivations of people wishing to use some alternate definition. There is a real profit motive in being able to call stuff "open source" when it doesn't grant its users the same kind of freedoms the BSD or the GPL license, etc, do.

If you allow stuff like "shared source" to be called open source, you reduce the term to a meaningless buzzword, like how the term "open" is frequently abused.

citing trademarks is a heavy handed approach, but many parties with a profit motive don't care about anything except strict legality.

This is relevant in particular to this blog because Microsoft has a history of attempting to change what the term means

http://opensource.org/node/280

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.]

Window managers are still commonly called window managers today. Word processors are still called word processors. That's the point - Microsoft hasn't taken away these generic terms. No, you can't call your competing product the exact same thing they call theirs. Why should you be able to? That'd be retarded.

No, you can't call your competing product the exact same thing they call theirs.

Likewise, it is reasonable that Microsoft can't call their competing license "open source" when that term already has an established commercial definition and trademark with a specific set of consumer expectations.

Further, until a tradmeark is filed or established by extensive use, competing products can use similar words in their titles. Once upon a time you could have had Microsoft Windows, OpenWindows, the comp.windows.x newsgroup (suggesting that X is a subset of the generic category of "Windows"), etc. Now they will sue if your OS name even rhymes with Windows.

Agreed. But that's all very general stuff. Nothing there so much as hints at special treatment for MS's trademarks specifically, which is what I was initially objecting to.

Microsoft trying to hijack a term with an already fully established meaning is dishonest and screws up everything. This may be an honest mistake by an employee that fell for Microsoft's own marketing, but it's still not right to spread misinformation. Is the license on this list [1]? Then it's almost certainly not open source. Also, this particular license has already been rejected by OSI.

The GPL is not the only open source license. It may screw up certain commercial usage, but it never stops users from forking the software. This Microsoft license does.

1. http://opensource.org/

Er, technically this license doesn't stop forks -- they are explicitly allowed -- but it definitely propagates the non-commercial clause. I agree, it's definitely not Open Source.

I meant that it doesn't allow arbitrary forking. There are cases in which it's illegal to keep using it, whereas with the GPL at most you'd have to release the derivative source to your (paying) users.

> Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions.

The GPL has a few problems, but non-commercial causes are just noxious.

Who exactly can use a non-commercial piece of software? Presumably, universities can. Can a government research lab use it? How about a military research lab? What about a contractor doing military R&D? If Exon-Mobile uses this to search for oil, is this research (thus non-commercial)?

Any clause which is likely to give your lawyer a headache trying to interpret it is probably a bad license.

The GPL has some ambiguous bits (like its interaction with interpreted code eg Python bindings to MySQL and Javascript libraries in the browser) but it's not as ugly as the term Non-Commercial.

Actually, interpreted code or browser code isn't really ambiguous. GPL is based on "derivative works" not necessarily C-style linking.

Is progressive enhancement of a HTML page enough to make the rest of the frontend "derivative"? What about the backend? What if they interact?

If the JS engine mixes interpreted code with the proprietary DOM, how does that work?

How about LGPL works?

But you're right - it's usually pretty clear if you think about it. There will always be edge-cases, but unlike non-commercial clauses the edge cases aren't that common.

Just about everyone who uses the term "open source" or "free software" would read "the source code can be used for non-commerical purposes" to mean "not open source".

There is basically no disagreement about what counts as an open source/free software licence. This licence is not that.

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).

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?

I don't say anything of the sort. Please read again. I am saying that total global commerce and use of computers is greater than the software industry (not the world's greatest insight I know).

Don't want to answer for RMS. I can't think of less arbitrary way of achieving their aims.

RMS didn't foresee the server hole. That's why GNU came out with the Affero GPL in 2007: http://www.gnu.org/licenses/agpl-3.0.html

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.

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.

Why do you think they are "simply lying", rather than (for example) being simply mistaken?

Because they've been trying to dilute the term "open source" for quite a while now.

1997 called and &c &c. Microsoft could give a shit about damaging "open source".

Those bastards. How dare they publish their source code on terms we don't agree with.

The post you are replying to and its parent are not disagreeing with the terms the source code was published under.

Go read them again and find where they disagree with the terms.

They do disagree with the way those terms are _described_. "Open source" has a fairly well defined meaning and that meaning excludes a license that restricts use based on "field of endeavour", which the license in question does.

This is also completely different from the GPL. The GPL does not restrict commercial use. I can use the GPLed linux kernel to serve up commercial websites all day. Presumably I could not use Z3 to serve a commercial service.

Non-commercial only. There are several similar projects some of which are really open source: http://smtlib.cs.uiowa.edu/solvers.html

Sadly, none as good as Z3. I'd want to study Z3, even if I'd rather use something else. The current license is good enough for studying.

I think one of the problems with it not being true open source is that they are selling a commercial version @ the microsoft store for 14,950. I suspect this is why they choose this license.

I'd be interested if they would provide different terms for the source for the people that bought the commercial version, or if you would just be stuck with the binaries.

Here is the link to buy the commercial version: http://www.microsoftstore.com/store/msstore/pd/Microsoft-Res...

It seemed really exciting until I realized that it is only available for non-commercial purposes.

IMO it's still exciting. Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from.

And it means that it can be ported to platforms it's currently not available for.

> Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from.

As long as nobody sees you, otherwise you are vulnerable to a lawsuit. If I had serious plans to make my own implementation I would purposefully avoid even running this program.

Right, if you intend to make your own implementation and profit from it, it's wise to avoid it. But for the rest of us it isn't that black and white...

Do you think Microsoft will be around in 10-20 years? Do you have a good idea of what you'll be working on (or interested in) in 10-20 years? Do you think laws regarding the forms of IP will be much better in 10-20 years? Do you think you'd get caught now or in the next 10-20 years if you do use this as research (or even rip code directly from it) and get sued for making money off it? Plug in your guestimations and make a decision. I looked at it, myself.

That's excellent (good to learn from, shame it's only non commercial; it's a step forward though)! I was accidentally checking rise4fun for open source just last week. I hope they open source more; unfortunately the project I'm most curious about at the moment (quickcode) will not be open sourced as it is officially part of Excel now.

As a plain old programmer, would a tool like this be useful to me? How can I use a theorem prover to improve my code, or make it easier to write my code on a day to day basis? I've heard that Z3 is used for demonstrating security properties, how would I apply this to ensure my own systems are secure?

Wish someone would update the topic here, since it's not open source as per the generally understood definition ... (as the article's source has updated / corrected on his blog)

Anyone able to find a link to the code? I have been looking around but I can only seem to find the binaries.

It's on codeplex http://z3.codeplex.com/SourceControl/changeset/view/9823ee3b...

People bitching about MS misusing the term "open-source" are, IMO, ungrateful SOBs who have never attempted to implement a non-trivial algorithm based on nothing but a stack of academic papers.

For me, the greatest value in having the source is to learn from it, not to hijack it.

I think a lot of people appreciate the move MS made while simultaneously condemning them for their casual appropriation of a term having a well-established meaning. They've updated the blog post in the meantime, so this is a non-issue.

Resorting to ad-hominems does nothing to strengthen your argument, btw.

Care to show some signs of appreciation by those who complain?

Could this be used to tes ZED models?

From the license text:

> Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose.

The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware.

> [A]ny feedback about the Software provided by you to us is voluntarily given, and Microsoft shall be free to use the feedback as it sees fit without obligation or restriction of any kind, even if the feedback is designated by you as confidential.

This I don't get. Why would MSFT want to publish confidential feedback?

> That if you breach this MSR-LA or if you sue anyone over patents that you think may apply to or read on the Software or anyone's use of the Software, this MSR-LA (and your license and rights obtained herein) terminate automatically. Upon any such termination, you shall destroy all of your copies of the Software immediately. Sections 3, 4, 5, 6, 7, 8, 11 and 12 of this MSR-LA shall survive any termination of this MSR-LA.

This part I certainly understand. "Sue us and you can't use our toys anymore."

> That the patent rights, if any, granted to you in this MSR-LA only apply to the Software, not to any derivative works you make.

This, again, is unsurprising, but good to keep in mind.

The feedback thing is probably along the lines of not wanting to have to have internal controls to deal with confidential information in their feedback processing.

The 'confidential feedback' boilerplate language would especially apply to projects with potential security implications. Your 'confidential feedback' might be disclosure of a security vulnerability and they'd want to choose to patch or not patch and publicly divulge or not divulge the vulnerability your feedback reveals.

> The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware.

MSFT claims a non-exclusive right to use your modifications.

Reply on news.ycombinator.com