alt Hacker NewsI'm not an expert on Rice's theorem but I believe it implies that 100% secure software is not possible.
And finding exploits manually is so incredibly time consuming, and the number of people who are good at it are so few. I don't think the result of thousands of existing exploits is suprising.
I think we will start to see more and more remote hardware exploits as AI improves. Especially with IoT devices. The limiting factor being AI's ability to interact with the real world,
> I'm not an expert on Rice's theorem but I believe it implies that 100% secure software is not possible.
It does not. All it proves is that you cannot have an automated check that for any given program decides "is this secure or not?" (according to some security criterion).
Rice's Theorem is often misunderstood as "we can't prove nontrivial properties about programs". But we really can, about a lot of programs. All the theorem really says is that there exist certain programs for which those properties are undecidable. The obvious answer is to just not write those programs then.
Practically speaking though, this often means that if you want to formally prove certain properties about your program, you can't just write the program in whatever way you want to and then hope to toss a verifier at it. You have to architect it in a way that makes it amenable to the proof techniques we have available. That could mean co-designing a C codebase and a set of mechanized proofs (this is how seL4 is built) or it could mean writing in a language that makes certain things easy to prove to begin with. There are even languages that are deliberately not Turing complete, so they avoid Rice's theorem entirely, while being useful for writing practical programs in. An example would be Idris, which famously is "Pacman complete" (i.e. you can write video games in it).