Category Archives: Personal

CCC Camp’11

Personal, Research, , , ,

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

Winning the SAT Race

Personal, SAT

The software I developed, CryptoMiniSat 2.5 won the SAT Race of 2010. It is a great honour to win such a difficult race, as there were 19 other solvers submitted from 9 different countries.

Thinking back and trying to answer the question why CryptoMiniSat won, I think there are no clear answers. Naturally, I put immense effort into it, but that is only one part of the picture. Other important factors include those who supported me: my fiancée, the PLANETE project of INRIA, and in particular Claude Castelluccia and my colleagues here in Paris, the LIP6 team and my professor here, Jean-Charles Faugere. As with all randomised algorithms, luck played a good part of winning, too.

In all of this, it is interesting to note that I never had a colleague who worked in or even near the field of SAT: both the PLANETE and the LIP6 team use SAT solvers only as a means to an end, not as an end in itself. In other words, I had to get this far mostly alone. To be honest, I think this is one of the reasons I had won, too: there probably is too much misunderstanding in SAT that everybody takes for granted. Since I never really talked with anyone about their understanding of the subject (I only read papers, which state facts), I had a white paper in front of me, which I could fill with my own intuitions, without being lead by those of others. Naturally, this means that I have probably stepped into a large number things that are widely understood to be wrong, but at the end, it seems that I must have also made some good steps, too.

As for the bad steps I have made (and of which I am aware of), I had copied the subsumption algorithm from SatElite, which the authors of MiniSat told me was a bad move, since its self-subsuming resolution is slow. I had in fact observed this, but I thought it was a fact of life. Alas, it isn’t. Other errors I have made include a non-portable pointer-shortening which shortens pointers to 32 bits when using 64-bit architectures (Armin Biere’s lingeling does this right), and a wrong clause-prefetching code that Norbert Manthey put me right about. I have also conceptually misunderstood the possible impact of variable elimination on the difficulty of resolving an instance, a grave mistake that Niklas Sörensson put me right about.

As for the good steps, I think I have made a couple of them. Firstly, I have put the 2009 SAT paper we wrote with my colleagues to its natural conclusion: including XOR clauses and partial XOR reasoning into the innermost parts of the solver. Secondly, I have used the community to its fullest potential: CryptoMiniSat was used by the constraint solver STP far before the SAT Race began, and it was distributed to a number of highly skilled individuals who made use of it and gave feedback. Sometimes I got very negative feedbacks (these were the most valuable), which highlighted where and why the solver was failing. Thirdly, I have tried to take advantage of the academic environment I work in: I have tried to read the relevant papers, used the clusters provided by the French universities to carry out experiments, and generally took my time (rarely an option in industry) to get things right instead of rushing out a solver.

The 2010 SAT Conference

Personal, SAT,

I am currently at the SAT 2010 conference, in Edinburgh. It is my second SAT conference, but the first one where I finally have a chance to know who is who. I had a chance to talk to some great researchers. For instance, I talked to (in no particular order) Armin Biere (author of PrecoSat and Lingeling), Niklas Een, Niklas Sörensson (authors of MiniSat — new version is out, btw), Marijn Heule (author of the march_* set of solvers), Matti Järvisalo (one of the authors of Blocked Clause Elimination), the author of MiraXT, and many others. It’s really a great place to meet up people and get a grasp on what SAT is really about. It’s also a great way to understand the motivation behind certain ideas, and to hear the problems encountered by others.

For instance, I now know that bugs, about which I have already written a blog post about is a problem that comes up for nearly everyone, and tackling them is one of the most difficult things for the developers. I have also finally understood the reason behind the MiniSat Template Library (MTL), which I’ve always found odd: it re-implements many things in the STL (the Standard Template Library), which I have always found unnecessary. Although the reasons are now clear (better control, easier debugging, less memory overhead), I think I will still replace it with STL. I have also had a chance to talk to the kind reviewer who did such an extensive review of my paper, which was quite an enlightening discussion. If you are interested in SAT, I encourage you to attend next year: there are usually some workshops associated with the conference, where it is easier to have a paper accepted: e.g. this year, a Masters student got his quite interesting paper (long version) accepted, and I am sure he has benefited a lot from it.

