Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Microsoft: 70 percent of all security bugs are memory safety issues

zdnet.com

Post reply on HN
Print view View original

141–150 of 180 posts

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#141

Post by pjmlp »

ilovecaching wrote: post #75

Rust couldn't solve all of these bugs, but it certainly would have drastically reduced the total amount. The code would also be drastically easier to write and debug. C++17 is still a total mess to write, despite what Microsoft might tell you in their docs. Really doesn't make sense to me, outside of the sunk cost fallacy, why Microsoft isn't pivoting to Rust if they want to write C++.

Microsoft is a big C++ shop, we would all be running AOT compiled .NET code post Windows Longhorn if it wasn't for the political wars between DevDiv and WinDiv.

Just notice that on current desktop and mobile OS SDKs, Windows is the only one where C++ still gets a place at the GUI table. Everywhere else it just got pushed down the stack.

So while some divisions would like a world of purely .NET (AOT/JIT compiled), others would rather that it did not exist.

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#142

Post by pjmlp »

coldcat wrote: post #79
ilovecaching wrote: post #75

Rust couldn't solve all of these bugs, but it certainly would have drastically reduced the total amount. The code would also be drastically easier to write and debug. C++17 is still a total mess to write, despite what Microsoft might tell you in their docs. Really doesn't make sense to me, outside of the sunk cost fallacy, why Microsoft isn't pivoting to Rust if they want to write C++.

you could ask the same question for every os. And none choose Rust even the recent like fushia. BTW go ask Linus to switch to Rust I'm waiting for you there.

Linus is never going to switch to anything else other than C, UNIX is married to C.

So it is always going to be something else, not UNIX related.

Fuchsia uses Rust and Go in several areas.

Microsoft is using Rust on VSCode, Azure and IoT Core.

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#143

Post by pjmlp »

Animats wrote: post #62

This late? With Microsoft's move to C# and the Static Driver Verifier? The latter pretty much fixed this for drivers, which used to be the biggest source of kernel crashes. I thought Microsoft was past this.

There is still a strong C and C++ community at Microsoft.

They are the only OS vendor (on consumer space) still having a full stack support for C++, with internal pushes to keep it going.

https://kennykerr.ca/2019/01/25/the-state-of-cpp-on-windows/

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#144

Post by pjmlp »

reallydude wrote: post #33
skyde wrote: post #2

we should all be using Rust then :)

> Microsoft: 70 percent of OUR security bugs are memory safety issues Fixed the title. This is not an analysis about general software errors.

Linux is much worse currently, hence the Kernel Self Preservation project being pushed by Google.

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#146

Post by pjmlp »

nineteen999 wrote: post #46
theamk wrote: post #12

Earlier quoted context omitted.

Obsessed much? This has no mentions of Rust anywhere. Given it's Microsoft, they are probably thinking about .net.

Microsoft haven't even rewritten Office in C#/.Net yet, what makes you think they are ready to rewrite/replace the Windows kernel with it? https://news.ycombinator.com/item?id=17305332

How do you think Office 365 works?

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#147

Post by pron »

sanxiyn wrote: post #99
pron wrote: post #69

Earlier quoted context omitted.

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 on…

> 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 executio…

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.

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#148

Post by mike_hearn »

millstone wrote: post #132
max76 wrote: post #76

As an industry we should deprecate all unmanaged code. We've proven time and time again that even very professional and highly scrutinized unmanaged code can have critical data safety faults. Yes, I understand this includes Linux, Windows, BSD, Darwin (iOS, MacOS, watchOS, etc), The Android Runtime, and lots of critical software that runs on top of those systems. We have the tools to write very efficient managed code…

Agreed on principle but not sure it can be bootstrapped. What would you write, say, v8 in? Rust doesn't have any provisions against type confusion, JIT bugs, etc, and v8 seems way too complex for a formal verification.

That's extremely easy to answer.

The answer is you'd write an interpreter for JavaScript in Java, use a partial evaluation framework also written in Java to convert it to a JIT compiler, and then run it on a multi-purpose optimising polyglot virtual machine that's also written in Java. Such a thing would be fully bootstrapped and fully managed.

And usefully, it exists already. That's what happens if you run JavaScript on SubstrateVM using TruffleJS and Graal:

https://www.graalvm.org/

The closest thing you find to unmanaged code is parts of the garbage collector, where "SystemJava" is used, a dialect that gives access to pointer arithmetic. But everything else including the JIT compiler itself is fully managed.

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#149

Post by pron »

monocasa wrote: post #73
pron wrote: post #69

Earlier quoted context omitted.

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 on…

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

Re: Microsoft: 70 percent of all security bugs are memory safety issues

#150

Post by mike_hearn »

pjmlp wrote: post #137
Someone1234 wrote: post #4

Just a painful reminder that they scrapped Midori[0] their managed Operating System based on Microsoft Research's Singularity project[1]. Even if it only replaced Windows LTSB/Embedded, I'd still prefer an ATM, checkout, or gas station terminal I was using was running on managed code. Doubly so for the next generation of Nuclear Powered submarines[3]. Plus between virtualisation and silo-ed software management ("Apps…

Midori was a victim of the WinDev vs DevDiv political wars. The most recent example is Kenny Kerr complaining that although they made a big effort to migrate from C++/CX into C++/WinRT, the large majority prefers to code in .NET nowadays. https://kennykerr.ca/2019/01/25/the-state-of-cpp-on-windows/ However many of the Midori outcomes have landed in .NET, namely .NET Native, async/await, TPL, span, blittable structs,…

Was it? How do you know that?

As far as I am aware the only public information on Midori comes from Joe Duffy's blog which didn't discuss why it got cancelled.

Beyond the general issue of the well known managed vs unmanaged wars within MS, it would appear to be the case that Midori sucked up massive investment within MS and had little to show for it in the end - a nearly 10 year effort to build a fully managed OS, but one that focussed entirely on trying to be competitive performance-wise with Windows, rather than providing entirely new functionality and new ideas. So they spent years doing things like hand-optimising libraries to get rid of vtables and ended up with something that wasn't really .NET (it eschewed threading and .NET compatibility), and wasn't Windows, and whose primary strength was "it's written in a managed language" which isn't very interesting to actual users.

Post reply on HN