Microsoft applies for a patent for a verifying a 'safe' operating system

Microsoft applies for a patent for a verifying a 'safe' operating system

Summary: Microsoft has applied for a patent for an "automated, static safety verifier" that will help verify the type- and memory-safety of an operating system. And why should anyone care? There are some connections to other Microsoft projects (and potentially, products) worth considering.

SHARE:

Microsoft has applied for a patent for an "automated, static safety verifier" that will help verify the type- and memory-safety of an operating system.

And why should anyone care? This isn't the Monkees coming to Zune, after all. But there are some connections to other Microsoft projects (and potentially, products) worth considering.

The patent application in question, noted first by Charon at the Ma-Config.com blog, is for tools and techniques that can "mechanically verify the safety of every assembly language instruction in the OS, run-time system, drivers, and applications, except the boot loader (which can be separately verified)."

What I'm most interested in is the OS that has been verified by these tools. That OS -- which Microsoft is calling "SafeOS" (but which also seems to go by the name "Verve") -- includes a Nucleus for accessing hardware and memory; a kernel for building services on the Nucleus; and applications that run on top of the kernel. The Nucleus, written in "verified assembly language," is what handles garbage collection, interrupt handling, device access, etc.

Garbage collection and type safety? Haven't we heard something about this before?

We have, indeed. A couple of years ago, I blogged about two interrelated projects in development at Microsoft, codenamed "Redhawk" and "MinSafe." Supposedly, these two projects were precursors to Midori, Microsoft's stealth distributed OS project.

Redhawk was the codename for new managed code work being done by the Developer Division, while MinSafe was the codename for the complementary managed code initiative on the Windows side of the house. Both projects were said to be aimed at providing a new managed-code execution environment that will be more lightweight and more appealing to developers who are put off by the perceived overhead of the current Common Language Runtime (CLR) at the heart of the .Net Framework, according to sources. Redhawk deliverables, according to my sources, included a new back-end compiler and new runtime that would still provide type safety and garbage collection, but perhaps not the rest of the functionality that is currently part of the current .Net CLR.

SafeOS should not be confused with ServiceOS -- another operating-system-related research project from the company. ServiceOS is the successor to Microsoft's "Gazelle" and "MashupOS" projects. SafeOS is a derivative of Microsoft's Singularity microkernel research project, but SerivceOS is more about the browser (designed as an operating system). SafeOS also sounds like a more generic, proof-of-concept entity than anything that is likely to morph into a commercial product. ServiceOS has the markings of something that some day could be commercialized (in my opinion).

Speaking of ServiceOS, Ma-Config also found a note on the Microsoft Research site explaining how ServiceOS could impact Microsoft's commercial offerings.

"The ServiceOS project aims to address many challenges faced by our Windows Phone platform, post Windows 8 platform, the browser platform, and Office platform," according to the note. It mentions a demonstration of a ServiceOS prototype that is MinWin-based and "refactors Trident to have a multi-principal OS-based design for the browser platform." (Trident is the rendering engine that is part of Internet Explorer.)

Topics: Operating Systems, Legal, Microsoft, Software

About

Mary Jo has covered the tech industry for 30 years for a variety of publications and Web sites, and is a frequent guest on radio, TV and podcasts, speaking about all things Microsoft-related. She is the author of Microsoft 2.0: How Microsoft plans to stay relevant in the post-Gates era (John Wiley & Sons, 2008).

Kick off your day with ZDNet's daily email newsletter. It's the freshest tech news and opinion, served hot. Get it.

Talkback

