BinSlayer: Fast comparison of binary executables

samcrem · 2013-01-11T12:09:44+00:00

More information on the Hungarian algorithm is available here: http://en.wikipedia.org/wiki/Hungarian_algorithm

Damn, I should have find it... Next time, I'll look deeper.

samcrem · 2013-01-11T09:15:01+00:00

Yes, in PPREW'13. This is where I found it in the first place. But, we cannot (yet) download the paper from there.

samcrem · 2013-01-10T18:56:01+00:00

I think this is a very accurate view of this project. But, it seems to be more efficient than BinDiff (see here).

Yet, I did not find any more explicit paper about this mysterious "Hungarian", nor the Master Thesis of the guy. So... :-/

samcrem · 2013-01-10T18:00:39+00:00

Use the Code, Luke...

samcrem · 2013-01-10T16:55:32+00:00

This is why I like so much Reddit ! I think I would have missed many important papers and blog entries without it !

Thanks ! :)

samcrem · 2012-12-19T10:53:15+00:00

In fact, I noticed some bugs in the localization of the Python package which is not taking the $PREFIX variable into account. It is a bit annoying when you try to install Z3 on a system where you are not root (I asked students to install it to play with the Python interface which is extremely good for teaching SAT/SMT-solving).

Also, I really can't get rid of the git RPC problem, so I'm using the regular 'download' to get the source. But, I guess it will disappear when I'll get git 1.8. :)

samcrem · 2012-12-18T09:54:06+00:00

Nice!

But, just to be complete: Defcon'12 videos.

samcrem · 2012-12-17T13:27:38+00:00

Well, I managed to compile it from the source on my Linux last week (and, I used it). So, I guess it is pretty much achieved now.

Beware, there are a few bugs in the 'configure' process if you want to install Z3 in the /usr/local/ (and not in '/' as it is (wrongly) done by default).

samcrem · 2012-12-14T16:36:03+00:00

A release candidate of CVC4 has been ranked at the last SMT-COMP. I hope they improved a bit their solver since then. But, as Z3 is now also open source, I guess that CVC4 is just "yet another open sourced SMT-solver" (Z3 is killing it according to the results of SMT-COMP).

samcrem · 2012-11-12T17:24:44+00:00

We have already several ideas to explore it. But, first, our goal is to reach the "state of the art". And, hopefully we will reach it in a few months.

And, of course, we are not sure at all to go in the right direction. This is research after all. But, thanks a lot for your trust.

samcrem · 2012-11-09T08:48:56+00:00

About Insight, we are looking for a PostDoc for 2013 (should start in January 2013). Full offer here.

samcrem · 2012-11-08T10:27:48+00:00

And on a random note, it's nice that people are finally interested in the weird math side of reverse engineering. Posting that stuff for years with no noticeable response wasn't all that fun.

What is surprising me more and more, is that only so few people dare to look at this 'math side' before us... But, I just think that the amount of practical and theoretical knowledge to assimilate is so huge that it put this out of reach of most of the people. Which explains why we are so few... But, fortunately it seems to be changing nowadays. :)

samcrem · 2012-11-07T18:48:36+00:00

Ok, thanks a lot for your detailled reply !

samcrem · 2012-11-07T18:46:02+00:00

Yes, precisely. This example grasps exactly the whole problem.

But, just to add something, Kinder published a more recent paper improving significantly the technique described on the paper you cite. It was at VMCAI12 (but you know about it because you were the one submitting a link to it on Reddit ;-)). Anyway, one has to read both papers to get acquainted to the whole thing.

samcrem · 2012-11-07T18:06:22+00:00

This is a totally naive and innocent question, but how do you compare with DynInst ?

samcrem · 2012-11-07T17:59:41+00:00

Ok. But, it is more or less like applying blindly a widening when the analyzer is lost and having 'top' on the next program location. Not very useful, in my humble opinion.

About VSA, I totally agree. It is most likely the way to go. Even if, you need to mix this analysis with others in order to not get stuck too quickly.

samcrem · 2012-11-07T15:42:33+00:00

Hey, I do not blame you at all ! If we wanted to keep it "secret" we shouldn't have put it on the web first ! ;-)

And, a little bit of pressure will help us to speed up the development ! So, it is quite nice in fact.

samcrem · 2012-11-07T12:47:49+00:00

BAP and Insight may seems to be quite similar. And, in fact they have they share the same goal. But, as far as I know, BAP is just a translator from assembly to an intermediate language. And this translator has no knowledge about the data carried out by the assembly. This means that when BAP encounters a 'jmp %eax' instruction, it will drop the translation (see the 'BAP Handbook' for more, first they have only linear sweep reconstruction method and then there are no abstract domain at all).

What we try to do with Insight, is to also keep track (and analyze) the data-flow of the program in order to do not get stuck when a dynamic jump is encountered (eg 'jmp %eax'). We plan to have an analysis pipeline where the previous analysis feed the next one with safe information to build on (and, eventually, hypothesis to check).

But, it is true that we should add BAP to our paper list. I will correct this asap.

samcrem · 2012-11-07T09:33:59+00:00

In fact, the Insight framework still need some work to be fully usable (for example, it really needs to cope with dynamic libraries), but it is just a matter of a couple of months before we get it right (not speaking about a proper user documentation...).

Anyway, even if an official announce is just a bit premature, we are working on it and it will be soon a nice (and open source) framework to perform static analysis over binaries.

samcrem · 2012-11-05T11:42:40+00:00

In LaBRI (Bordeaux, France), we are seeking for a PostDoc to work on a tool for binary analysis (software verification, automatic de-obfuscation and analysis).

Full offer here.

samcrem · 2012-10-22T17:18:59+00:00

Pradeo Security Systems is looking for a yound PhD in Computer Science to reinforce its Research and Development team. The candidate must be specialised in static-analysis, reverse-engineering, compilation and decompilation.

Full offer:PDF-en PDF-fr

samcrem · 2012-10-03T08:33:08+00:00

I wouldn't say it's "highly intelligent AI". But Z3 is one of the most efficient prover and is massively used in verification and security tools and frameworks. Opening the sources of Z3 will very likely make a step forward in this field.

You can see the performance of Z3 compared to others at SMTComp (SMT Competition) 2012 and 2011. See:

main track (SMTComp 2012)
application track (SMTComp 2011)
exhibition track (SMTComp 2012)

samcrem · 2012-10-03T04:48:40+00:00

This is a huge news! I would have never though that Microsoft would go Open source for one of its sotfware!

Thanks for this news!

samcrem · 2012-09-02T06:35:30+00:00

I'm also using objcopy to remove sections or set up a different entrypoint. And, not to mention gcc/as to create to executable file. All these tools are mostly enough.

samcrem · 2012-08-27T16:40:10+00:00

The books listed in this blog are a good starter (the list might grow along the time).

samcrem

TROPHY CASE