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?
-
51It depends on how big of a software we are talking about. If it's a small toy with a $0.20 microcontroller in it, where all the software does is blinking a LED, then yes, it's possible. But most software is way more complex than that.– vszCommented Oct 21, 2019 at 4:41
-
60"if companies keep updating their software, eventually there will be no vulnerabilities" No, because they keep adding new features, removing old ones or changing them. Each time this happens there is a chance a mistake was made that adds a new vulnerability.– QwertieCommented Oct 21, 2019 at 4:44
-
27Theoretically software can be bug free. Large, complex software is unlikely to be bug free but with enough effort you could make it bug free.– MichaelCommented Oct 21, 2019 at 9:12
-
11@marshalcraft What exactly do you mean by that comment? How does Turing-Completeness affect the exploitability of code?– user163495Commented Oct 21, 2019 at 10:23
-
14@MonkeyZeus Every vulnerability is a bug, but not every bug is a vulnerability.– user163495Commented Oct 21, 2019 at 13:19
17 Answers
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?
-
61It is possible in theory, but I have no idea why you would claim that tor or any particular bitcoin client are exploit-free. Just look at tor, for example, and you see plenty of bugs with it. The extremely short short-version is "No sufficiently complex software is bug-free."– user163495Commented Oct 20, 2019 at 21:24
-
30@Zheer we sometimes find horrible vulnerabilities in security-critical open source code that was written 10 or more years ago by respected experts doing so carefully (because the code was considered important security-wise) and that has been reviewed many times by many people over these years not noticing that vulnerability. So we have evidence that all these factors are not sufficient to have vulnerability-free code.– PeterisCommented Oct 21, 2019 at 9:06
-
18@marshalcraft Here is a concrete story of an old Windows component screwing folks over big time. Furthermore, I never mentioned Windows itself. I just said "OS component".– user163495Commented Oct 21, 2019 at 10:34
-
14@marshalcraft The Google Nexus 7 phones used to get really slow after they'd been running a while. Eventually Google tracked it down to a 27 year old memory leak in the Linux kernel itself. It's not just Windows. All complex software has vulnerabilities. Commented Oct 21, 2019 at 13:58
-
11@Zheer Automatic vulnerability scanners exist, and they get used. But with automatic systems, you get false positives and false negatives - meaning you will get reports for things that are not vulnerabilities, and no reports for things that are. And keep in mind AI is not a magic bullet– user163495Commented Oct 21, 2019 at 14:45
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.
-
58It's also worth noting that all this proof does is ensure that the behavior of resulting binary 100% matches the abstract specification. Thus, if the abstract specification has a bug - some unintended consequence of the interaction of specified features enables some interesting attack - then the binary will also have it. And many security flaws really are holes in the specification or some protocol, not in the implementation.– PeterisCommented Oct 21, 2019 at 9:11
-
6See also CompCert a C compiler proved to follow the C standard (without this you cannot really guarantee any correctness of C programs...) Commented Oct 21, 2019 at 12:18
-
5Hardware-based security failures are not nearly as impossible as we'd like. Well-known, current examples include row hammer, meltdown, and spectre. Further, it is normally impossible to prove the absence of side-channel attacks. Side-channel attacks are reliant on implementation details; there is no guarantee that a proof covers every possible category of side-channel (admittedly, such a guarantee might be theoretically, but not practically, possible in the case of quantum computing).– BrianCommented Oct 21, 2019 at 13:01
-
11@CGCampbell I'd argue that "bug free" is the low bar to pass. Only once you are bug free can we even talk about exploit free meaningfully. Commented Oct 21, 2019 at 15:21
-
5And in many of those cases, the “wrong tool” was C. Even one of the inventors of C wrote something like “If your code is more than X SLOC, you should be looking at Ada.” X was either 1500 or 15K—I no longer have that book to check. Today, there are several languages more robust than C, yet people still cling to the dinosaur. In the book “C traps and pitfalls” almost two thirds of the errors described are impossible in better languages.– WGroleauCommented Oct 21, 2019 at 16:35
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.
-
10You mentioned the shuttle, and that reminded me: The Apollo Mission Computer had a divide by zero bug that almost prevented Apollo 11 from going to the moon. (when the fault occurred, it took out a protective algorithm that prevented the gyros from tumbling.) Commented Oct 21, 2019 at 15:24
-
This is an interesting one. Of course, there is always a trade off between robustness and time to deliver, and if we are designing a simple web form with low risks incurred from usage then we aren't going to spend a fortune on testing and quality assurance. On the other hand, in my experience, most projects are non trivial and nearly all of them would benefit in long term costs if more testing and quality assurance was given. The problem I see often is that many software projects are carried out in situations such as banks/telcos, where safety-critical culture is lacking.– SentinelCommented Oct 23, 2019 at 8:35
-
To add some (ironic) humor:The space shuttle programs (developed in the late 1960s and early 1970s) may have been bug free, but the Space 'Program' itself was full of bugs! (The poor'Challenger' crew knows this...R.I.P). Commented Oct 23, 2019 at 15:20
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".
-
I was wondering, what does "writing it as mathematical proofs" mean?– ZheerCommented Oct 21, 2019 at 20:59
-
1It could mean something as literal as using something like Prolog or more conceptually as 'writing the proofs then writing the code according to the proofs and the chosen language's specification.' Commented Oct 21, 2019 at 21:06
-
1We might have to reduce our requirements a bit, down from "make code that cannot be exploited even in principle" to just "code that is difficult enough to exploit that no conceivable human would be smart enough to figure out how to do so". Then we just have to worry about the AIs... Commented Oct 22, 2019 at 3:34
-
2This is the correct answer: yes you can write perfect software with enough effort (read: $$$) but it's irrelevant because that does not guarantee security. +1. Commented Oct 22, 2019 at 19:32
-
1@Zheer it means, for example, writing in Coq, a pure functional language which allows to prove mathematical assertions, declaring lemmas and implementing proofs. Commented Oct 23, 2019 at 14:11
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.
-
4You should give some examples of what you mean by those performance-related concerns. This seems dubious to me. Sure – if you write some given algorithm in Coq for the purpose of verifying it, that'll generally run stupidly slow. But most of that is due to the runtime handling of the dependent types. Often enough, the actually needed program parts can be extracted as OCaml or Haskell, and that can give quite decent performance. Perhaps not quite as fast as a hand-tuned C or Rust implementation, but also not “crawl, not run”. Commented Oct 22, 2019 at 11:33
-
2@leftaroundabout I assumed that was referring to the perf optimizations enabled by e.g. undefined behavior in C: compiler generates faster code by assuming integer operations don't overflow, no out-of-bounds array accesses, no null pointer dereferences, no uninitialized memory reads, etc. Commented Oct 22, 2019 at 15:37
-
@JaredSmith maybe that's what Tom meant, but then the point is definitely not valid except in the sense “don't use C for security-critical applications”. E.g. Java avoids most of these problems without major performance hits, and certainly Rust and OCaml do. Commented Oct 22, 2019 at 15:41
-
-
2I don't mean one specific type. The Intel CPU issues were also caused by overzealous performance optimizations. Lots of input validation issues are caused by people thinking "nah, this won't happen, I don't need to check for it", then yes, compiler optimisations, then shortcuts in code, then assumptions about data, the list goes on.– TomCommented Oct 23, 2019 at 5:26
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.
-
2If I compile this code and invoke the executable with output redirection and your hard drive is completely full then bad things might happen. Commented Oct 21, 2019 at 21:26
-
4@gnasher729 I don't think that you could blame that problem on the 'hello world' program -- any bad things that happened (i.e. worse than an 'out of disk space' error message) in that case would be due to a bug in the OS or the OS's filesystem. Commented Oct 22, 2019 at 3:30
-
5Note that it is possible to exploit the code above but not where you think. Way back when Unix was being invented Ken Thompson as a joke introduced a Trojan horse into the one and only C compiler in existence that would crash Unix if any program intercepts a specific input (see his seminal essay win.tue.nl/~aeb/linux/hh/thompson/trust.html). While it's true that this "cheats" by exploiting the compiler, all exploits exploits things outside a program's source code: rowhammer exploits how RAM is manufactured, CRIME exploits statistical anomaly of compressed data etc. Commented Oct 22, 2019 at 7:07
-
2@Zheer IMO, you'd be exploiting the hardware, not the program.– GloweyeCommented Oct 22, 2019 at 13:39
-
3@Zheer per gloweye's comment, the difference is semantic not practical. No matter how often we pretend otherwise for the sake of our sanity, no program is independent of the hardware it runs on. Or the software it runs on (e.g. the operating system or virtual machine) for that matter. In other words, yes. Commented Oct 22, 2019 at 15:32
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.
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.
-
1Correctness is not bug free. In my 20 years of experience 90% of bugs in the wild comes from buggy specification, not buggy code. So a 100% correct program can still be buggy Commented Oct 22, 2019 at 7:11
-
Keep in mind, that things can be verified in implementation, but still have unforeseen vulnerabilities. Quantum cryptography is known mathematically (by all known physics) to be unbreakable. However, attacks on implementations have been found. The hardware is implemented exactly as specified, the mathematics behind the specification is verified... yet, attacks were still possible: researchgate.net/publication/… Commented Oct 22, 2019 at 13:35
-
I mentioned "verified design", from the orange book. But I admit that formal verification looks more accurate.– peterhCommented Oct 23, 2019 at 7:27
-
1+1 and I'd add that you might also use formal proof assistant tools. Commented Oct 23, 2019 at 15:01
-
While exploit free software is possible, it can NEVER be quantified/verified. Commented Oct 23, 2019 at 15:08
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.
-
1Well, there is a C compiler which "is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues". I suppose that this does not imply bug-free, but it is a big step. Of course a C compiler is probably small by today's standard (for example it is probably much smaller than the software in my color TV remote or my watch) but it is not trivial and does something genuinely useful. Commented Oct 23, 2019 at 14:41
-
@PeterA.Schneider Thanks, nice to know! However, it is only a proof that the compiler is correct, thus it does not generate bad binary from a good source. It does not imply, only requires, that all the software created with it, are correct.– peterhCommented Oct 23, 2019 at 16:55
-
Indeed :-). The software you compile with it may be buggy as hell. But I was refering to the compiler itself as a non-trivial proven correct program. Commented Oct 23, 2019 at 17:12
-
@PeterA.Schneider I imagine a language, more clearly, an extension to any language, what we could call proof. Proof would be a language describing, why the code is correct. The proof could be created only by humans, but both the validity of the proof (i.e. the proof is correct), and that it relates to the code underlying, could be verified algorithmically. There could be interessant side-effects. For example, in practical software development, the complexity / resources of the code + proof would need to be minimized, and not only the code alone.– peterhCommented Oct 25, 2019 at 8:30
-
@PeterA.Schneider Such a proof + code would be essentially a language in which it is impossible to write buggy code. There won't be automatized testing needed any more, actually nothing would be needed, and the only source of the problems would be the bad modelling or task statement.– peterhCommented Oct 25, 2019 at 8:33
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.
-
We'd also have to throw away all existing software (except for seL4 and CompCert). Yes, really, all of it. Commented Oct 21, 2019 at 15:59
-
1@immibis That might or might not be what would be economic if there were penalties to insecure software. I do imply in my very last sentence of the answer that it might come to that. But it's unlikely. It would be stupid to introduce sudden and large penalties, it would need to be gradual transition. So people might also gradually harden their software. Provable correctness isn't the only way to write secure software, although it would probably make insurance of liability much easier.– NobodyCommented Oct 21, 2019 at 16:16
-
Regardless of what is most economically viable, we'd have to throw away all existing software right now, because it's not secure. Until the new software is written, it's back to pencils and paper. Commented Oct 21, 2019 at 16:19
-
@immibis As I reiterated in my comment, obviously this is not an instant switch. That's why maybe we would want to start now as opposed to when we're even deeper in the mess and someone starts a "cyber war".– NobodyCommented Oct 21, 2019 at 17:15
-
Bugs, vagueness, or other problems in the spec are frighteningly common, at least in my experience. Especially when some feature is added at a future point in time, the interaction between New Feature and Old Features is often not fully explored in the spec. It's fine to say "we implemented it as written", but if it's a real problem you're still going to be there in the middle of the night/weekend/your vacation fixing it. Commented Oct 21, 2019 at 21:26
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.
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.
-
"If it can be programmed, it can be hacked." No. If it was programmed wrong or to a bad spec - it can be hacked. Exploits are not some magical living things that pop up on their own. Commented Oct 22, 2019 at 18:29
-
If you can come up with a clean way to divide programs into a productive group and a counterproductive group, then you are right. I assume that such a clean partition is not possible. Commented Oct 23, 2019 at 7:11
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.
-
1An apt analogy. There is no exploit-free complex system. Be it software or otherwise.– MartinCommented Oct 23, 2019 at 7:55
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.
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...
For specific cases (programs), almost. In general, NO
- 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.
- 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.
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'.
-
How does the " auto triggering warning/audits to log unauthorized access"work? If you exploit their system how can they log the unauthorized access?– ZheerCommented Oct 23, 2019 at 15:37
-
There are two types of exploitation, authorized and unauthorized. An authorized person is allowed to access a system within specific parameters (times/days/allowed menu items,etc). An unauthorized user also falls in to that category as well as doing something without logging in. Logging is 'easy', triggering means the script and/or database must be able to alert/control activity of the user/script ($$$). Commented Oct 24, 2019 at 1:51
-
Your WiFi section does not appear to relate to the rest of your answer, appears to make a colossal leap in logic, and a misinterpretation of Part 15; "radio interference" does not mean "exploit".– schroeder ♦Commented Oct 25, 2019 at 12:08
-
@schroeder: I can exploit anything! I have the skiil,that means there are others out there. The question is 'exploit free software' and it cannot be done because the vessel is exploitable! Also, I have DESIGNED and BUILT FCC compliant devices, so I know the FCC regulations and implications. Commented Oct 25, 2019 at 13:57
-
And you are still reading Part 15 wrong. And you keep making errors in logic. You are correct, the question is 'exploit free software' not 'hazard-free systems'. Exploits in the "vessel" are out of scope in the question, even if Part 15 somehow meant "WiFi exploits".– schroeder ♦Commented Oct 25, 2019 at 14:19