Is exploit-free software possible?

Question

I have heard that there will always be vulnerabilities in codes, software. However, I don't understand why it is not possible to have an exploit-free software. If companies keep updating their software, eventually there will be no vulnerabilities, right?

Answer 1

Software is too complex

This is by far the most important factor. Even if you just look at something like a web application, the amount of work hours put into the codebase is immense. The code works with technologies, who's standards are pages over pages long, written decades ago, and which offers features that most developers have never even heard of.

Combine that with the fact that modern software is built on libraries, which are built on libraries, which abstract away some low-level library based on some OS functionality, which again is just a wrapper for some other OS function written in the 1990s.

The modern tech stack is just too big for one person to fully grok, even if you exclude the OS side of things, which leads to the next point:

Knowledge gets lost over time

SQL Injections are now 20 years old. They are still around. How so? One factor to consider is that knowledge inside a company gets lost over time. You may have one or two senior developers, who know and care about security, who make sure that their code isn't vulnerable against SQL injections, but those seniors will eventually take on different positions, change companies or retire. New people will take their place, and they may be just as good developers, but they don't know or care about security. As a result, they might not know or care about the problem, and thus not look for them.

People are taught the wrong way

Another point is that security isn't really something that schools care about. I recall the first lesson about using SQL in Java, and my teacher used string concatenation to insert parameters into a query. I told him that was insecure, and got yelled at for disturbing the lesson. All the students in this class have seen that string concatenation is the way to go - after all, that's how the teacher did it, and the teacher would never teach anything wrong, right?

All those students would now go into the world of development and happily write SQL code that is easily injectable, just because nobody cares. Why does nobody care? Because

Companies are not interested in "perfect code"

That's a bold statement, but it's true. To a company, they care about investment and returns. They "invest" the time of their developers (which costs the company a specific amount of money), and they expect features in return, which they can sell to customers. Features to sell include:

• Software can now work with more file formats
• Software now includes in-app purchases
• Software looks better
• Software makes you look better
• Software works faster
• Software seamlessly integrates into your workflow

What companies can't sell you is the absence of bugs. "Software is not vulnerable against XSS" is not something you can sell, and thus not something companies want to invest money in. Fixing security issues is much like doing your laundry - nobody pays you to do it, nobody praises you for doing it, and you probably don't feel like doing it anyways, but you still have to.

And one more final point:

You can't test for the absence of bugs

What this means is, you can never be certain if your code contains any bugs. You can't prove that some software is secure, because you can't see how many bugs there are left. Let me demonstrate this:

function Compare(string a, string b)
{
    if (a.Length != b.Length)
    {
        // If the length is not equal, we know the strings will not be equal
        return -1;
    }
    else
    {
        for(int i = 0; i < a.Length; i++)
        {
            if(a[i] != b[i])
            {
                // If one character mismatches, the string is not equal
                return -1;
            }
        }

        // Since no characters mismatched, the strings are equal
        return 0;
    }
}

Does this code look secure to you? You might think so. It returns 0 if strings are equal and -1 if they're not. So what's the problem? The problem is that if a constant secret is used for one part, and attacker-controlled input for the other, then an attacker can measure the time it takes for the function to complete. If the first 3 characters match, it'll take longer than if no characters match.

This means that an attacker can try various inputs and measure how long it will take to complete. The longer it takes, the more consecutive characters are identical. With enough time, an attacker can eventually find out what the secret string is. This is called a side-channel attack.

Could this bug be fixed? Yes, of course. Any bug can be fixed. But the point of this demonstration is to show that bugs are not necessarily clearly visible, and fixing them requires that you are aware of them, know how to fix them, and have the incentive to do so.

In Summary...

I know this is a long post, so I am not blaming you for skipping right to the end. The quick version is, writing exploit-free code is really really hard, and becomes exponentially harder the more complex your software becomes. Every technology your software uses, be it the web, XML or something else, gives your codebase thousands of additional exploitation vectors. In addition, your employer might not even care about producing exploit-free code - they care about features they can sell. And finally, can you ever really be sure it's exploit free? Or are you just waiting for the next big exploit to hit the public?

Answer 2

The existing answers, at the time of writing this, focused on the difficulties of making bug free code, and why it is not possible.^†

But imagine if it were possible. How tricky that might be. There's one piece of software out there which earned the title of "bug free:" a member of the L4 family of microkernels called seL4. We can use it to see just how far the rabbit hole goes.