27 comments
Log in or register to join the discussion
  • Verification . . .

    Verification of code is an interesting area of study from a computer science point of view - but it has its weaknesses.

    -Thanks to the halting problem and related problems, there are some fundamental limits to how well you can verify code. Some types of code can never be verified completely.

    -Sometimes the issue isn't with the program - it's with the target user or target market. The programmer may verify that the program does one thing, but the user may have actually be thinking about something else. You can verify it does what you think it should do, but that's not always what the user thinks it should do.

    -Bugs in the verifier can allow bugs in the code. It becomes a classic "who watches the watchers?" style problem. While it's certainly better than no verification at all, the truth is that true perfection is elusive, and we are nowhere near the "perfect" machines commonly found in Sci-Fi fiction.

    -Verification is usually more difficult to do than unit testing. It's a lot more math/logic-heavy and proofs can be tedious to write. IMO a good test suite can create the same quality code with less effort.

    -Automated verifiers can cause problems when code does strange things on purpose. This happened to Debian Linux when some RNG code used a memory trick to try to increase the entropy of the random numbers. They tried to "fix" the odd problem, which lead to the RNG losing its randomness. This lead to a major breach in some security packages, because the lack of randomness made them easy to crack.

    You really do want to know [i]why[/i] somebody is doing something before assuming it's a bug because a verifier said it's broken - especially if the code you are trying to verify is not your own. Although intentionally doing strange stuff with memory isn't recommended, some devs still do it.

    In any case, it's interesting to see what Microsoft does with it. It does serve to show that they are aware of their reputation for being insecure.
    CobraA1
    • marketing

      it seems like it will be used as part of their marketing strategy - just like "get the facts" used vulnerability counts instead of actual penetration tests, where the latter is infinitely more valuable than the former.
      ~doolittle~
  • MS has finally figured out ....

    how to make a safe OS? ;-)
    Economister
    • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

      @Economister
      not yet, wait for Win15; in the meantime, don't forget to buy your antivirus and antimalware.
      theo_durcan
      • for every action, there is an equal and opposite reaction

        Would it really matter what version you waited for? The bad guys will just reverse engineer and decompile... e.g.

        TDL4 Rootkit Bypasses Windows Code-Signing Protection
        http://threatpost.com/en_us/blogs/tdl4-rootkit-bypasses-windows-code-signing-protection-111610
        "The boot option is changed in memory from the code executed by infected MBR"

        Ouch
        ~doolittle~
      • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

        antivirus and anitmalware dont do anything as the os allows viri to bypass and or turn them off.
        MS should really work on stop writing OS's that have single points of failure. relying on 99% of the programs running/responding to be stable is idiotic yet there it is.
        bspurloc
    • They sure did...years ago. Your comment is decades too late.

      @Economister: [i]MS has finally figured out ....
      how to make a safe OS?[/i]
      ye
      • No, in that case....

        @ye

        their patent is late
        Economister
      • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

        XP was already declared the most secure OS EVER so why did vista win7 etc come about and ruin that!
        bspurloc
    • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

      @Economister windows 7 is safe as long as your not dumb.
      Jimster480
  • Who cares?

    Glad you put the word 'safe' in quotes, because Microsoft wouldn't know a safe operating system if it bit them on the left big toe.

    The way you describe it, it sounds as if they're trying to move parts of the .NET CLR into the operating system, which would be a bad move because it would result in a much slower kernel than the already bloated and slow kernel that is Windows.

    There's always going to be a trade-off between speed and security. The more checking you put into the kernel, the more slowly the whole OS runs.

    If they really wanted Windows to be secure, they'd open up the source code and let the open source community help them find their bugs. But their "not invented here" mentality continues to cost users every day. Viruses, identity theft, botnets and DDOS attacks -- all of these could be stopped if there were more eyes looking at the source code, finding and fixing these security vulnerabilities before they become problems.

    And this is why I use Linux.
    roncemer
    • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

      @roncemer - Sorry to tell you this but the open source community is NOT the answer to every question in the software world.

      Riddle me this Batman: If Linux were truly secure, why do I get security updates to my Linux systems more often than I get security updates from Microsoft on my Windows systems? Why isn't there one monolithic update to Linux that fixes everything once and for all?

      Answer: Because the Open Source community is not perfect either.

      How long has the Open Source community had to get Linux right and yet still they are failing?

      Yeah...
      PollyProteus
      • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

        @PollyProteus Are you kidding me right now? The reason why there isn't a magical patch that fixes all of the operating system issues is because technology itself evolves. And as that evolution continues, new vulnerability issues will emerge.

        The reason why Linux gets MORE updates is because with millions of people WATCHING the malicious attacks as they emerge; they're quickly shot down before the developers at Microsoft can notice. And I can place a bet that some of the issues by the developers on the Linux kernel that have been condemned; developers at Microsoft, Apple, and Oracle have taken note of and attempted to quench in their software.

        The Open Source community hasn't ever failed to get Linux right; it's constantly under metamorphosis.
        jacky.alcine
    • Open Source updates... from who? Anyone?

      @roncemer

      I start with the assumption that any OS will be exploited if it "lives in the city", i.e attains market share.

      There's little to suggest Linux would be automatically better in this scenario, especially given its roots in UNIX... these are the same roots that gave us open-to-spammers smtp, remember?

      What puzzles me, is how one would "trust" updates were Linux to be pounded as heavily as Windows is today. Sure, it's nice that anyone can code these, and may be obliged to disclose the source code as per OSS licensing. But how do I know these "patches" aren't in fact malware, or deliberately crafted to be exploitable in other ways known to the creator?

      Even if I am prepared to devote my life to the skills and effort required to read and understand the source code of every patch before use, I can't do that fast enough to avoid being exploited while still unpatched. Remember, these defects are there because all those eyes that developed the software in the first place, missed them; the chances of me being able to spot such defects in patches as they arrive are not good.
      cquirke
    • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

      @roncemer open source doesn't help prevent bugs. As sooner who has had Linux servers for years, they need constant patches and updates otherwise they can be easily exploited. Opening up the source would just cause more problems.
      Jimster480
  • law of engineering...

    complexity <> security

    gary
    gdstark13
  • Scam time &amp; Microsoft is as pointless as ever...

    What a load of bull! Why is this even an article? Dismiss this as unimaginative toad talk from the company run by Monkeyboy...
    alfielee@...
    • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

      @alfielee@...
      They are waiting on your resume, in hopes of replacing him. Is yours ready??
      eargasm
      • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

        @windozefreak
        Mine is. I'm perfectly fine with chopping it up into small pieces and ending the desktop monopoly as we know it.

        ;)
        ahh so
    • RE: Microsoft applies for a patent for a verifying a 'safe' operating system

      @alfielee@... well you seem to be a trolled fanboi.
      Jimster480