4 ms·

In addition to what others have already said, actually preventing major breaches like the recent Solarwinds hack. Eg, besides the tinfoil hat stuff, just getti

In addition to what others have already said, actually preventing major breaches like the recent Solarwinds hack. Eg, besides the tinfoil hat stuff, just getting the basics right. Personally I'd like to see the entire US govt IT infrastructure rebuilt around DARPA's HACMS project [1]. Get rid of Windows, base it all on SEL4 Linux or similar, rebuild the apps (everything in userspace), etc. That would significantly reduce the attack surface. Huge project obviously, but one can wish. [1]:https://www.darpa.mil/program/high-assurance-cyber-military-systems https://www.darpa.mil/program/high-assurance-cyber-military-...

ampdepolymerase 6y ago
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.
- dylan604 6y ago
  You missed the part about basing everything on SELinux4. That would mean drop Windows. I'm all onboard for that.
- SkyMarshal 6y ago
  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. [1]:https://www.microsoft.com/en-us/research/project/singularity/ https://www.microsoft.com/en-us/research/project/singularity...
  - ampdepolymerase 6y ago
    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.
    - SkyMarshal 6y ago
      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. I wonder why this hasn't happened yet. https://en.wikipedia.org/wiki/Secure_by_design https://en.wikipedia.org/wiki/Secure_by_design https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process/correctness-by-construction https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process...
      - ampdepolymerase 6y ago
        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.
        SkyMarshal 6y ago
        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.

ampdepolymerase 6y ago

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.

dylan604 6y ago
You missed the part about basing everything on SELinux4. That would mean drop Windows. I'm all onboard for that.
SkyMarshal 6y ago
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. [1]:https://www.microsoft.com/en-us/research/project/singularity/ https://www.microsoft.com/en-us/research/project/singularity...
- ampdepolymerase 6y ago
  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.
  - SkyMarshal 6y ago
    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. I wonder why this hasn't happened yet. https://en.wikipedia.org/wiki/Secure_by_design https://en.wikipedia.org/wiki/Secure_by_design https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process/correctness-by-construction https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process...
    - ampdepolymerase 6y ago
      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.
      - SkyMarshal 6y ago
        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.