Funding Formal Methods for the Cyberpocalypse

Introduction AI capabilities are rapidly increasing, including in offensive cyber, with open-weight models quickly following their closed-weight frontier cousins by whatever means necessary.  It seems likely these trends will continue to a point where the average teenager with a few hundred dollars can pull off heists on the scale and sophistication of a nation-state in 2018, or better.[1]  And humans aren’t the only potential problem: agents can also autonomously hack and self-replicate. Some (e.g. Matthew Green) believe that defensive AI uplift will massively outpace offensive uplift, which seems possible eventually, but clearly wrong at least for a while. To put a pin on it: offense is logically and structurally easier than defense.[2]  Many industries are inherently slow to defend, for example, due to FDA regulation on software updates for medical devices, fear of litigation, requirements for backward compatibility or interop with devices controlled by other vendors who are not incentivized to collaborate (a common problem with military hardware), or uptime requirements which, in the short term, make patching less tolerable than being continuously exploited.[3]  Consequently, there may soon be a cyberpocalypse, in which the cybersecurity (and, thus, stability) of table-stakes internet-connected infrastructure will plummet to zero, driven by rampant AI-enabled cybercrime. Recently, several philanthropic organizations have asked me[4] how I think they should go about funding formal methods to pre-empt the cyberpocalypse.  The framing is basically that we can reduce or maybe even pre-empt this cyberpocalypse using AI-enabled formal methods at scale, i.e., by mathematically hardening existing software against future attacks.  But, doing so would be very expensive, and requires moving very quickly.  How should a well-funded philanthropic organization go about doing this? In this document I outline a loose vision for how to fund formal methods quickly, for broad, global cyberassurance.  I envision this document as candidate guidance for large organizations which plan to spend money broadly on AI safety causes, and want to allocate a fraction of their portfolio to approaches rooted in formal methods.  Note that I do not claim formal methods solves AI safety generally, rather, I claim that it ameliorates some of the short-term problem of offensive cyber uplift. My high-level conclusion is twofold.  First, current FM tools are built for a very different world than the one we will live in in a year or two.  We can build more impactful tools if we build for the future.  Second, these tools need to be applied where it actually matters: hardening the cyber infrastructure that real people actually depend on, for banking, energy, private messaging, commerce, and so forth. This is a global problem and it requires global talent. What not to do It is tempting to say, well, finding and funding real human people is hard, so how about instead, we just give the money to half a dozen SF vampires and ask them to burn tokens generating wholesale Lean-verified replacements for popular open-source software, or something like that.  This approach is foolish.  Existing software builds on decades of latent folklore knowledge: implicit specification in the form of email chains, github issues, tweets and so forth, all of which is missing context for any autoformalization agent.  The agent won’t even know the software was meant to do that in the first place.  The operator who uses the software might not even know what the software is meant to do, and certainly doesn’t know every aspect of what it currently actually does.  This problem, spec elicitation and validation, is what Mike Dodds is working on, and it is an enormous one.[5] It is also tempting to say, well, sure it would be nice to hire talented researchers from around the world, but we don’t really have time for meritocracy because the world is going to end tomorrow.  So let’s just get a bunch of Oxford and MIT kids and pay them to do FM work.  This is also foolish.  There are banks and hospitals and telecom and utility companies in Morocco and India and Mexico just like there are in the United States.  All these countries will be impacted by the cyberpocalypse, and they should all share in the remediation.  The only way to achieve global cyber-hardening is therefore to rapidly train the next generation of computer scientists, worldwide, to help harden everything, everywhere, all at once. People and organizations I believe that philanthropic organizations should spend money in a way that maximizes the number of FM experts available, worldwide, to harden cyber systems; the number of critical systems that can be secured per FM expert; how easy it is for a forward deployed FM expert to harden an arbitrary software system; the cybersecurity of commonly used, foundational open-source software; and the cybersecurity of commonly used closed-source products that lack proper incentive