Perhaps the fact that our computer systems are now of military importance and the fact that a security hole can mean deaths and international relations disasters will finally lead to people taking a good look at verified computing. Where a virus doesn't mean outsmarting some forgetful C programmer but is mathematically impossible.
Or not, it was just a bug, we'll fix it this one time and pretend it will never happen again. Worse is better, as they say!
To answer your two questions, it is possible to mathematically prove, using certain tools that are admittedly rather academic (my argument is that we should consider using them more), that certain behaviors are impossible in a program. For example, a buffer overflow, or some form of data leak. This has been done, though admittedly not to programs anywhere near as complex as, say, the Windows kernel.
And, if there's a bug in your math, you will, of course, have some bug. Garbage in, garbage out. But! You can write your mathematical proof in such a way that the computer checks it for you (for example, static typing is a weak form of this). So all you need to have faith in is that program. Now we've exchanged faith in all programs to faith in one program. Which is an advance. But then we can formulate a proof that that program is correct in its own proof language. We hand-check this proof once, and then from then on the program can check later iterations of itself.
That's the dream, anyways. Some of the machinery to do this is available today, but some not.
Or not, it was just a bug, we'll fix it this one time and pretend it will never happen again. Worse is better, as they say!