What analysis was Bruce Schneier referencing when he wrote:
Viruses have no “cure.” It’s been mathematically proven that it is always possible to write a virus that any existing antivirus program can’t stop.
From the book Secrets & Lies by Bruce Schneier, page 154.
Under one possible interpretation of that, it's a result of Rice's theorem. A program is malicious if it performs some malicious action, which makes it a semantic property. Some programs are malicious and some aren't, which makes it a non-trivial property. Thus, by Rice's theorem, it's undecidable in the general case whether a program is malicious.
Actually, the opposite can be easily proved: since all computer viruses are executable code in one way or another, all you have to do is write an antivirus program that will report ANY executable code as viral. It logically follows that such a program will detect ALL possible viruses:
Sure, an argument could be made about this antivirus software barfing out too many "false positives". But what are the criteria to decide whether a positive is false or true? Ah! Turns out the distinction between benign code and malicious code, between an honest "remote PC control" suite and a trojan like Netbus is completely arbitrary, and so the whole question is pointless.
According to Wikipedia:
In 1987, Fred Cohen published a demonstration that there is no algorithm that can perfectly detect all possible viruses.
It also references this paper. That might be the analysis Mr. Schneier was referring to.
The statement can't be mathematically proved unless it is reformulated as a mathematical proposition.
At the very least, that requires a mathematically sound definition of what a "virus" is: which is challenging; and you might end up with an abstraction that isn't useful in practice, because it includes some behaviours which people regard as entirely benign and useful, and/or excludes some behaviours which people consider antisocial.
The tough thing here is that a virus is a program that changes its environment in some way, and any attempt to define the environment rigorously is going to be too limiting for practical use.
So I would say no: the proposition can't be mathematically proven, and that's because it can't be mathematically formulated.
tl;dr- The answer depends on exactly what requirements you impose on the question.
If you merely want to detect all viruses without further constraint, then simply flag anything and everything as a virus, and you're done.
If you want to properly identify all programs as either a virus or not, then it's impossible in the unbound case since the classification problem reduces to the halting problem.
If you want to properly identify all programs as either a virus or not, and you're considering a finite machine, then it's theoretically possible but not generally feasible in practice.
If you allow that the computer can produce random errors, then any program can be a virus.
Obviously, flagging all programs as viruses catches 'em all. (Pok'e'mon!)
Starting with this case to make the point that it's not hard to detect all viruses; rather, the specific theoretical problem is correctly classifying iff programs are viruses.
Consider the program:
doHaltingProblem(); // Not a virus operation itself
installEveryVirusEver(); // Definitely a virus operation, but will it happen?
In this case, the program is a virus only if the halting problem halts, allowing installEveryVirusEver() to occur. So, virus-detection reduces to the halting problem in the general, unbound case.
If programs to be classified as viruses-or-not are to operate on a finite machine, then you can simply simulate the machine running from every possible starting state. Finite machines will eventually loop back to a prior state, so it's necessarily a finite (if lengthy) analysis.
Assuming that a machine can run a program that'd be considered a virus, and there's a non-zero chance of a random mutation shifting it into that state, then it should eventually arrive at a virus state.
Which is kind of a boring point, but just for completeness's sake.
Viruses have no “cure.” It’s been mathematically proven that it is always possible to write a virus that any existing antivirus program can’t stop.
–"Secrets & Lies", Bruce Schneier, page 154
As pointed out in Case (1) above, it's possible to flag all viruses by just flagging everything as a virus; that's easy. What's impossible is to, in an unbound case, determine if every possible program is a virus or not.
Further, it's difficult to establish if particular programs are viruses in bound cases. For example, consider the program:
var toExecute = decryptByBruteForce([ciphertext]); // Decrypt the next part of the program by brute-force
run(toExecute); // Run the now-decrypted part of the program
As discussed in Case (3), this program can be classified as a virus-or-not when run on a finite machine, but since doing so would require brute-forcing an encrypted message, it's not likely feasible in practical scenarios.
So, in real-world applications, it reduces to an issue of heuristics: anti-virus programs make guesses at what's a virus or not. Or if you want more reliable security, you could have an anti-virus program flag anything that it can't prove to be safe, dodging the issue of needing to classify every possible program.
Unfortunately, the use of heuristics gives knowledgable attackers security holes to target. Without reading the source of the quote, I suspect that this problem is what they were trying to refer to.
It depends on your definition of "stop".
If you define stop as being "detect, ahead of time, that code could do something malicious, and prevent it running", then as others have mentioned, this is impossible, by Rice's theorem.
If you define stop as "detect when a running program is attempting to do something bad, and then stop it", then Rice's theorem doesn't apply. Your antivirus doesn't need to decide if the program could do something malicious, only whether it's doing something malicious now.
AFAIK, the second version hasn't been proven impossible mathematically impossible. And indeed, for any sufficiently specific definition of "malicious", it's very doable - this is essentially sandboxing.
It seems likely, however, that there is no good definition of "malicious", than would cover all the forms of malice that a virus might attempt. What about a virus that mines bitcoin? Or that serves up pirate movies? Or that spams message boards on your behalf? All of these are indistinguishable from code being run by users who genuinely want to do exactly these things. As such, I suspect (although I don't know of any attempt to prove) that creating antivirus is AI complete.
Yes, it was mathematically proven by Alonzo Church in 1935–36 and independently shortly thereafter by Alan Turing in 1936.
No, you can not, because the difference between malware and a useful program is completely subjective. Any "evil" behavior can be intended behavior. For example, I have the following programs running on my computer right now:
You can't tell the difference, because from a purely technical perspective they do the exact same things. The only difference is in the intention. One program deceives the user about what it does and acts against the users interests, the other does exactly what the user wants it to do. But what the user really wants from their software is something a machine can not decide... at least not at the current stage of AI technology. That's why all virus scanners are primarily signature-based.
To mathematicly prove that it is always possible to write a virus that can bypass all existing anti-virus programs, you would first have to mathematicly define what is a virus, and good luck with that.
Perhaps a "program that performs undesired actions"? Well that is simply impossible, imagine a program that opens a connection to your PC and enables remote control. The antivirus can see that the program does this, but how can it know if it is desired or not?
It might be a legit remote control program like TeamViewer, or it might be a virus mascarading as a simple image viewing program, eigter way, your antivirus will see a program that can read and view images from your PC and open remote connections, and it will have no way to tell if that a "desired" behavoiur or not, since it can't know why you are installing that program.
As pointed out by @walen, it is actually possible to detect all viruses if false-positives are allowed: just report everything as a virus.
Let's assume that it is also possible to detect all viruses if false-positives are not allowed. We'll have a IsVirus function which can be run on any program and return whether or not that program is a virus. Now, consider this program which we'll call P:
if IsVirus(P):
exit
else:
DoVirusThings
What is the value of IsVirus(P)? If it's true, then P just exits without doing anything and we therefore have a false-positive. But if it's false, then P does virus things and we have an undetected virus.
This proves that it is not possible to detect all viruses if false-positives are not allowed.
The original question was "Has it been mathematically proven that antivirus can't detect all viruses?"
It's likely accurate to say that we can never prove that we have written code that will detect all viruses.
A general-purpose computer attached to the Internet with the ability to download and execute code is likely equivalent to a universal Turing machine. This equivalency includes Turing's infinite tape size: If the bandwidth of the machine's network interface is less than the total growth rate of Internet-accessible data, the machine can never reach the "end of the tape". (I covered this a little in the conclusion of this paper a long time ago. While it's demonstrable in a practical sense, coming up with a mathematical proof would probably require adding some constraints.)
If the above is true, and if "to halt" means "to produce a report listing all viruses on the system, no more or less", then we can't prove in advance that the program will halt with a correct answer; we have to run it in order to find out.
If both of the above paragraphs are true, then we can never verify correctness of the resulting report, because we can never compile a complete list of all possible viruses to compare it with: Those viruses are all out there somewhere on the tape, it's infinite in size, and we can never read the whole thing.
If all three paragraphs are true, then we can never prove that we have written a 100% correct virus detector.
Well, the definition of a virus is pretty vague. Yes, it is a malicious entity, but malicious is just as vague. Depending on the system and it's policies the the possibilities for a malicious entity will change. Defining a ever changing entity is something thats has come up in various fields, number theory, state machines, etc. and it has been proven in different ways that it is not possible, at least based on what we know.
One way would be, instead of defining what is malicious we can define what is allowed, a very strict and independent system, which allows only certain sequences of operations to be performed. That way it MAY be kept safe.
This problem IMO is just as hard as defining random.
A Virus is just code--it's kind if saying "Can my AI lawn mower program tell the difference between weeds and plants"--if so, does it pull daises?
If you download a program that sends emails to everyone in your contact list, is it a virus or are you a spammer? Depends on why you downloaded the program, not any specific of bytes in the program.
So you don't even have to go to mathematical proof--you can just reason that it can't be done.
On the other hand, you could say it's easy to identify viruses if you define virus by behavior. Programs are updated as part of an update process, if anything attempts to change code on your computer outside this process you could define it as a virus. With this definitions you could easily detect changes that happen outside of specific installation procedures. It might take hardware that can separate code from data and lock down the code space when you aren't holding in a button, but it's possible (if annoying).
This also assumes that the code you deliberately installed during the update process is not a virus itself, but since we are defining a virus by behavior for this example then by definition I guess it's not.
Has it been mathematically proven that antivirus can't detect all viruses?
What analysis was Bruce Schneier referencing when he wrote:
Viruses have no “cure.” It’s been mathematically proven that it is always possible to write a virus that any existing antivirus program can’t stop." [0]
[0] Secrets & Lies. Bruce Schneier. Page 154
This answer does not directly address what analysis Bruce Schneier was referencing. An individual who is interested in what a primary source meant when they made a statement should make the effort to contact the primary source themselves to ask their specific questions, to avoid speculation, conjecture or confusion.
Kurt Gödel's Incompleteness Theorem published in 1931 in Über formal unentscheidbare Sätze der "Principia Mathematica" und verwandter Systeme (called in English "On Formally Undecidable Propositions of "Principia Mathematica" and Related Systems") when carefully considered is very instructive relevant to analysis of any formal system, from computer viruses to politics
1. If a (logical or axiomatic formal) system is consistent, it cannot be complete.
2. The consistency of axioms cannot be proved within their own system.These theorems ended a half-century of attempts, beginning with the work of Frege and culminating in Principia Mathematica and Hilbert's formalism, to find a set of axioms sufficient for all mathematics.
In hindsight, the basic idea at the heart of the incompleteness theorem is rather simple. Gödel essentially constructed a formula that claims that it is unprovable in a given formal system. If it were provable, it would be false. Thus there will always be at least one true but unprovable statement. That is, for any computably enumerable set of axioms for arithmetic (that is, a set that can in principle be printed out by an idealized computer with unlimited resources), there is a formula that is true of arithmetic, but which is not provable in that system. To make this precise, however, Gödel needed to produce a method to encode (as natural numbers) statements, proofs, and the concept of provability; he did this using a process known as Gödel numbering.
Not a mathematical proof, but AFAIK there are two ways to detect malware:
Signatures
As new malware can be developed - Including obfuscating or modifying existing ones - the signature of the new malware won't be in the antivirus database, therefore it won't be detected
Heuristics
This method uses automatic dynamic and/or static analysis to understand the behavior of the software and according to what it does the antivirus decides if it's malicious or not.
And here comes the tricky part, not everything that today is considered innocuous may be in the future.
For example, 20 years ago a piece of software using encryption libraries may have not been seen as something malicious, now we know that it may be some kind of ransomware encrypting your data. At the same time, you may (And you should) use a password manager that also uses encryption libraries to securely store your data. So how can we decide if it's malware or not only based on the fact that it encrypts data? Similarly a TCP connection may be used to leak information or to browse websites
The only difference is semantic, which is hard to analyze in an automatic way because technologies constantly evolving and malware adapts to that evolution. After all malware is no different from any other software except for its owner bad intentions
No, it has not been proven, and cannot be proven because it's not true. An antivirus program that actually works is simply a suitable permissions/access control model enforced by the runtime environment. Rice's theorem is irrelevant because you don't have to determine ahead of time if a program is safe. You just run it under the access controls, and abort it (or just deny access) if it attempts to do something contrary to your policy.
Mathematically, this means you have a computable test that gives you a positive result if a progam is malicious, but may not halt if the program is not malicious. That's fine, because the test is running the program, and you can just keep running at as long as it's not malicious.
Of course real-world antivirus programs don't do the simple obviously right thing (which would be integrated with the OS, runtime VM, or similar component, not a separate AV product). Instead they use bogus signatures and heuristics to classify programs. It is provable (see other answers) that such an approach cannot work.
No math needed. Experiment time. Lets arrange a pool of viruses, a pool of systems-that-try-to-defend-themselves and mechanisms that constantly change/improve both parties.
Give them a planet. Wait billions of years.
Do we still have viruses?
For me the sheer number of possibilities already tested is far beyond satisfactory.
Here I'd like to explain why I've drastically reframed your question.
The direct answer to your question "Has it been mathematically proven that <statement about real world>" is: No, mathematicians have never proven your statement about real world (or any other such statement). By real world I mean the one that you see when you look out your window.
You can only prove anything in axiomatic systems ("worlds" that are ruled by a set of axioms - where axioms themselves are defined as unprovable). I don't know axioms that rule the real computer viruses, so I cannot prove anything about these.
I'll try to predict reality and I'll be often correct, sure. But I will use falsifiable theories for that, not proofs.
I would agree with Najib myself. Models theorems can only ever be applied to very formal logical subset of a formal logic. I dont know that any thing can be formulated about incompleteness of reality, based on some formal logical grammar. Seems its a matter of greater philosophy at some point. That said assuming you can concretely describe what it means to be virus or malicious, that is that this can be formulated as a mathematics question, then sure it can be shown.
Computers exhibit finite resources. Thus through brute force every state can be considered and if it is malicous.
This fails if combinations of states through time are considered, maybe? I can't say myself.
More or less, yes. Mathematics behind it in layman's terms, this is boiled down to a Bootstrapping Paradox, a type of temporal paradox that questions where information originated. This relates to this problem in that if you have an antivirus that detects all known viruses, but then the next day, somebody creates a new virus, there would be no signature in the old virus scan to detect the new virus. If you could conceivably take all computer viruses from the end of time, then beam them back to before now and created virus signatures from them all, where did the information come from? The future, or the past? Since the general consensus is that time travel is impossible for a number of reasons mathematically/physically, you can't have coverage of all viruses, only all known viruses.
