# CCC Camp’11

In case you’ve missed it, the CCC Camp was a great opportunity to meet people both working in security and otherwise. I have even met a very kind Taiwanese researcher who worked on SAT and GrÃ¶bner basis: in fact, if you haven’t had the chance to read this paper, I highly recommend it. A set of kind Taiwanese researchers recommended this paper to me, and I think it’s the most interesting SAT paper I have read in the past year.

We at SRLabs have made two releases during this camp, one that breaks GPRS encryption, and one that breaks smart card ROM encryption. I was involved with the first release, essentially working on the crypto part. In case you are interested in the videos, the one on GPRS is uploaded here, and the one on smart card ROM encryption is here. This reminds me of something: the videos from the MIT SAT/SMT Summer School are missing :( Well, given my fail there, maybe that’s a good thing :)

# Presentation at Hackito Ergo Sum

The HES’11 event was great: I had the pleasure of listening to some awesome presentations, and to meet some great people. The most interesting presentation from a non-technical point of view was the attacks at the automount feature of Linux, which everybody thinks is completely secure, but is in fact very flawed due to some buggy rendering libraries. It’s quite interesting that almost everyone thinks that their Linux installation is secure, when in fact if Linux was mainstream, viruses would be abound — but Linux is only a minor player, so malicious software is rarely written for it.

My presentation is available here. I tried mostly to demonstrate how SAT solvers work as an element of the technique that can most amply described as:

As the graphics show, the SAT solver is in fact only one player in this environment. As it turns out, it is the very last step after obtaining the cipher, creating equations describing the cipher, and converting the ANF equations into CNF. The best way to create equations from the original cipher is to use the excellent Sage Maths library for this, a tutorial of which is here. Then, the ANF created by Sage can be transcribed into CNF using, e.g. the anf2cnf tool by Martin Albrecht and me. Finally, the CNF must be solved with a SAT solver to recover the key of the cipher. This last step can be carried out by many SAT solvers, such as lingeling or MiniSat, but I prefer CryptoMiniSat, since I am the main developer for that SAT solver, and it is also very convenient to use in this domain due to some domain-specific advantages it has over other solvers. The middle two steps of the diagram are all automated by the Grain-of-Salt tool if you don’t want to use Sage, and it also contains some example ciphers, so you don’t even have to do step no. 1 in case you wish to work on one of multiple pre-defined industrial ciphers.

In case you are interested in the visualisations I used during my presentation, here is the set of tools I used. For the 3D visualisation, I used 3Dvis by Carsten Sinz — it’s a great tool to extract some structure from problems already in CNF. In case you still have the ANF, it contains more structure, though, and so it is more interesting to look at it that way. Unfortunately, that is rarely the case for typical SAT problems, and so one must often resort back to 3Dvis. For the example search tree, I used CryptoMiniSat 1.0 and gnuplot, and for the example real-time search, I used CryptoMiniSat 2.9.0, available from the same place. Unfortunately, CryptoMiniSat 2.9.0 cannot generate a search tree yet, but this eventually will be included, with time — especially if you join the effort of developing the solver. We are always looking forward to people joining in and helping out with various issues from graph generation to algorithm performance tuning, or even just some fun research.

# Come to Hackito Ergo Sum’11

There is going to be a nice hacker conference in Paris real soon now: Hackito Ergo Sum, between the 7th and the 11th of April. There will be plenty of interesting talks, among them, I will also be presenting some fun crypto-breaking :) The schedule is here, I am scheduled for the first day, on Thursday at 11:30 AM. If you are in or near Paris, come around for the conference, I am sure it will be a really nice one :) If you are interested in meeting me, we can also meet in Paris, just drop me a mail, but better yet, come and chat with me at the conf, I will be there all day long.

The HES conference mainly focuses on attacks: against software, crypto, infrastructure, hardware, and the like. If you are interested what the current trend in attacking these systems is, and/or you are interested in making your organisation safer from these attacks, it’s a good idea to come and visit to get the hang of what’s happening. It’s also a great opportunity to meet all the organisations and people who are driving the change in making software and hardware systems more secure by demonstrating their weaknesses and presenting possibilities for securing them.

Meet you at HES’11 ;)

# The Cathedral

Last week I visited Micosoft Reasearch in Cambridge, where I gave a talk on SAT solvers, Grobner basis algorithms, and Cryptography. It was nice to visit Microsoft, and in particular I enjoyed seeing how “the cathedral” works. The kind of software development carried out at Microsoft and almost all large software companies is called the cathedral model due to the book “The Mythical Man-Month“. It’s a very interesting book that talks about how software (and in particular, a “Programming Systems Product”) is developed. All Windows variants, and e.g. the IBM System/360 fall into the category of programming systems products: they are all tested, documented, extensible, have predefined inputs and outputs, come with predefined interfaces, etc. The development of these software is called the cathedral model simply because that’s the example the book uses, and it got stuck in the literature.

I have been developing CryptoMiniSat for quite some while now, and I must say it is exceedingly difficult to create a programming systems product — CryptoMiniSat doesn’t even scratch the surface of the requirements, but then almost no SAT solver does — maybe SAT4J is the sole exception. Documentation is usually scarce, and even though I have added a lot, it’s still not enough. The input is rarely checked for sanity, and resource needs are usually just ignored: if memory is not enough, then the program will probably just crash; don’t expect graceful degradation.

As for Microsoft, I must say I was pretty impressed. It’s a nice building, with large offices, free tea/coffee/orange juice, filled with some very kind and very bright people. The audience was astonishingly good too, asking questions when they felt like they haven’t understood something, instead of just getting disinterested and e.g. browsing email. All in all, it was very interesting to visit the place, though I still feel more inclined to release my code as Free Software ;)