High-Assurance Crypto Software

HACS 2020

HACS 2020 will be a two-day event in January in New York (5th & 6th January) followed by an optional hack day (January 7), all taking place directly before the IACR Real World Crypto Symposium, which is scheduled for 8th-10th January also in New York. The "hack days" in past years were something many attendees wanted to repeat in future events.

As in 2017, HACS will be held in the Vanderbilt Hall of the NYU School of Law at 40 Washington Square S, New York. For the hack day we'll be at Google, 85 10th Avenue, New York.

We will build on the success of the past 3 HACS events by keeping a similar size (somewhere between 60-90 people), similar facilitation process, and similar attendees. Our hope for the 2020 meeting is continue to advance the core focus areas while also expanding to consider a broader range of topics including:

  • Testing, formal verification, and generation of crypto code. This has been a core topic area in all three prior HACS events, and work at HACS 2020 will focus on assessing progress made and work remaining to be done.
  • Formal verification and generation of security proofs for cryptographic protocols, with the goal of having machine-checked proofs instead of error-prone pencil-and-paper ones.
  • Zero-knowledge topics, including Schnorr, SNARKs/STARKs, bulletproofs, and pairing-friendly curves, with particular focus on languages, tools and formal methods applied to these topics.
  • Advanced implementation attacks, addressing specific microarchitecture attacks including Spectre and variants, fault attacks, and power attacks, as well as formal modeling of these attacks and associated countermeasures.

Considering that previous workshops served to make introductions and start a number of projects, we will continue adjusting the process to drive collaboration toward concrete outcomes. We expect a significant number of attendees have ongoing projects and concrete goals in mind. The organizers will spend significant time before the event discussing what these are and arranging workshop sessions to advance concrete objectives.

HACS events to date have already produced significant outcomes in driving the convergence of cryptographic software and formal and high assurance verification. We are excited about the potential for the 2020 event to continue this trajectory while also moving in new and compelling directions.


Apple AWS Google Microsoft
Electric Coin Co.