You probably don't need HACM. Microsoft Research has produce quite a number of software and compilers for producing provably secure low level code and drivers.
When are we getting that in Windows? It needs to start with a formally verified OS (and firmware), then build a provably-correct protocol/driver/app/etc stack on top.
MS was working on Singularity [1] a while back, but its webpage speaks of it in past tense, so it doesn't appear to be an ongoing project.
Microsoft, and more importantly Microsoft Research, have many, many projects tackling this. Off the top of my head: the P programming language, F*, Dafny, and a bunch of others (I think the last two are part of something called Project Everest). Microsoft Research is one of the biggest players in this field. A lot of their efforts span multiple departments so you will have to search around.
Yup, I'm aware they do a lot of work on this, and hired up half the Haskell and PLT researchers in the world, and have a bunch of projects on it scattered across their web properties.
And maybe some of it is trickling down into parts of Windows or .NET, like F# and others, but I wish they'd develop an entire ecosystem around it and make stronger push to commercialize it.
With all the aforementioned resources MS has at their disposal, by now they should have their own version of SEL4, comprehensive tooling for secure-by-design and correct-by-construction application development, and optionally secure sandboxed containers for backward compatibility with legacy apps. Though ideally MS funds a Manhattan project for rewriting the most popular apps using their SxD and CxC tooling.
Singularity was on the right track, but they let it languish and die for some reason, when instead they could be rebuilding an entire secure/correct ecosystem with Singularity as the focal point, and commercializing it with enterprise support, and selling it to governments and large enterprises with significant security concerns.
It is hard to iterate and make changes when your codebase relies on human/machine assisted proofs. Great for airplanes and cars when regulatory approval means iteration is slow. Not so great for consumer software.
Good point, though I’d suggest most consumer software, at least office apps and similar needed by the government, are mature enough they don’t need rapid iteration. Most new features being added to them these days are optional at best.
