AI is here, and AGI is coming. It's quite possible that any work being done now will be futile in comparison to reducing AI risk.
This is one of those things that's unsettling for me as someone who did a Ph. D. in a non-AI area of computer science.
But one of the main vectors by which a bootstrap AGI will gain power is by hacking into other systems. And that's something I can do something about.
Not many appreciate this, but unhackable systems are very possible. Security vulnerabilities occur when there is some broken assumption or coding mistake. They are not omnipresent: someone has to put them there. Software has in general gotten more secure over the last few decades, and technologies that provide extremely high security guarantees have. Consider the verified hypervisor coming out of Bedrock Systems; RockSalt, an unbreakable sandbox; or sel4, the verified kernel now being used in real safety-critical systems.
Suppose we "solve" security by bringing the vulnerabilities in important applications to near zero. Suppose we also "solve" the legacy problem, and are able to upgrade a super-majority of old software, included embedded devices, to be similarly secure. How much will this reduce AI risk?
To be clear: I personally am mainly interested in assuming this will be solved, and then asking the impact on AI safety. If you want talk about how hard it is, then, well, I won't be interested because I've given many lectures on closely related topics, although some others here may benefit from the discussion.
(When I call something verified or unbreakable, there are a number of technicalities about what exactly has been proven and what the assumptions are. E.g.: nothing I've mentioned provides guarantees against hardware attacks such as Row Hammer or instruction skipping. I'll be happy to explain these to anyone in great detail, but am more interested in discussion which assumes these will all be solved.)
I must disagree with the first claim. Defense-in-depth is very much a thing in cybersecurity. The whole "attack surface" idea assumes that, if you compromise any application, you can take over an entire machine or network of machines. That is still sometimes true, but continually less so. Think it's game over if you get root on a machine? Not if it's running SELinux.
I can speak only in broad strokes here, as I have not published in verification. My publications are predominantly in programming tools of some form, mostly in program transformation and synthesis.
There are two main subfields that fight over the term "verification": model checking and mechanized/interactive theorem proving. This is not counting people like Dawson Engler, who write very unsound static analysis tools but call it "verification" anyway. I give an ultra-brief overview of verification in https://www.pathsensitive.com/2021/03/why-programmers-shouldnt-learn-theory.html
I am more knowledgable about mechanized theorem proving, since my department has multiple labs who work in this area and I've taken a few of their seminars. But asking about time/space of verification really just makes sense for the automated part. I attended CAV in 2015 and went to a few model checking talks at ICSE 2016, and more recently talked to a friend on AWS's verification team about what some people there are doing with CBMC. Okay, and I guess I talked to someone who used to do model checking on train systems in France just two days ago. Outside of that exposure, I am super not-up-to-date with what's going on. But I'd still expect massive breakthroughs to make the news rounds over to my corner of academia, so I'll give my sense of the status quo.
Explicit state enumeration can crush programs with millions or billions of states, while symbolic model checking routinely handles $10^100$ states.
Those are both very small numbers. To go bigger, you need induction or abstraction, something fully automated methods are still bad at.
Yes, we can handle exponentially large things, but the exponential still wins. There's a saying of SAT solvers "either it runs instantly or it takes forever." I believe this is less true of model checking, though still true. (Also, many model checkers use SAT.)
If you want to model check something, either you check a very small program like a device driver, or you develop some kind of abstract model and check that instead.