Tools that I often use

Personal,

I used to use Perl a lot in the old days. Martin Albrecht, through the sage mathematics software, showed me Python. I first really hated Python. But then, I realised I can simply type away in it, as in C++, but without all the hassle of C++. I saw a little of AWK once, and I got madly in love with it — when it comes to simple scripts like counting numbers printed by programs, AWK is unbeatable. I use grep a lot, and recently I realised how great a combination grep and wc (a very dumb utility that counts lines/words) are. For instance, I can simply do: “grep “s SAT” *.output | wc -l” to find how many problems have been solved by CryptoMiniSat. I am also finding myself using grep and AWK together to create shell scripts that I run later. For example, I can do: “ls *.cnf | awk ‘{print “./cryptominisat ” $1 ” > ” $1.output” }’ > script.sh” which, when executed, solves all CNF files in the directory, and generates a *.cnf.output file for each, containing the output of CryptoMiniSat. An interesting utility in UNIX is ulimit, with which can limit the memory and time (and stack, etc.) usage of a process. Putting a “ulimit -t 10000” at the beginning of our “script.sh” we can simply limit CryptoMiniSat to 10000 seconds for each instance.

As for failures in terms of the tools I use, I can probably list a few. I tried very hard to learn Haskell, a purely functional language, but I simply couldn’t fully wrap my head around it. Haskell bothered me, because it seems so intuitive, yet it is so hard to master. I haven’t yet got around learning sage, either, even though I think Martin Albrecht is doing a great service to the community by coordinating it. I hope one day CryptoMiniSat will be used inside it, though :)

My connection with the boost library is a love-hate relationship. I think boost is just amazing: it lets me program with the least amount of effort, creating a program that is less error-prone, more robust and multi-platform. However, at the same time, many programmers avoid it like the plague, for multiple reasons. Firstly, the library changes so often that something you wrote just two months ago might not compile with the new boost. Secondly, it’s a nuisance to have dependencies in the code. Thirdly, compilation times can increase significantly e.g. with the Spirit parser. I don’t agree with the second argument, since boost as a dependency isn’t significant and it saves on a lot of debugging time, and the third argument is becoming moot due to gcc 4.5. But the first argument has, actually, hit me too, and it is very unpleasant.

A great essay on security in the cyberworld

Personal,

I just read this paper on cybersecurity by Daniel E. Geer, and I was very impressed. Unfortunately I haven’t heard from the author yet, but I regularly used to read the blog of Bruce Schneier, and this essay basically puts the same ideas into perspective.

I have found the essay to be very interesting, and very thought-provoking. It shows very well that security in the cyber (or cyber-connected) world is very difficult to attain. There are no simple solutions. I personally think that security in the real world (not only the cyber world) is also very difficult to obtain, and unfortunately politicians tend to go the easy way, and simply bend in front of the will of the people by implementing “security measures” that in the end don’t help much (if at all) in terms of security, but reassure the people. An example of this is the ban of liquids on airplanes, while cockpits in Europe are still not reinforced — the former doesn’t achieve much but is very visible (and so is more of a security theater), while the latter would be much less visible, but also much more effective. Also to note, that the former takes a lot of man-power to implement, and inconveniences the users (thus taking their time, too), while the latter would be relatively cheap.

The mentality that leads us to believe that bombing is more of a threat is that most people expect planes to be blown up, while hijacking is most only an afterthought. This serious mistake is probably a psychological effect, as most people tend to remember visually colourful incidents more, and Hollywood has made use of the “blow-up” effect too much, etching it into the brains of most people, even decision-makers. However, it is important to remember, that most serious problems in airports and airplanes were carried out through the use of arms other than bombs: to take a trivial example, no planes used in 9/11 were bombed. As a side-note, reinforced cockpits would have prevented all of 9/11, and European cockpits are still not reinforced, but my toothpaste is always taken away — a serious defect, I say.