1. 22

  2. 3

    Compilers are big: most major compilers consist of several million lines of code. Their development is not stale either: every year, each compiler sees thousands of changes. Their sheer size and complexity, plus the pressure to continuously improve compilers, results in bugs slipping through. These compiler bugs may in turn introduce security vulnerabilities into your program.

    I was really not expecting this from Microsoft. But a company gather a lot of different people with a lot of different ideals…

    This makes me think about scc, a compiler tatgetting simplicity (through code correctness), portability (featuring easy bootstrapping). Maybe there are other compilers with similar goals, like pcc or somd that nickpsecurity quoted.

    1. 7

      I was really not expecting this from Microsoft.

      Well, it’s Microsoft Research, which often seems to be in the different universe than Microsoft. To me the post seems to be very much the thing you expect from MSR.

      1. 3

        “Microsoft, you hire researchers, they actually do a great job! What about starting to apply their advises?”

        1. 3

          Like sanxiyn said, MS Research is always doing great stuff. Look up VCC, Dafny, esp VerveOS, Gazelle Browser, Verifast, Midori, IronApps… those pop into mind immediately. The results rarely get used by ops side for who knows what reason.

          When they get used, there’s interesting results out of it. The SLAM driver verification tool is the reason you don’t see blue screens much anymore. ExpressOS was independent work with their tools on mobile OS. Too sleepy still to remember more.

          1. 2

            So it’s great that their projects are being in use.

            This supports the idea I have of megacorp as neither good or evil by nature, but have large tendencies for some (good or evil) practices.

    2. 2

      Those interested in this might also enjoy looking into CompCert, CakeML, Simpl/C, Dafny, and SPARK. Each uses some technique in the article with SPARK and Dafny making it easier to do imperative code but still takes skill/effort.