Yes, you're reading that title right. It's saying unhackable. Are you confused or angry? Welcome to the "wonderful" world of formal verification. Perhaps it's not that wonderful if you have to do the formal verification itself though. Considering the outcome and your use case it might be really helpful or even necessary.

Warning

I try to be as technically accurate as possible, while not overcomplicating things. I'm aware that the main audience of Sejuice readers consists of people that are really technically interested and skilled. Still, I try to be as inclusive as possible considering people who are either just starting or don't know about this specific niche in infosec that well. Due to simplification of things though, some more or less important info might either not be given their fair amount of attention or they might be completely left out (because they're either too complex and too far off the original subject, or simply because I take them for granted and accidentally left them out (sorry in that case)).

This article is supposed to be an introduction to the subject and my style of writing is supposed to be entertaining, and interesting, but lacking in monotone. When I talk about things that are very technically specific and it's not directly clear what you'd have to look for I most of the time link to the sources.

Preface/Abstract

Computers are complicated. Most of the time they're really a pain in the ass for all of us even. Yet we somehow ended up in this industry. Either because we have a love-hate relationship with computers, or because we want to make some money. I guess the second choice was really a flop for most of the people in our industry. Besides that, not just people in infosec hate computers. Software developers, frontend folks and regular people of almost every age do. Basically, ranging from your mom to your grandpa.

We all can agree that technology sucks, maybe not for the same reasons but still. Yet another problem we face and I do while writing this post, is that you can't compare all computer things to other subjects etc., at least not without leaving out important information or becoming too abstract. This is just something that I've personally noticed, either by observation of other people in the industry, or by observing myself. In that sense, please be aware that I try my best to share my knowledge in the most comprehensive way, but sometimes I'm unable to simplify things.

What I want to make clear, is that computers are very complex nowadays and additionally have many flaws due to different reasons. Most notably for me, because of legacy systems and compatibility with legacy systems. Obviously, there are many other problems, but this article can only be so long and shouldn't bore you to death.

Besides hardware flaws and exploits though, we'll focus on something really abstract that really is kinda out of control. Software. Hardware is in a way easy to understand, at least easier than software. Hardware is built on logic and many hardware manufacturers use formal verification as well. Software is already more complex than hardware anyways, since the software runs on the hardware and not the other way around. In a sense, software is just a higher abstraction of hardware. Of course, this is a quite "controversial" way to put it, but I'm just guessing that you know what I mean by that statement.

I mean, you would theoretically know what a simple circuit design would do, but I believe nobody truly can explain even a simple C program (considering the way the C program is compiled for a given architecture, how the operating system deals with it and finally how it runs on the given processor). This is an "unfair" comparison of course, but that's nothing bad in this context. Through that statement, we just assume that software is always going to be more complex than hardware.

What also makes hardware more interesting is combinational logic. Combinational logic (as you can most likely guess) is logic that combines "logical" statements or the like, to build a bigger logic statement. For example, we all know AND gates. AND as described as a "logical statement" means, that only if both inputs are positive the result will also be positive. From that we can derive, that every other input where just one or none inputs is positive, the output will be negative. This means we can create an easy truth table with just 4 outcomes (since 2^2, because two inputs and either positive or negative input possibilities). Combining multiple logic gates though, creates the hardware you're using right now.

As we all know though, computers run software on their hardware. Thing is, hardware manufacturers are the main users of formal verification (no worries, we'll get to it very soon) and not software developers. We notice this quite often, since mostly the software fails on us, but not the hardware. Software relies mostly on software testing instead of formal verification. Don't get me wrong, testing is way easier, economically feasible and most of the time does its job. Sometimes though, we can't just rely on testing and we shouldn't. Imagine if companies like Boeing or Ford would rely just on testing for their products. Nobody would wanna fly with a Boeing plane anymore or buy a car from Ford. Understandably so, there just are some things that are not allowed to crash. Where error doesn't mean a minor inconvenience, but the death of people, economical catastrophes or similar.

Foundations of Formal Verification

So, now that you've read all this text what we'll explain here will be way easier to understand. With formal verification, you generally wanna prove the correctness of whatever you're doing. To prove the correctness of hardware or software for example, you'll have to translate it into a formal specification though. Formal specifications in turn are underlying formal methods of mathematics. Going to the core of formal verification though is even more complex, it's really a mess of logic, mathematics, paradoxes and more stuff that I can't even put in words. You'll have to experience the madness yourself to really understand it, but for now it's better to put the madness aside. Instead let's focus on the essentials.

Formal verification isn't really just one thing. There are many approaches to formally verify something, we'll get to that later in this blogpost. As I already stated, you can formally verify hardware or software. This makes it quite complicated for me to talk about all the appliances in more detail as you can surely imagine. You just eventually have to do some research yourself or maybe read something over again, before you truly understand it.

The basis

Formal verification is (unlike testing) about writing mathematical proofs, which show the correctness (or incorrectness) of all possible inputs of a given algorithm. Beyond this short explanation basically, every approach to formal verification is different. This is (as I already mentioned) because of the different applications for formal verification, as well as the different approaches.

Good luck learning into this one :)