seL4 is a microkernel. It is unique because, in 2009, it was proven to have no bugs. What is meant by that is that they used an automated proof system to mathematically prove that if the code is compiled by a standards-complient compiler, the resulting binary will do precisely what the documentation of the language says it will do. This was strengthened later to make similar assertions of the ARM binary of the microkernel:

The binary code of the ARM version of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more. Furthermore, the specification and the seL4 binary satisfy the classic security properties called integrity and confidentiality.

Awesome! We have a non trivial piece of software that is proven to be correct. What's next?

Well, the seL4 people aren't lying to us. They immediately then point out that this proof has limits, and enumerate some of those limits

Assembly: the seL4 kernel, like all operating system kernels, contains some assembly code, about 340 lines of ARM assembly in our case. For seL4, this concerns mainly entry to and exit from the kernel, as well as direct hardware accesses. For the proof, we assume this code is correct.
Hardware: we assume the hardware works correctly. In practice, this means the hardware is assumed not to be tampered with, and working according to specification. It also means, it must be run within its operating conditions.
Hardware management: the proof makes only the most minimal assumptions on the underlying hardware. It abstracts from cache consistency, cache colouring and TLB (translation lookaside buffer) management. The proof assumes these functions are implemented correctly in the assembly layer mentioned above and that the hardware works as advertised. The proof also assumes that especially these three hardware management functions do not have any effect on the behaviour of the kernel. This is true if they are used correctly.
Boot code: the proof currently is about the operation of the kernel after it has been loaded correctly into memory and brought into a consistent, minimal initial state. This leaves out about 1,200 lines of the code base that a kernel programmer would usually consider to be part of the kernel.
Virtual memory: under the standard of 'normal' formal verification projects, virtual memory does not need to be considered an assumption of this proof. However, the degree of assurance is lower than for other parts of our proof where we reason from first principle. In more detail, virtual memory is the hardware mechanism that the kernel uses to protect itself from user programs and user programs from each other. This part is fully verified. However, virtual memory introduces a complication, because it can affect how the kernel itself accesses memory. Our execution model assumes a certain standard behaviour of memory while the kernel executes, and we justify this assumption by proving the necessary conditions on kernel behaviour. The thing is: you have to trust us that we got all necessary conditions and that we got them right. Our machine-checked proof doesn't force us to be complete at this point. In short, in this part of the proof, unlike the other parts, there is potential for human error.
...

The list continues. All of these caveats have to be carefully accounted for when claiming proof of correctness.

Now we have to give the seL4 team credit. Such a proof is an incredible confidence building statement. But it shows where the rabbit hole goes when you start to approach the idea of "bug free." You never really get "bug free." You just start having to seriously consider larger classes of bugs.

Eventually you will run into the most interesting and human issue of all: are you using the right software for the job? seL4 offers several great guarantees. Are they the ones you actually needed? MechMK1's answer points out a timing attack on some code. seL4's proof explicitly does not include defense against those. If you are worried about such timing attacks, seL4 does not guarantee anything about them. You used the wrong tool.

And, if you look at the history of exploits, it's full of teams that used the wrong tool and got burned for it.

^{†. In response to the comments: The answers actually speak to exploit free code. However, I would argue a proof that code is bug free is necessary for a proof that it is exploit free.}

Answer 3

You can have high quality code, but it becomes massively more expensive to develop it. The Space Shuttle software was developed, with great care and rigorous testing, resulting in very reliable software - but much more expensive than a PHP script.

Some more day-to-day things are also very well coded. For example, the Linux TCP/IP stack is pretty solid and has had few security problems (although unfortunately, one recently) Other software at high risk of attack includes OpenSSH, Remote Desktop, VPN endpoints. The developers are typically aware of the importance of their software as often providing a "security boundary" especially with pre-authentication attacks, and in general they do better and have fewer security problems.

Unfortunately, some key software is not so well developed. A notable example is OpenSSL that is very widely used, yet has messy internals where it's easy to introduce security flaws like Heart Bleed. Steps have been taken to address this, e.g. LibreSSL.

A similar effect happens in CMS software. For example, Word Press core is generally well engineered and has few issues. But plugins are much more variable, and often outdated plugins is how such sites are hacked.

Web browsers are a front-line in this. Billions of desktop users rely on their web browser to be secure, keep malware off their systems. But they also need to be fast, support all the latest features, and still handle millions of legacy sites. So while we all really want web browsers to be trustworthy security boundaries, they are not that currently.

