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

IoT core is not new, not a secret, and Microsoft makes no effort to hide it.

Your MS reps need to be fired if they do not know about IoT Core, or chose not to tell you.

Also, I personally find it best to never rely on a rep from any company to give me the truth about their product line. I will make time to do preliminary research (at least) myself.

Microsoft will ALWAYS push IoT Enterprise over IoT Core because IoT Core costs nothing, and generates no revenue for Microsoft (other than the associated Azure revenue that they hope you spend connecting those IoT Core devices to infrastructure.)

All that said, I recommend looking into IoT Core if it interests you. It is very well suited for certain kinds of use cases.

Now I'm starting to wonder if you even read the "No Output" letter and understand its implication? You essentially called a bunch of Microsoft employees productivity drains on the rest of the company.

The fact that you think a cancelled project means it is the same as DEC's "No Output" team likely means you don't understand what the "No Output" team even was at DEC or the implication for the people within it.

You absolutely do need to present proof of what you're saying, because it is a serious charge for both Microsoft and those employees alike.

Surely there was output.

Async/await, TPL, Span<>, blittable structs, safe stackalloc, .NET Native, and a couple of other minor features come from M# (System C#) usage.

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.

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.

>> Nonsense. Rust safeties are massively overhyped.

No. They are not. You obviously have not done your homework on the subject.

I don't know of any technique to model or avoid timing attacks that wouldn't drastically slow down execution to the point of being impractical.

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

I read this and thought, "this can't be right, they must be assuming some things."

According to them, they, sensibly, are indeed assuming some things to be correct without proof: http://sel4.systems/Info/FAQ/proof.pml

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

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.

From the assumptions page: http://sel4.systems/Info/FAQ/proof.pml

```

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.

No, because linux OS's includes a lot of software in their repositories and new packages are added all the time. Look closer at the list. "40 Debian CVEs in 2019" breaks down to this:

* Google Chrome: 36

* Artifex Ghostscript: 1

* ZeroMQ: 1

* macOS CUPS: 2

* Debian: 0

You are right. One current estimate is that Linux is introducing security bugs at a rate faster than they are fixed.