First: I’d like to encourage other people to give this talk. Let me know how it goes, and I’ll update the slides or checklist. I’m probably not the best person to do this sort of “lay” outreach. (It was hardly “lay” in any case—I think most of the audience were CS majors.) Maybe you are?

Second: I’d appreciate your feedback. I’d like to keep the slides and checklist up to date. I unfortunately don’t have the time right now to build up more permanent advice à la Decent Security.

Third: I am fundamentally on board with Taylor Swift’s attitude to security. There is so much fear and condescension around security that many people—even CS majors!—have turned off to it. While academic security research can be really interesting, it’s at least as important to have direct, concrete advice for people without significant expertise. In many ways we’re further along than we used to be—Signal, HDD encryption, SSL/TLS—but in some ways we’re worse off (JS drive-by attacks). Whose responsibility is it to educate and protect computer users, if not us? And if not now—when?

The first abstract, Temporal NetKAT, is about adding reasoning about packet histories to a network policy language like NetKAT. The work on this is moving along quite nicely (thanks in large part to Ryan Beckett!), and I’m looking forward to the conversations it will spark.

The second abstract, Type systems for SDN controllers, is about using type systems to statically guarantee the absence of errors in controller programs. Fancy new switches have tons of features, which can be tricky to operate—can we make sure that a controller doesn’t make any mistakes when it talks to a switch? Some things are easy, like making sure that the match/action rules are sent to tables that can handle them; some things are harder, like making sure the controller doesn’t fill up a switch’s tables. I think this kind of work is a nice complement to the NetKAT “whole policy” approach, a sort of OpenFlow 1.3+ version of VeriCon with slightly different goals.

Should be fun!

One thing I omitted from the presentation—which came up more than once in conversations afterwards—is that my compiler uses LLVM as a backend. I parse a program, translate it to my own IR, optimize, and then send it off to LLVM. I’m not writing LLVM passes, or adding any kinds of AST nodes. Having my own IR probably isn’t the best architecture, but it’s much more agile than trying to modify LLVM itself. It also seems like a natural choice: my IR is tailored to reasoning about DIFC label lattices, while LLIR is particularly well suited for lower level languages, like C.