SLAyer

by Tomte • 10 years ago

105 15 10 years ago

daveguy• 10 years ago

It is a tool for verifying memory safety from Microsoft under the MIT license.

1) From MS under the MIT license? What? Did MS abandon their proprietary open source licenses?

2) What is the significance of SLA? Service level agreement doesn't seem to fit. I thought it would be a tool for the facilitation of SLA (in terms of service duplication). I guess verifying program safety would improve uptime for each individual instance (but there's a whole lot more to it than that). Is that what this SLA refers to?

Edit: Thanks everyone for the clarifications! I knew SLA as service level agreement didn't fit. And @zamalek binging on open source hah! so punny.

Tomte• 10 years ago

"Separation Logic", no idea about the "A".

Maybe "analysis"?

zamalek• 10 years ago

Did MS abandon their proprietary open source licenses?

This is not new, Microsoft has been binging on open source lately (much to my glee). Many things on their GH org[1] are permissively licensed, including CoreCLR (the .Net runtime).

[1] https://github.com/Microsoft

tyingq• 10 years ago

What is the significance of SLA?

Guessing "Separation Logic-based Analyses": http://research.microsoft.com/pubs/163161/2012%20CAV%20Diagn...

moftz• 10 years ago

Formal verification of service level agreements and other contracts would be a pretty cool machine learning project.

saminishtiaq3• 10 years ago

1. MIT is the standard GitHub.com/Microsoft license. 2. SLAyer is an acronym of Separation Logic Analyzer. And also a reference to Josh's musical taste.

akavel2• 10 years ago

Is anyone aware what are the tool's limitations? Seems open-sourced ~1-2 months ago already, with publications history spanning much longer [1], but the README is very sparse, and I wouldn't probably understand much if I tried to dive into the research papers. Or am I to believe it will find 100% all memory issues?

[1] http://research.microsoft.com/en-us/projects/slayer/

saminishtiaq3• 10 years ago

It's a static analysis tool, so it has many TimeOut limitations :-) In practise, many abstract interpretation based tools generalize too much, lose too much information, then get lost and TO instead. The test suite released there gives a good empirical idea of what SLAyer can do. You'll see lots of while-loops over single- and doubly-linked lists as SLAyer can generalize Separation Logic points-to predicates to 'sll' list predicates.

akavel2• 10 years ago

I'm specifically interested here in what the tool cannot do, more than what it can do. For now all I can tell is it "works for some empirical cases, and maybe works in rest of cases, but not strictly defined, don't expect anything concrete".

nv-vn• 10 years ago

Anyone have more information for the NS library included in src/Lib? It looks very similar to Batteries or Core so I'm interested in why Microsoft chose to develop their own solution instead. Also, Microsoft hasn't released it as a separate library from SLAyer. Is the whole library being open sourced here (or are they only sharing a small part of it?)? And if so, why doesn't Microsoft create a new repository for it and publish it to OPAM?

saminishtiaq3• 10 years ago

NSLib was just a small modification (change argument orders, other HO functions for Map, etc)to the OCaml stdlib that SLAyer used. It's not essential or necessary here, should have been cleaned up before release.

nn3• 10 years ago

Here is a web demo for people to try it out (and actually some documentation)

http://research.microsoft.com/en-us/projects/slayer/

From some quick experiments it seems to be weak on malloc, no problem with:

int main() { char *p = malloc(1); p--; free(p); }

rochacbruno• 10 years ago

If a successful metal band tries to change its name to e.g: "Active Directory of Hell", "SQL Server No More" or something like this, for sure Microsoft lawyers would do something against. Now I think Tom Araya from Slayer should do it against microsoft. It is a trademark from hell.

dsp1234• 10 years ago

Unless Active Directory or SQL Server are trademarked names in the music category, there isn't much they could do. There is no possibility of confusion.

Just as there is no possibility of confusion that this software was written by the band Slayer, or is even endorsed by them.

Although, 'They official C formal verification tool of the band Slayer' would be a pretty funny tie in.

krylon• 10 years ago

Who doesn't love a good pun? As a a Slayer fan, programmer and Windows admin, I really dig the name. ;-)

In "I Sing The Body Electronic", Fred Moody describes Alice Cooper visiting the Microsoft campus (which is home to a fair share of metal heads, apparently). "Why are you guys called Microsoft? Wouldn't you rather be called Macro-Hard?"

The same book also mentions a programmer having to work the weekend before Encarta is shipped, because a freelance programmer put an article titled "Slayer sucks like vacuum" in it. So, historically speaking, this kind of evens things out. ;-)

SLAyer

Related Stories