When it comes to bespoke software - which is often web applications - the developers working on them are typically less experienced and security aware than core infrastructure developers. And commercial timescales prevent them taking a very detailed and careful approach. But this can be helped with architectures that contain security critical code in a small area, which is carefully coded and tested. The non-security-critical code can be developed more quickly.

All development can be helped with security tools and testing, including static analyzers, fuzzers and pen tests. Some can be embedded in an automated CI pipeline, and more mature security departments do this already.

So we've got a long way to go, put there is definitely hope in the future that there will be much fewer security bugs. And many opportunities for innovative tech that gets us there.

Answer 4

Yes...

As others have pointed out, it's possible to proof your code, and by such means demonstrate that your code will work exactly as intended. The difficulty with proofing timing and non-deterministic models (such as network interactions) is one of difficulty, not impossibility. The patches to Meltdown and Spectre show that even side-channel timing attacks can be accounted for and addressed.

The primary approach to building code such as this is to treat code as mathematics. If you cannot proof your code, do not treat it as bug-free. If you can, then you have ... only a shot at bug-free.

... but ...

Even if you can proof that your code is pristine, cannot release data except as intended, cannot be put into an erroneous or aberrant state, etc, remember that code on-its-own is worthless. If a developer writes code that has such a proof, but runs that code on hardware that itself contains hardware vulnerabilities, the security of the software becomes moot.

Consider a simple function for retrieving some encrypted data from memory, stores it in a CPU register, does an appropriate transform in-place on that register to decrypt, process, and re-encrypt the data. Note that at some point, the unencrypted data are in a register. If the available opcodes for that CPU hardware afford the possibility of a program that does not clobber that CPU register, running parallel to your proven code, then there is a hardware-based attack.

What this means, ultimately, that to have such an exploit-free software, you would need to proof first that you have exploit-free hardware. As Meltdown and Spectre (among many others) have demonstrated, commonly available hardware just doesn't pass that mark.

Even military spec and space spec hardware fails at this metric. The LEON line of processors, which see use in military and space deployments, are only hardened against Single Event Upsets (SEUs) and Single Event Transients (SETs). This is great, but it means there's always the possibility of an attacker placing the system in an environment with enough radiation to induce enough upsets and transients to place the hardware in an aberrant state.

... and more buts ...

So proofing the software and hardware is not enough. We must consider even environmental effects in proofing our hardware. If we expose a LEON4 to enough radiation to either overwhelm the casing OR cause enough induced radiation in the casing to overwhelm the processor, we can still cause aberration. At this point, the sum total system (software, hardware, environment) would be insanely complicated to fully and properly define to attempt such a proof.

... so no, not really...

Assume that we have devised an RDBMS that we've proofed the code, we've proofed the hardware, and we have proofed the environment. At some point, we finally hit the weak point in any security chain:

Idio... er, Users.

Our glorious database and our illustrious PFY make for an insecure system. The PFY -- let's be more charitable and bestow upon them the title 'JrOp'... The JrOp accesses the database and is given only that data the JrOp needs to know and nothing more, nothing less. In a moment of brilliance only JrOps can muster, our JrOp leans over to a coworker and mutters, "Did you see what User12358W just uploaded? Look at this!"

So much for our security...

... one last hope (and defeating it with absurdity) ...

Let us say, however, we imagine the future hypothetical where we've finally figured out human consciousness. Humanity has finally achieved a scientific and technological accounting of all human mental functioning. Let's further say this allows us to proof our system against even our users -- the appropriate feedback systems are built into the system to ensure our JrOp doesn't even THINK of revealing that which was revealed to the JrOp. We can leave the question of meta-ethics and manipulation to the philosophers -- speaking of philosophers...

Note that at every single step, we've utilized proofs.

"Ah-hah," exclaims the Pyrrhonic skeptic with glee. "You've assumed that some formal system, such as ZF/ZFC, Peano, non-naive Set theory, classical propositional logic, is sound. Why?"

What answer can be given? Between Godel and Tarski, we cannot even formally define truth (see Godel's Incompleteness Theorum and Tarski's Undefinability Theorum), so even the assertion, "well, we pick it because it seems good to use a system in alignment with reality," at core is just an unfounded assumption -- which means any proof our system is exploit-free is ultimately itself assumption.

... so no, it isn't.

While it may be possible to write bug-free code, by writing it as mathematical proofs, and thus technically attaining the top-level goal of 'exploit-free code', this requires looking at code in a vacuum. There is some value in this -- it's a worthwhile goal ("But that assumes wor--" "Most people do, deal with it Pyrrho"). However, never allow yourself the comfort of thinking you've ever succeeded at that goal -- and if you do, have the humility to title your code "HMS Titanic".

