Furthermore, as Microsoft has patched most of the basic memory safety bugs, attackers and bug hunters have also stepped up their game, moving from basic memory errors that spew code into adjacent memory to more complex exploits that run code at desired memory addresses, ideal for targeting others apps and processes running on the system.
```
Is all we can hope for in the security game a series of mitigations? As soon as we add layers of security (Stack cookies, ASLR, memory "safe" languages with exploitable runtimes, etc.) it seems like new methods are invented to bypass them and those methods gradually become widespread (ROP chains, runtime fuzzing, rowhammer, speculative execution exploits). What is the next "70 percent" of security bugs? Is there an end to this race?
I think the only thing in the future that can ever be as secure as in-person conversation and paper records is devices using zero-intermediary communication, in the style of an ansible https://en.wikipedia.org/wiki/Ansible, and extremely restricted storage which can only store data and not arbitrary application state.
sel4 shows that an endgame is possible wrt to memory safety, it's formally verfied to be memory safe.
It's sitting at ~25 to 1, proof code to implementation code. I think you could probably get that down to 5 to 1 or so by treating a lot of the work they did as a library. The proof covers a full equivalence from abstract spec to machine code, and you could reuse a lot of that. Sort of how it's not fair to include the LOC of your compiler even though you need that for your program ultimately.
Nope, sel4 is unsafe against modern Spectre/Meltdown attacks. Only Fiasco was recently made safe against these.
Secondly, Microsoft's own SecureMemZero is insecure against those attacks. It only applies a trivial compiler barrier, but no memory barrier, so you cannot use it to securely delete sensitive memory.
That's not an endgame if the resources required to block an attack are significantly greater than those required to make one. Moreover, verification is done with respect to specific properties that ensure no attacks of a particular kind. The more kinds of attacks you need to defend yourself from, the harder you need to work (and you will miss some). Not saying we're not making steps in the right direction, but no one thinks it's an endgame.
It's an endgame wrt to memory safety (like I said). sel4 is memory safe. All the other mitigations like ASLR, canaries, etc are just hacks around the fact that proving memory safety of existing codebases is a Sisyphean task.
And getting down to 5/1 proof to implemention is within the realm of what unit tests you should be writing anyway, so it's not that much of an economic investment.
I am not at all against formal verification. In fact, I evangelize it and use it myself quite a bit. But it is important to understand that it is very, very far from being a miracle cure.
All software proofs prove correctness of specific theorems about a program given certain axioms. Those axioms must include, at the very least, the conformance of the hardware to some specification. But hardware can, at best, conform to the specification with some probability. For example, when you write `mov rax, [rdx]` it is not true that the computer will, 100% move the contents of the address pointed to by rdx into rax, only that it will do so with some high probability. Therefore, any proof about a software system (as opposed to an algorithm, which is an abstract mathematical entity) is a proof of a theorem of the form, "as long as the system behaves according to my assumptions, it will exhibit behaviors consistent with my conclusions." And that is even assuming that your conclusions cover all possible attacks. As it is generally impossible to formalize the concept of an arbitrary attack, you generally prove something far weaker.
But none of this is even the biggest limitation of formal verification. The biggest would be its cost and lack of scalability. seL4 is about 1/5 the size of jQuery, and it is probably the largest piece of software ever verified end-to-end using deductive formal proofs as a verification technique. However much the effort of a similar technique can be reduced, it doesn't scale linearly with the size of the program (it may if the program does the same things, but usually larger programs are much more complex and have many more features).
> However much the effort of a similar technique can be reduced, it doesn't scale linearly with the size of the program
[citation needed]
Sure, you can write an arbitrary application where that's true, but AFAIK it doesn't have to be. IMO, sel4's really cool part isn't that it just was formally verified, but it's total design specifically for verifiability.
The argument reminds me of all the people in the late 90s talking about how unit tests would never take off because they tried to introduce it in their legacy spaghetti codebase, and it wasn't amenable to testing.
> IMO, sel4's really cool part isn't that it just was formally verified, but it's total design specifically for verifiability.
Well, they were very selective with their algorithm choices, so that only very simple algorithms were used. Whether that's cool or an unaffordable restriction depends on your perspective.
> The argument reminds me of all the people in the late 90s talking about how unit tests would never take off because they tried to introduce it in their legacy spaghetti codebase, and it wasn't amenable to testing.
Except that I've been both practicing and evangelizing formal methods for some years now. I argue in favor of using them, not against, but as someone with some experience in that field I want to make sure people's expectations are reasonable. Unreasonable expectations all but killed formal methods once before.
> Moreover, verification is done with respect to specific properties that ensure no attacks of a particular kind.
No. seL4 proved functional correctness. It eliminates all attacks, not just particular kinds.
Functional correctness means implementation matches specification. As a corollary, seL4 has no buffer overflows. Proof: Assume seL4 has a buffer overflow. Exploit it to run arbitrary code. Arbitrary code execution is not part of specification, hence implementation does not match specification, leading to contradiction. QED.
Above proof applies to use after free, or any other exploits enabling arbitrary code execution, including methods which are not discovered yet.
This is effectively the same idea behind Rust's `unsafe`. It represents the things you assume to be true. Of course, when compared to seL4, the scales are massively different. :-)
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.
Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels
```
Rowhammer and Spectre exploits hardware not working to spec.
These sorts of attacks using heretofore "unreasonable" exploitation of side-channel and hardware vulnerabilities are exactly what worries me. We have no solutions for these classes of attacks. Complex high-speed systems are still inherently unsolvably vulnerable, it seems.
Formal proofs prove certain theorems about your programs. If you could formalize the notion of an arbitrary attack you could prove it's impossible, but there is no such formalization. Of course, you don't need to verify the lack of a certain attack techniques, only their effect, and so you can certainly verify even with respect to undiscovered techniques, but this still would never cover all attacks regardless of their effect. E.g. you may be able to prove no arbitrary code execution, but you may still fail to verify no data leaks. If you have a data leak, you can steal passwords and certifications, and if you have those you can execute arbitrary code without any arbitrary code execution attack or privilege escalation. Note that this could occur even if the kernel is itself impervious to data leaks, due to vulnerabilities in user code.
Even with regard to what you do prove, the conclusions depend on certain assumptions about the hardware which, even if true (and they often aren't -- read some of the seL4 caveats) at best hold with high probability, not certainty.
I am an avid fan of formal methods, and have been using them quite extensively in the past few years, but you should understand what they can and cannot do. You can read about formal methods on my blog: https://pron.github.io/ The paper discussed here also mentions some common misunderstandings, about seL4 in particular: http://verse.systems/blog/post/2018-10-02-Proofs-And-Side-Ef...
Nevertheless, there is no doubt that a kernel such as seL4 has a much lower probability of being hacked than, say, Linux, given similar hacking efforts, and I would trust it much more. But it really isn't an endgame.
But does formal verification even help when you're up against side channel attacks on the hardware? Like the branch predictor or DRAM memory access timing.
Computer security is a fundamentally asymmetric game. Your entire stack needs to contain zero mistakes and an attacker only needs to find one. Also the resources you would expend trying to find and patch every last hole would break the economics. It is what it is.
>Also the resources you would expend trying to find and patch every last hole would break the economics.
If people built with things that weren't made of holes (ie. using memory safe languages), then there wouldn't need to be much effort in the "find and patch" side of things.
I'll agree with the sentiment that memory safe languages are less prone to security holes because by nature they entirely remove a whole class of issues related to managing memory...
but I can't help but think that it still stands to be the case that finding and patching the remaining holes that aren't related to memory management would still break the economics.
Perhaps the one thing I could imagine that might make a difference is regulations coming into force that mandated pentests / fuzzing for companies producing software doing a certain amount in revenue. It's been my experience that that stuff gets done but it's once in a blue moon. And stuff is always turned up. I'm yet to work anywhere where it is part of a regular process.
Even if it were I'm always blown away by security researchers who spend months and months attacking something and finally crack it then give a presentation about how they did it. There can't even be that many people on Earth with the level of skillset required.
I dunno... the economics of it seem to play out like "let's just deal with the fallout of an incident when it happens because that's cheaper than investing in security"
The asymmetric nature of finding holes vs not creating them combined with the asymmetric nature of the business value of investing in security is just a mildly awful combination.
If there is, it'll be a combination of two things.
One is you make things simple enough that finding the bugs is more realistic. WireGuard, not OpenSSL.
The other is that you make things modular, and once you have one of the modules right, you mostly leave it alone. Many people still use djbdns and qmail for a reason, and it's not the pace of new feature support.
These are trade offs. They do have costs. But it has proven to be more effective.
Well, that wouldn't eliminate everything (row-hammer, speculative execution), but it would probably get rid of the most common culprits - buffer overflows and use after free.
Things like row hammer will not get attention until they are commonly used. Rust does eliminate the most common vulnerabilities and should be seriously considered for any new project that would otherwise be written in C.
Nonsense. Rust safeties are massively overhyped. Not enough memory safety (comparable to Java, which is similarily memory unsafe), no type safety (unsafe keyword), not enough concurrency safety (not deadlock free, need to manually set mutexes). While there do exist safe and fast languages, Rust is not one of them.
If we all wrote in languages as memory-safe as Java, almost all these security bugs would go away.
Is Rust guaranteed to be 100% memory-safe? No, there could always be bugs in the compiler and/or unsafe code. (Aside: it annoys me how people consider the presence of an unsafe keyword inherently less trustworthy than a non-verified compiler/runtime system, when there is really little difference between them.) Is it a huge improvement? Yes.
Full agreement, but I think unsafe-phobia is mostly about user-extensible nature of it. unsafe in standard library is okay, because as you said it's no more dangerous than doing it in runtime. unsafe in "your" library is not okay, because I don't trust you to modify runtime either.
unsafe memory and unsafe types are not okay if you widely claim to be memory safe. Thousands of people actually believe these lies, and companies do makes decisions on these claims. It's much more memory unsafe than Java in fact. Java recently removed the unsafe tricks, whilst rust was once safe and went more and more unsafe since.
Obviously not. I've only worked on two different compilers/languages which do provide all three safeties, while you probably wouldn't even be able to name a single one. It's embarrassing.
It's a nice language, and safer than C/C++ but for sure not a safe one, even if thousands of newbies will repeat it constantly.
Yes, the goal is to increase the costs to the attacker as much as possible while having minimal added costs during development and runtime of the software. Statically proven programs are great security wise but they are expensive to produce, while adding ASLR is not perfect but comparatively easy to pull off.
```
Furthermore, as Microsoft has patched most of the basic memory safety bugs, attackers and bug hunters have also stepped up their game, moving from basic memory errors that spew code into adjacent memory to more complex exploits that run code at desired memory addresses, ideal for targeting others apps and processes running on the system.
```
Is all we can hope for in the security game a series of mitigations? As soon as we add layers of security (Stack cookies, ASLR, memory "safe" languages with exploitable runtimes, etc.) it seems like new methods are invented to bypass them and those methods gradually become widespread (ROP chains, runtime fuzzing, rowhammer, speculative execution exploits). What is the next "70 percent" of security bugs? Is there an end to this race?
I think the only thing in the future that can ever be as secure as in-person conversation and paper records is devices using zero-intermediary communication, in the style of an ansible https://en.wikipedia.org/wiki/Ansible, and extremely restricted storage which can only store data and not arbitrary application state.