we should all be using Rust then :)
Maybe you can do a proof of concept by writing a mini-Linux using Rust.
[deleted]
Microsoft: 70 percent of all security bugs are memory safety issues
51–60 of 180 posts
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#52we should all be using Rust then :)
Right because Rust will prevent all the issues of Unsafe usage that an OS uses all the time ...
You're being sarcastic, but I think you'll find the limited use of unsafe in Philipp Oppermann's series informative: https://os.phil-opp.com/
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#53In 2015 they become the first gold contributor to OpenBSD
https://www.zdnet.com/article/microsoft-becomes-openbsds-fir...
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#54To quote the article: ``` 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 seri…
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…
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.
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#55To quote the article: ``` 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 seri…
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…
Reinforcement learning can be used to improve theorem proving, but it probably needs more research:
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#56Earlier quoted context omitted.
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…
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.
With a model of the full system, quite possibly. That's one of the things that makes me so excited for RISC-V.
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#57Earlier quoted context omitted.
Okay thanks. I could Google that. So it's code written in C# or VB or another supported language, compiled by JIT to a common bytecode running on a virtual machine and probably a whole slew of libraries that target that VM too. Okay. I have no idea why I'm struggling so much with that. Thanks.
No problem. Sorry for the brevity, I was on my phone and have texter's thumb, but you got me to stop being lazy and go to my PC, so hey! Two years ago, .NET in an everyday connotation would imply C# (VB.NET is mainly only used in legacy corporate environments, although there was nothing stopping people from implementing greenfield VB projects until last year or so) and an installation of the .NET Framework (equivalen…
Thank you so much. Your recent timeline of events really helps clear things up. Because a few years ago I did think I got it when I thought of .NET as C# + a monolithic suite of libraries.
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#58Earlier quoted context omitted.
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
I wouldn't be surprised if it's easier to rewrite the kernel than to rewrite Office.
Why is that?
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#59Linux is also written in C.
And it has MORE reported CVEs than Windows: https://www.cvedetails.com/top-50-products.php?year=2018
It's also OSS and it is much easier to surface security bugs for Linux than for Windows.
In my own research, I have attempted to send Microsoft security bugs only to be told they would be backlogged and reviewed later (which never happened to my knowledge).
Re: Microsoft: 70 percent of all security bugs are memory safety issues
#60Just 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, as cool as it was, was Microsoft's "no output division" (see https://archive.computerhistory.org/resources/text/DEC/dec.b... for context). It existed so that very senior engineers wouldn't go elsewhere and cause trouble for Microsoft. It had fullfilled its purpose in that regard. I strongly suspect that some of Google's more ambitious endeavors serve the same purpose.