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.

From the book Secrets & Lies by Bruce Schneier, page 154.

• I think it is already impossible to do a complete and formal definition of what a computer virus is in the first place, i.e. describe what exactly the "maliciousness" is. But such definition is needed in order to even argue about decidable vs. undecidable problem. But even if ou find a kind of useful albeit not perfect definition it will probably be undecidable because of the halting problem. Mar 17, 2018 at 17:17
• Post is locked because it is generating a ton of speculation and opinion. The question is asking about the source of a paper referenced in another article. Jan 24, 2019 at 7:51
• This questions reminds me of a dialogue by Douglas R. Hoffstadter explaining Gödel's Incompleteness Theorems: genius.com/Douglas-hofstadter-contracrostipunctus-annotated
– 0112
Jan 26, 2019 at 23:03
• The Halting Problem says yes? If you can't tell if a program halts, it would seem to follow that you also can't tell if a program does something malicious/is a virus. Jan 29, 2019 at 10:39
• Your title asks a different question than was claimed in the quote. The quote claims not all viruses can be stopped. This is obviously different than asking if they can all be detected as in your title. (This is true case since it is possible to stop a virus without detecting it)
– Matt
Jan 29, 2019 at 13:38

19 Answers

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.

• Not to mention, "malicious" is an almost entirely subjective term. I've seen disassembly programs get flagged as malware because the AV author apparently considered reverse engineering to be a "malicious" thing (even though I can't think of a situation where someone who didn't want said disassembler on their computer would end up with it there). Jan 25, 2019 at 20:17
• @DoktorJ: The point is that even if you come up with some rigid non-syntactic definition for "malicious" (regardless of if that definition misses some viruses, or includes some non-viruses), it's still impossible to flag all/only malicious programs. Jan 25, 2019 at 22:49
• @Stéphane Chazelas Self-replication is a non-trivial semantic property as well, ergo it is undecidable. Jan 26, 2019 at 23:49
• I think Rice's theorem only applies if you have to decide ahead of time if a program is malicious, and if you don's allow false positives. If the virus scanner can e.g. intercept API calls, modify the program (e.g. to insert runtime checks) and occasionally reject a "safe" program, it should be possible to prove safety. That's basically how e.g. a Java VM can offer safety guarantees, isn't it? Jan 28, 2019 at 18:07
• @JeroenMostert: No, it has nothing to do with static vs runtime analysis. The difference is in whether the definition is semantic or syntactic. "A list of the actions the program is allowed to perform" is a syntactic definition. This is why writing a sandbox is so much easier than writing an antivirus. Jan 28, 2019 at 23:11

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:

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

• Cute. I mean, utterly irrelevant, but also cute and clever. Jan 23, 2019 at 14:39
• @supercat, the problem with your version is that you need to come up with a definition of "virus behavior" that can be programmatically applied. For example, a Javascript Bitcoin miner might be virus-like when visiting the New York Times website, but desired behavior when visiting Joe's Discount Pirate Software. Encrypting the contents of your hard drive may be good behavior when it's your FDE software doing it, and virus-like when it's being done by ransomware.
– Mark
Jan 23, 2019 at 21:17
• This antivirus program would detect itself as a virus and shut itself down, making it incapable of detecting anything else. Jan 23, 2019 at 21:43
• @supercat A lot of viruses are installed with the operator's consent, but do things the operator didn't consent to. However, if you prevent automatic running, then a reboot would kill it, just not the side effects.
– Poik
Jan 23, 2019 at 22:41
• Sounds like an argument for white-listing wanted programs only, as in a repository of only tested software to install (maybe even FOSS, not unlike most linux repositories), to at least avoid installing malicious things on purpose Jan 24, 2019 at 10:53

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.