Answer 5

I want to answer sideways to the previous questions. I don't believe that bug-free software is theoretically impossible or that software is too complex. We have other complex systems with much lower error rates.

There are two reasons why exploit-free code will not happen within the forseable future:

Performance and other Optimizations

Many issues, including exploitable ones, are not cases of where we don't know how to write the code correctly, it is just that correct code would be slower. Or use more memory. Or be more expensive to write. Many shortcuts are taken in software to squeeze out more speed or for some other gains. Some of these shortcuts are the source of exploits

Fundamental Problems

The systems we use to create software today have fundamental flaws that lead to exploits, but are not in principle unavoidable. Our compilers aren't proven to be safe. The library system, especially the Node ecosystem (now copied by composer, cargo and others) of dynamically integrating hundreds or thousands of small packages through automated dependencies is a huge security nightmare. I'd have to use 72pt fonts to show just how huge. Almost all our languages contain fundamentally insecure constructions (the thinking behing Rust illustrates a few of them). Our operating systems are built on even older systems with even more flaws.

In short: At this time, the best we can do is basically "try not to mess up" and that just isn't enough for a complex system.

Conclusion

So in summary, with the software world as it is today, no. Exploit-free code is impossible with those tools and mindsets and dev environments unless we are talking about trivial or extremely self-contained (the L4 kernel that was mentioned already) code.

Theoretically, however, nothing stops us from building software from small modules, each of which can be formally proven to be correct. Nothing stops us from modelling the relations, interactions and interfaces of those models and formally prove their correctness.

In fact, we could do that today, but without fundamental advances in software design, that code would crawl, not run.

Answer 6

Is it possible? Yes. But not for the software you're looking for.

"Bug/Exploit Free" basically means that a program will have a sensible, safe response to any input. This can include ignoring that input.

The only software where this can achieved is small, trivial programs just beyond a Hello World. There are no exploits in this:

print("Hello World")

Because this code ignores all inputs, and outputs only a hardcoded string.

However, this code also accomplishes exactly 0 useful work for you.

As soon as you want to, for example, connect to the internet and download something, you'll be downloading data that you have no control over and might be malicious. Of course, there's a lot of restrictions our downloading software puts on that data to defend you, but it is impossible to defend against a threat angle that you're not aware of.

Answer 7

In security, we like to believe that nothing can be secured, only hardened.

This is because no matter how much you try to update your software and applications, Zero Day's exist. Especially if your software is worth hacking in to. This means although your team of security engineers might be able to patch the issue, the software can be exploited before the vulnerability goes public.

And the more applications you create in your software, the higher the chance of Zero days.

Answer 8

Yes

I'm surprised nobody has mentioned formal verification by its name (though Cort's answer does mention the L4 microkernel, which has been formally verified).

I'm not personally very familiar with formal verification, so I'll point to some relevant bits from the Wikipedia page on the topic; please refer to it for more information.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.[1]

Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. [...]

The growth in complexity of designs increases the importance of formal verification techniques in the hardware industry.[6][7] At present, formal verification is used by most or all leading hardware companies,[8] but its use in the software industry is still languishing.^{[citation needed]} This could be attributed to the greater need in the hardware industry, where errors have greater commercial significance.^{[citation needed]} [...]

As of 2011, several operating systems have been formally verified: NICTA's Secure Embedded L4 microkernel, sold commercially as seL4 by OK Labs;[10] OSEK/VDX based real-time operating system ORIENTAIS by East China Normal University;^{[citation needed]} Green Hills Software's Integrity operating system;^{[citation needed]} and SYSGO's PikeOS.[11][12]

As of 2016, Yale and Columbia professors Zhong Shao and Ronghui Gu developed a formal verification protocol for blockchain called CertiKOS.[13] The program is the first example of formal verification in the blockchain world, and an example of formal verification being used explicitly as a security program.[14]

As of 2017, formal verification has been applied to the design of large computer networks[15] through a mathematical model of the network,[16] and as part of a new network technology category, intent-based networking.[17] Network software vendors that offer formal verification solutions include Cisco[18], Forward Networks[19][20] and Veriflow Systems.[21]

The CompCert C compiler is a formally verified C compiler implementing the majority of ISO C.

Answer 9

Yes, if the security of the system is mathematically proven. It is not a new idea, the Trusted Computer System Evaluation Criteria, in short "Orange Book" originates from 1985.

