Notes on HACS 2017

January 17, 2017

Real World Crypto is probably one of my favorite conferences. It’s a fine mix of practical and theoretical talks, plus a bunch of great hallway, lunch, and dinner conversations. It was broadcasted live for the first time this year, and the talks are available online. But I’m not going to talk more about RWC, others have covered it perfectly.

The HACS workshop

What I want to tell you about is a lesser-known event that took place right after RWC, called HACS - the High Assurance Crypto Software workshop. An intense, highly interactive two-day workshop in its second year, organized by Ben Laurie, Gilles Barthe, Peter Schwabe, Meredith Whittaker, and Trevor Perrin.

Its stated goal is to bring together crypto-implementers and verification people from open source, industry, and academia; introduce them and their projects to each other, and develop practical collaborations that improve verification of crypto code.

The projects & people

The formal verification community was represented by projects such as miTLS, HACL*, Project Everest, Z3, VeriFast, tis-interpreter, ct-verif, Cryptol/SAW, Entroposcope, and other formal verification and synthesis projects based on Coq or F*.

Crypto libraries were represented by one or multiple maintainers of OpenSSL, BoringSSL, Bouncy Castle, NSS, BearSSL, *ring*, and s2n. Other invited projects included LLVM, Tor, libFuzzer, BitCoin, and Signal. (I’m probably missing a few, sorry.)

Additionally, there were some attendants not directly involved with any of the above projects but who are experts in formal verification or synthesis, constant-time implementation of crypto algorithms, fast arithmetic in assembler, elliptic curves, etc.

All in all, somewhere between 70 and 80 people.

HACS - Day 1

After short one-sentence introductions on early Saturday morning we immediately started with simultaneous round-table discussions, focused on topics such as “The state of crypto libraries”, “Challenges in implementing crypto libraries”, “Efficient fuzzing”, “TLS implementation woes”, “The LLVM ecosystem”, “Fast and constant-time low-level algorithm implementations”, “Formal verification/synthesis with Coq”, and others.

These discussions were hosted by a rotating set of people, not always leading by pure expertise, sometimes also moderating, asking questions, and making sure we stay on track. We did this until lunch, and continued to talk over food with the people we just met. For the rest of the day, discussions became longer and more focused.

By this point people slowly started to sense what it is they want to focus on this weekend. They got to meet most of the other attendants, found out about their skills, projects, and ideas; thought about possibilities for collaboration on projects for this weekend or the months to come.

In the evening we split into groups and went for dinner. Most people’s brains were probably somewhat fried (as was mine) after hours of talking and discussing. Everyone was so engaged that you not once found the time to take out your laptop or phone, or had the desire to do so, which was great.

HACS - Day 2

The second day, early Sunday morning, continued much like the previous. We started off with a brainstorming session for what we think the group should be working on. The rest of the day was filled with long and focused discussion that were mostly a continuation from the day before.

A highlight of the day was the skill sharing session, where participants could propose a specific skill to share with others. If you didn’t find something to share you could be one of the 50% of the group that gets to learn from others.

My lucky pick was Chris Hawblitzel from Microsoft Research, who did his best to explain to me (in about 45 minutes) how Z3 works, what its limitations are, and what higher-level languages exist that make it a little more usable. Thank you, Chris!

We ended the day with signing up for one or multiple projects for the last day.

HACS - Day 3

The third day of the workshop was optional, a hacking day with maybe roughly 50% attendance. Some folks took the chance to arrive a little later after two days of intense discussions and socializing. By now you knew most people’s names, and you better did because no one cared to wear name tags anymore.

It was the time to get together with the people from the projects you signed up for and get your laptop out (if needed). I can’t possibly remember all the things people worked on but here are a few examples:

• Verify DRBG implementations, various other crypto algorithms, and/or integrate synthesized implementations for different crypto libraries.
• Brainstorm and experiment with a generic comparative fuzzing API for libFuzzer.
• Come up with an ASCII representation for TLS records, similar to DER ASCII, that could be used to write TLS implementation tests or feed fuzzers.
• Start fuzzing projects like BearSSL and Tor. I do remember that at least BearSSL quickly found a tiny (~900 byte) buffer overflow :)

See you again next year?

I want to thank all the organizers (and sponsors) for spending their time (or money) planning and hosting such a great event. It always pays off to bring communities closer together and foster collaboration between projects and individuals.

I got to meet dozens of highly intelligent and motivated people, and left with a much bigger sense of community. I’m grateful to all the attendants that participated in discussions and projects, shared their skills, asked hard questions, and were always open to suggestions from others.

I hope to be invited again to future workshops and check in on the progress we’ve made at improving the verification and quality assurance of crypto code across the ecosystem.