• Schneier states here that this is the result he was referring to when he made a very similar statement some time later in another context: schneier.com/blog/archives/2009/07/making_an_opera.html Jan 23, 2019 at 11:31
• @Stephan: For every possible binary there exists a hypothetical platform for which it is virulent and a hypothetical platform for which it is not virulent. This theorem is stronger than Rice's theorem as it applies to hypercomputers also. Jan 23, 2019 at 16:47
• @user1067003, I'm not a computer scientist, but I'm pretty sure the phrase "there is no algorithm" means that there is no possible algorithm, not just that there is no known algorithm. Otherwise it would not be a very interesting result. (The proof as written probably only applies to classical computers though, it might need to be redone to cover quantum computers or any other more abstruse architectures.) Jan 24, 2019 at 20:45
• This answer heavily relies on an external link to answer the question. Can you maybe sumarize the arguments from that paper? Jan 25, 2019 at 8:52
• @HarryJohnston: Quantum computers are equivalent to Turing Machines in terms of computability, so no, it doesn't need to be redone. In fact, pretty much every computer scientist believes that every physically-realizable computer is, at best, equivalent to a Turing Machine Jan 25, 2019 at 22:57

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.

• A counterexample: I'll specialize the original question (losing its generality), by defining a virus as any `bash script` which invokes `rm -rf /*` when run with no arguments; and I'll define an antivirus as a version of bash interpreter which denies that `rm -rf /*` command from execution. I hope you agree that we can go all the way down rigorously defining what a "bash interpreter", "execute", etc means mathematically. Did I just formulate a weaker version of the original question? Does this disprove your claim that it can't be mathematically formulated? Yes and yes. Jan 23, 2019 at 18:36
• @ulidtko No. You cannot just arbitrarily define a virus to be anything you want. Otherwise, I could define a virus as "software which has 'anti-virus' in its name", which would not help the discussion any, as that is a discussion of philosophy, not of security or mathematics. In fact, your definition of virus is like saying "I define the set of even numbers to be {2}". Go ahead and make such a system if you want, but you have not disproven anything by doing so. As Michael has suggested, "virus" cannot be mathematically defined in any way useful to this conversation. Jan 23, 2019 at 20:48
• Re: "At the very least, that requires a mathematically sound definition of what a 'virus' is": Not necessarily. If there are characteristics that would apply to any definition of "virus", then you may be able to mathematically formalize some of those characteristics without needing to produce a specific complete definition. That partial characterization could be enough to let you apply Rice's theorem. Jan 23, 2019 at 21:16
• @ulidtko On the same basis, I could define a virus as any program that sends an email. I'm sure I could do some reasoning about that class of programs, but it would tell me nothing about the class of programs that ordinary people classify as viruses in the real world. Jan 23, 2019 at 22:07
• @MichaelKay: I'm aware; I only mentioned Rice's theorem as an example of why your statement was incorrect. Sorry if that was unclear. Jan 23, 2019 at 22:17

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.

• The case (4) is not just boring, but indicates a more likely scenario and problematic scenario. Consider a code that contains some calls if (cannotHappen) installEveryVirusEver(); where cannotHappen cannot happen if the machine works ok, but is likely to occur if the machine is overclocked. How to correctly classify that? Jan 25, 2019 at 12:34
• @HansOlsson Yeah, it'd require generalizing the ontology to capture problems that don't fit well into the deterministic model; presumably we'd have to consider the ensemble of possible outcomes, then classify them according to how secure we'd deem them, or else just concede that programs in general may act maliciously even if not designed to. I was hoping to provide a nod to issues like row hammer, where the presumption of error-free operation can really mess up analysis.
– Nat
Jan 25, 2019 at 12:42
• "brute forcing an encrypted message" Why not run the program in a sandbox, and figure out how it decrypts the message itself? IIRC that's how some antivirus already works. Feb 1, 2019 at 5:50
• @micsthepick Running a program in a sandbox is a better-scaling solution that's liable to be generally superior in non-trivial cases, so you're right that that'd tend to be preferred in practice. Just, the question is about anti-virus in the sense of preemptive analysis; sandboxing is a different subject.
– Nat
Feb 1, 2019 at 6:03
• Worth noting that the halting problem example can be bypassed by simply flagging any program that has the potential to install a virus be virus (I.e. dedicated byte code to do that exists so presumably the software can do so). Jan 3, 2020 at 3:29

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.