In them, the highest level of security, named A1, is when we have verified design. It means that it is mathematically proven that there is no way to break the system.

In practice, proving the mathematical correctness (incl. security) of any software is very hard, and a very hairsplitting work. As far I know, no complete computer system has such a proof, but some systems (at least the VM/ESA kernel) were partially proven.

Note also, IT Security inherently deals with possible attacks from which we don't know, were are they coming from. For example, such a mathematical model would be fine and working for a system which - directly or indirectly - assumes that there is no way to eavesdrop its internal TCP communications. Thus, it would be eligible to get the A1 certificate. While in practice, such a system could be easily breakable on a compromised router.

In general, automatized (or partially automatized) correctness testing of programs, incl. their security testing, is a well-going computer science field since some decades ago. It resulted many well-referred publications and Phd degrees. But it is still so far away from the practical wide usage, as it was 25 years ago.

Answer 10

It's possible, but not economic without regulations that currently do not exist.

The answer about the proven to be correct kernel seL4 is very good in giving an example of bug-free code in the sense that it will perform exactly as described - and if they description is wrong, well, that might be called an exploit. But bugs in the description/specification are comparably extremely rare and it's debatable if they really even are bugs.

The limits that are also cited in the other answer all boil down to "we limited ourselves to the kernel, because we had limited resources". All of them could be solved by developing the hardware and surrounding software and client software in the same manner as the seL4 kernel.

If everyone did this, then writing, say, a provably correct website would become trivial, because all the tools you would be using would be provably correct and you would only be writing a little glue code. So the amount of code that would need to proven correct for a small project would be small. Right now, the amount of code that needs to be proven correct if you want to write a small provably correct program is huge because you would basically need to start over from scratch without having any of the tools available that were developed since the start of computers.

Some people today call for oppressive tools like like surveillance and censorship and trade blockades and counter attacks in response to digitization. If they instead switched to incentivizing secure software, for example by requiring a certain amount of liability (also called responsibility) from software and hardware manufacturers, then we would soon only have secure software. It would take much less time to rebuild our software ecosystem in a totally secure manner than it took to create it in the first place.

Answer 11

Currently, it's very costly to write bug-free code that is complicated enough. It's even more costly to verify that it is actually bug-free, or the verifier program is bug-free, ad infinitum. I don't think anyone already had a solution for the scale of most commercial software.

But I'd argue that some programs, which may have bugs, would be at least free of vulnerabilities. For example, a program that is supposed to run in a perfect sandbox such as a browser, and doesn't attempt to interact with anything except the user, or at least doesn't have any documented promises that other programs are supposed to trust. If there is something going wrong, it's a vulnerability of the sandbox, and not the program itself.

We have ways to design systems that accept a result only if multiple differently designed versions of a program agrees. And we have ways to make the parts of a program stateless. We could recreate the promises by using these methods. As a sandboxing program would have limited complexity, I'd argue that, in the distant future, there is some hope to make it eventually possible to write exploit-free code as long as all the used algorithms are provable. I don't know if it will ever become economically viable, though.

Answer 12

Most of the answers have focused on bugs that enable exploits. This is very true. Yet there is a more fundamental avenue for exploits.

If it can be programmed, it can be hacked.

Any system that can be programmed can be told to do stupid things, even malicious things.
Programmability can take many forms, some of which are not very obvious. For example is a word processor or a spreadsheet has a macro feature. This feature provides sequences to the user. If in addition, there are features providing selection and reiteration, suddenly it's very programmable.

If it cannot be programmed, the users will demand more flexibility.

Just about any complex application package will eventually create an environment where the users want to automate their routine behavior. This automation sometimes takes on the form of scripting, like Powershell or Python, but sometimes it comes about through something like a macro feature with a few extra bells and whistles for automation. When the builders accommodate the users, it's suddenly a programmable system.

Answer 13

Just think in terms of 'developing' an impenetrable building... and think of few possible scenarios and assumptions:

• is the budget limited? Always is! Bad actor with bigger budget could buy means of getting in (as in buy tools, bribing builders, ...)
• there is always environment scale beyond which you have no control: a region going rouge, a meteor striking crucial safety infrastructure, technological advances further down the line which you had no way of planning for, ...

You could let your imagination run wild with this example.

And now accept the fact that buildings are often simpler to defend as being physical objects, most likely simpler and rarely built from components with as long chains of dependencies or as hard to establish provenance as 3rd party software libraries are.

Answer 14

Theoretically, yes.

