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.
Did you mean the Linux talk was a non-technical talk? I thought it was pretty technical. I actually thought it was a bit dull until he started showing us some results (like the non-uniform distribution of libc load addresses) and pulling out the DVI font parser code. At that point it was very interesting for me. Although I tend to think browser/email/attachment/document attacks are slightly more interesting, simply because they are more powerful.
Is there a video of your talk? :-)
I didn’t think it was non-technical — it had some very real tech inside, as you noted. What was interesting for me from a non-tech point of view is that everyone is seriously convinced that Linux is safe from this kind of USB viruses, when in fact it is not. As for the presentation being partially boring — I actually enjoyed its first half exactly because it was rather non-technical and somewhat philosophical about Linux security. I myself am deluded sometimes about the security of Linux from the point of view of USB devices. I regularly plug anything into my computer, without even thinking about it — so much so that when I booted my new Windows installation up, I just plugged in a USB without thinking (it was a clean install, so no antivir, autorun enabled, etc.), a gave mistake, of course. The worst is not when you are insecure, it’s when you are insecure, and you are convinced you are invincible.