• The problem of defining malicious is hardly a show-stopper. Different people will have different interests that go into constructing a definition appropriate to them, but that's okay. Jan 23, 2019 at 23:55
• So, someone produces a link on a web site that installs software on your machine to monitor what movies you are watching, and feeds the data to MegaCorp. Is this a virus? Does your answer vary depending on whether the "someone" is Microsoft, versus a teenage hacker? Does your mathematical assessment of the software take into account the trustworthiness of the originator? In short, can this actually be formulated as a mathematical problem? Jan 24, 2019 at 0:25
• @Michael AI compete is the (I believe somewhat more woolily defined) idea that "you can't solve this problem without also creating an artificial general intelligence". I don't think it's as clearly defined as NP, so it's probably not amenable to mathematical proof. Jan 25, 2019 at 7:37
• Thanks, that makes sense. I had heard a less rigourous version of this, along the lines of: here are five (or 10) problems which would be high value to solve, but it turns out that solving just one of them (creating an AGI/ASI) would actually provide the means to solve the others as well (assuming it doesn't wipe us out / make us its pets / etc.) Jan 25, 2019 at 18:25
• Reminds me of the old question "what is a weed?" with the answer "anything you don't want growing in your garden" , re: your comment to @R Jan 25, 2019 at 18:27

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

• If the statement was somehow reducible to the halting problem, the interesting bit would be showing that this is the case, not just name-dropping it. Or, to put it more directly: no, this is definitely not what Church and Turing proved (it's not even close to what they set out to prove). Jan 23, 2019 at 13:13
• Yes @JeroenMostert you have right. I was wrong. Church and Turing proved that there does not exist mechanism that decide if such program that detect all viruses could be even written. I have confused the concepts. Uncle Bob was blogging about it:blog.cleancoder.com/uncle-bob/2018/06/21/… Jan 23, 2019 at 13:20
• So, does this answer need to be deleted or completely rewritten? Jan 23, 2019 at 13:53
• Martin's blog, while amusing, commits some of the more common fallacies when it comes to explaining the halting problem. For example, "the specification of a program is a great big Diophantine equation in a bazillion unknowns" is wrong, plain and simple. Certainly that's a way of specifying a program (if you squint), but you need to be much more careful than that to make meaningful statements over what proofs say is and is not possible. Explanations like these tend to obfuscate rather than clarify -- the actual math is subtle, but for the good reason that these things are subtle. Jan 23, 2019 at 14:15
• I'm not too sure this answer is wrong: 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 unless we run it to find out. Note that the referenced paper also refers to the halting problem: web.archive.org/web/20140525233117/http://grnlight.net/… Jan 23, 2019 at 22:16

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.

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.

• Downvoter please explain why. As far as I can tell, this proof is valid. Jan 25, 2019 at 11:54
• I didn't downvote, though this does look a bit off, as there doesn't appear to be a contradiction. This is, if `IsVirus(P)` is true, then your script isn't viral; however, `IsVirus(P)` claimed that `P` was viral, not your script.
– Nat
Jan 25, 2019 at 12:20
• Realistically, nobody would care if `IsVirus` reported that `P` was indeed a virus, even though it wouldn't actually be one with that definition of `P`. Indeed, it's not at all unreasonable to call `P` a virus, as it's designed to do bad things and get clever with us if we attempt to identify it. In other words, the very act of invoking `IsVirus` could be used as a virus identifier for any program that isn't our own anti-virus program. (There are ways to "fix" this line of reasoning, but they involve getting much more precise with our definitions.) Jan 25, 2019 at 13:08
• @Nat `P` is the script Jan 25, 2019 at 21:25
• @Matthew Hah, opps, missed that part! That does seem to be a contradiction then, though it appears to be a self-referential problem, like "This statement is false.", rather than virus-classification.
– Nat
Jan 25, 2019 at 21:59

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

• You are answering the question like a programmer (which I am). It's useless. Their question does not live in the realm of reality but rather theory. It's like when I try to convince people that no "AI" (Artificial Intelligence) can be evil or have a soul. They point out some research or some Elon Musk/Alex Jones-tier article and I point out the word "Artificial". They still won't listen. Being an expert does not help you when arguing with most people. Jan 23, 2019 at 22:26
• "Being an expert does not help you when arguing with most people." While true, they are asking in website whose only purpose is to ask "experts" in the subject. Why ask somebody if not willing to accept his/her answer? Jan 24, 2019 at 13:09
• Everybody is an expert. Jan 26, 2019 at 5:32

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" what? Not it has not been proven? But read the other answers that show that it has been proven? A very confusing start to your answer. Can you clarify? Jan 23, 2019 at 16:41
• The no is a direct answer to the question subject line. I'll elaborate. Jan 23, 2019 at 16:55
• Shall I get out the virus that uses rowhammer to overwrite the kernel security checks? Jan 23, 2019 at 17:02
• @Joshua: The runtime environment can fully detect or prevent that. For example by running the program under an interpreter. See "suitable access control model". In this case the hardware is buggy and allowing any direct low-level access to that part of the system (making requests to the memory bus) is insufficient access control. Jan 23, 2019 at 17:13
• While good, it will not prevent all viruses. @Ray allowed you to side-step the issue with that specific example, but that will not always be the case. What about where the exact same software can be viewed in one use case as useful but another use case as malicious? Consider software that allows remote control of your computer, written and used initially for good. Then others abuse it. The gamer calls it awesomeware when his buddy gets him XP while he sleeps, and their neighbor considers it malware when their enemy blasts obnoxious white-noise. One person's trash is another's treasure. Jan 23, 2019 at 21:07

Can we have an antivirus that detects all viruses?

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.

About "proving"

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.

• Your argument goes a bit too much in the other direction -- there are obvious gaps in what biological evolution can practically achieve (no cow has jumped over the moon), and the absence of "solutions" to certain "problems" is hard to accept as absolute proof that something can't be done unless you demonstrate why we couldn't possibly do any better. In particular, the mechanisms by which viruses and anti-virus software are "evolved" and "selected" are quite different. Even the word "virus" has become a misnomer when it comes to current malicious software (which rarely copies itself). Jan 23, 2019 at 11:18
• @JeroenMostert I've just reported a fact. While you imply that fiddling with thoughts inside our heads would yield more satisfactory results, in this case the number of repetitions and the huge pools of specimen involved is good-enough for me. That is, I assume it's vastly more probable for a human brain to overlook something here, than for the entire biosphere checking it for so many generations. (But - yes! - in some other cases our thinking can be superior, of course. Good for us!) Jan 23, 2019 at 11:32
• Cars are impossible. Proof: billions of years of evolution have not yielded wheels. Q.E.D. This fails, of course, because the parallels between biology and engineering only go so far -- you don't even need to presuppose smart inventors for this. Likewise computing. We've spotted some cute parallels between replicating programs and biological viruses way back when, but that's as far as it goes, and actual replicating programs have become no more than theoretical curiosities, while malicious programs are dead yet kicking. Is the biological parallel still valid and insightful? I wouldn't assume. Jan 23, 2019 at 11:49
• Whether or not proofs are possible is not the question. You have side-stepped answering the question. There was a reference made and the framing is made in that context. This is a non-answer. Jan 23, 2019 at 12:11
• In addition to the shortcomings pointed out in previous comments, this answer (probably accidentally) implicitly relies on incorrect assumptions about the equivalence between biological and computer viruses. Just because both are called “viruses” doesn't mean that they have identical relevant properties. The name is a metaphor, not an accurate definition. Jan 23, 2019 at 14:56

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.

• This relies on the unstated assumption that "antiviruses can't detect viruses that didn't exist, or weren't known, when the antivirus was created/last updated". This is key to the question, so just assuming it's true means that your answer has no actual substance. Also, for some viruses, this assumption is clearly false, since heuristics do work on some viruses. All of the talk of time travel is just fluff. Jan 24, 2019 at 5:32