Dtyjlui

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 virical. It logically follows that such a program will detect ALL possible viruses:

• All code is detected by your antivirus (C → D)


• All viruses are code (V → C)


• All viruses are detected by your antivirus (V → D)

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.

1. If you merely want to detect all viruses without further constraint, then simply flag anything and everything as a virus, and you're done.




2. 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.




3. 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.




4. If you allow that the computer can produce random errors, then any program can be a virus.

Case 1: Complete virus detection

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.

Case 2: Impossible to correctly classify in a general, unbounded scenario

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.

Case 3: Possible by brute-force search in bounded scenarios

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.

Case 4: Machines that can error can have viruses spontaneously emerge

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.

Discussion on the quote in the question

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.

https://en.wikipedia.org/wiki/Entscheidungsproblem

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:

• A program which encrypts all my files. Is it a cryptolocker ransomware or a full disk encryption tool?


• A program which allows remote access to control my computer. Is it a trojan or is it Team Viewer?


• A program which creates network connections to all kinds of computers all over the internet and exchanges obscure data with them. Is it a a botnet or a distributed computing platform?


• A program which sends all my personal files to a remote server. Is it spyware or is it Cloud Backup?


• A program which downloads executable files from the Internet and runs them. Is it a malware dropper or is it Steam?

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.

No, you can not, because the difference between malware and a useful program is completely subjective. Any "evil" behavior can be intended behavior. How do you tell the difference between:

• Cryptolocker ransomware and a full disk encryption tool?


• A trojan and a remote administration tool?


• A botnet and a distributed computing platform?


• A spyware and a fileshare program?


• A dropper and a package manager?

You can't, because from a purely technical perspective they do the exact same things. The only difference is in the intention. One acts against the interest of the user, the other does 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.