CSF is in full swing and extremely interesting so far - and temperatures in Vienna are around 36 degrees Celsius in the sun. I guess we'll get the big storm in a day or two. Let's start with the most important point of any conference, the food. Lunch isn't included in the programme here but there's a two-hour lunch break, great for sightseeing, and there's a kilometre long avenue of market stalls selling food from around the world just behind the conference building. The snacks at the reception yesterday evening were a bit stingy - one canapé per three people, it seemed - but luck would have it that some friends of mine are in Vienna too at the moment so I spent the rest of the evening with them in a beer garden, which made the evening a sucess overall. Also I can't leave without trying a proper Wiener Schnitzel one day.
Oh yes, the conference. Saturday opened with a panel on discrepancies between theory and practice in complexity (joint between CSF and other conferences). The story goes a bit like this: industry has a problem and gives it to some theoreticians. They define a general class of problems containing the real one and study how hard it is to solve a random instance of the class; the answer is usually "very". So they go and prove that the class is PSPACE-complete (NP-completeness no longer gets you a paper these days) or even undecidable.
Meanwhile, practicioners go ahead and solve the particular problem they were given: SAT-solvers and SMT-solvers are real things, and they tend to solve things. Interestingly, if you let them loose on a "random" instance of a class of problems containing your real one and they perform badly, but one thing discussed at the panel is why such algorithms perform unexpectedly well on the particular problems that arise in reality.
One attempt to bridge this gap has been to hold regular solver competitions, the winners getting a paper in the conference organizing the competition. Here, the common complaint is that solvers nowadays seem to be optimized for scoring points in these competitions, at the expense of progress on actual industrial problems. Also some of these papers seem to offer very little insight.
As a cryptographer, I'm glad that we're not the only ones with a chasm between theory and practice. How to bridge it? I have a small idea, perhaps not so much a bridge as a foundation on which one could support a pillar on which one could build a bridge, but before I propose it let's look at another talk I particularly liked. Back in 2012, IEEE S&P infamously sent an acceptance notification to all submitted papers, followed by an apology to all the rejected ones. (I had a submission there myself and have never quite forgiven them.) This led Popescu et al. to wonder how one would build a better conference management system. So they defined some actors (author, PC member, chair) and objects (paper, review, comment, decision) and did what looks like system-theoretic analysis to me to get some dataflow requirements and security constraints (reviewers can see papers they're assigned to; authors cannot see their reviewers' identities etc.) and formally coded all this, then verified its soundness in the theorem prover Isabelle. The theory they needed to do this seems quite involved, definitely not a trivial task - the main notion used is nondeducibility [Sutherland 1986] with improvements from a string of more recent papers.
At this point they could have written a paper on "yet another proposal for a new conference management system". Instead, they used a code generator to get a verified core, wrapped a web server around it and wrote client programs. Then, they used it for a real conference (a 2014 one on the theorem prover Isabelle) and it sounds like it worked a treat. The result is called CoCon [ http://www21.in.tum.de/~popescua/rs3/GNE.html ] and on the last slide of the talk we were all invited to try it out if we have an upcoming conference to organise.
Generating code from a fromally verified core is certainly a promising strategy - if we can do CoCon today, perhaps a SSL implementation tomorrow? What I liked most about the authors' work though is that they did not stop at "we've got the theory worked out, it looks practical to us, let's write a paper", they actually built the thing and used it for real.
Which brings me to my proposal. It's not actually that new an idea but based on the concept of technology readiness levels, as used in aerospace engineering for example. This is a set of well-understood levels describing how mature a technology is, from "drawing board" through "has been built and stress-tested in isolation" through to "used in production applications for X years and data on long-term perfomance in real environments is available".
What I propose is that we introduce a similar classification for papers presenting new cryptographic technologies, which would greatly help us to share research outcomes with practitioners. The number and descriptions of categories are of course open to debate but here's a proposal off the top of my head. The classification only applies to papers proposing new constructions or schemes (or improving on existing ones); there are other classes besides the ones below such as work that synthesizes existing knowledge, automates modes of reasoning or breaks an existing scheme. I propose that authors of papers presenting new constructions should be obliged to say which class they believe their constructions to lie in; whether this claim is justified will be one of the criteria by which papers are judged.
R : realised
This construction has been implemented and successfully used in practice to solve a real-world problem. Concrete examples of the type and size of problem solved are given. The value of such a paper is not in the theoretical insight that it provides (though such insights are by no means forbidden in a type-R paper) but in demonstrating the practicality of the construction and presenting insights gained during implementation and use. Concrete parameters such as the size of the problem solved, key sizes and timings are provided.
Examples of a class-R papers could be the CoCon one presented here at CSF or De Marneffe et al.'s work on using Helios at Louvain-la-Neuve.
I : implemented
The authors have implemented their construction, run it and provided timings, space requirements etc. for realistic problem domain and key sizes. The authors consider the implementation ready to be applied to real-world problems but it need not have been used "for real" yet. A central question in judging a type-I paper shall be whether the implementation stands up to the claim of practicality.
The 2008 paper by Adida et al. that introduced Helios to the world could be an example of a type-I paper.
P : proposed
The construction is worked out to the point that the paper could be used as a basis for implementation by engineers, without requiring any more theoretical advances to build the scheme. The authors further believe that an implementation of the proposed scheme is practical (for parameters specified in the paper) and the paper shall be judged among other things on these claims.
An implementation and timings are not required for type-P papers.
An example of a type-P paper could be the Oakland 2008 one on Civitas. While Civitas is definitely type-R today, the 2008 presentation contains the lines "This work is about advancing the science, not selling a particular system ... not suitable for running a national election (yet):"
A : advance in the theory
A paper in this class presents an advance that has no immediate claims to practicality yet but may be a step towards a practical solution. It could realise an existing notion under weaker assumptions or lower resource bounds.
The first advances in fully homomorphic encryption after Gentry's founding paper come to mind as examples of type A: orders of magnitude faster than the original yet still orders of magnitude away from being worth implementing (for our current understanding of suitable lattice key sizes). I would personally put many early voting protocols in this class as they make unrealistic assumptions on voters' abilities.
T : theoretical
A construction in this class asks to be judged on its theoretical contribution alone. It could solve an open problem or show that a particular class of scheme is realisable in principle; it could also be valued for the theoretical insight and understanding gained. The theoretical contribution is sufficient that short- or medium-term practical applications are not relevant.
Example constructions in this class include Gentry's original paper on fully homomorphic encryption or the result that zero-knowledge proofs (without random oracles) exist for all statements in class NP.
Note that the classification is nominal in the sense that a paper describing a type-R scheme is not a priori better or worse than one describing a type-T one; rather the classes express that there are different valuable goals in the design and construction of cryptographic schemes. Reviewers get the extra power not just to judge how interesting a problem is per se but how interesting it is to solve a particular problem in a particular class - results in different classes are not directly comparable in our opinion. Conferences may restrict which classes of problems are within their scope of course. One could also produce statistics on submitted and accepted papers in each class and conference organisers could incentivise submissions in particular classes in their calls for papers if they judge this to be in the interest of the cryptographic community.
The biggest advantage that I claim for this classification (though the actual categories would need to be discussed and refined) is that we gain an extra level of discourse to present our work to the wider world and give more practically oriented computer scientists a better way to understand the state of the art of cryptography.
Post a Comment