Although exploit-free software is possible, it is extremely hard to achieve, if you could program a piece of software to program for you, technically, this is possible. I have heard of people attempting to make something like this, although it is harder than it seems, creating a bot that can program for you, is harder than it seems. Another way a program could be exploit free is if the piece of software is mathematically proven. Although, man made code could not achieve something like this, other types of programming can be exploit free if it didn't require human input.

Answer 15

Writing perfect code is like building a perfect car. We might be able to build a perfect car but only for the age we are in. As the technology grows, ideas get shared and more brains get togather to solve problems then you might have something much better.

You are correct in saying that if a company keeps working on a software, then at some time in time they will be bug free. Thats true, but with time different technologies evolve and you make choice to either stay up to date with technology or just keep up with the same old perfect codebase.

Lets take example of facebook because they are a large group and are focused on on a single product. Facebook used to use jquery library for all the dynamic stuff a few years back. It was a cutting edge technology and everything was going great and never thought of replacing it. But to keep users engaged they needed to become much more dynamic. So as facebook grew and needed more and more dynamic functionality and realised that jquery was not fulfilling their needs.

Because no other website had that many users, no body actually understood the need for newer libraries. So they started to work on their own library called React. As time passed on more people started using the internet because of facebook and so obviously they got introduced to other sites as well. Now other websites also started to have the problems that facebook were facing, but fortunately now they had React Library to fullfil their needs instead of building a new one.

Google was having a similar problem and instead of using facebook's React they thought of building their own to address their specific needs. This will keep on going and there wont ever be a single codebase that is perfect.

Its the law of nature whenever something bigger arrives that drives more people to think bigger and do better than that, Similar to how more and more powerful characters keep on coming in Avengers.

Because time is the only unique entity and there never is an unlimited amount of time. Business owners as well as developers make triad off's. Triad off's in code can be something like:

• To be more optimized/faster or to be more manageable ?
• To focus more on security or to have a better user experience ?
• Should new features be more tested or to ship new features on time ?

We make these triad off's everyday...

Answer 16

For specific cases (programs), almost. In general, NO

1. For specific cases:

You can repeatedly refine a given program until most or all known forms of vulnerabilities (i.e. buffer overflows) got away, but many forms of vulnerabilities happen outside the source code. For example, suppose you compile such that almost or perfect program. This produces an object or executable program that you distribute. In the target computer it is exposed to malware that can modify such that binary code i.e. inserting jumps to malicious code that of course, are not in the original program.

2. In general

Is it possible to have a program, now or in the future, being able to validate the source code of any program for vulnerabilities ?

A bit of theory. Being a vulnerability-free program is a semantic property of programs, not a syntactic one. A syntactic property can be formalized (and hence, it can be detected by formal methods), but a semantic one cannot:

A semantic property is one that is not a trivial semantic property. a trivial semantic property is one that is always present or always absent in all and every program. A well known semantic property of programs is "This program will run forever" (the famous Turing's halting problem) because some programs will run forever, while some other won't. Turin proved that the halting problem is undecidable, so a formal method to test the halting nature of any program cannot exist.

The Rice's theorem states that that all non-trivial, semantic properties of programs are also undecidable. In fact, the proof is based in the fact that if a non-trivial semantic property of programs were decidable, it could be used to solve the halting program, which is impossible.

As another example of semantic properties, consider the property "This program is harmful". It is of course a semantic property and hence, as a consequence of the Rice's theorem a formal and deterministic malware detection program cannot be built; most of them use heuristics for their detection procedures.

Of course, as it is used in malware detection, you can use heuristics, artificial intelligence, machine learning, etc. to approach to a method for searching vulnerabilities in code, but a formal, perfect and deterministic one cannot exist.

Answer 17

The first rule of software testing (QA):

'It cannot be confirmed that the last bug has been found'.

I have coded since 1980 (also an electronics engineer) and none of my software has been exploited, that does not mean it couldn't be, just that nobody did it. Banking systems (and 'Snowden'-like systems) have auto-triggering warning/audits to log unauthorized access (I have worked on similar systems).

So, yes, exploit free software is possible, but how would you quantify/verify it?

Finally, look up FCC (USA) rules:

Part 15 of the FCC rules, which governs unlicensed devices, incorporates a fundamental tenet of U.S. spectrum policy: an unlicensed device must accept interference from any source, and may not cause harmful interference to any licensed service

Which means your Wi-Fi signal is 'exploitable' which in turn means the software on it is 'exploitable'.