Microsoft is certainly exploring operating systems beyond Windows, and SafeOS can be added to the list that already contains Midori and Singularity.
But in all fairness, SafeOS is not designed as a moniker but rather it serves the purpose of describing the concept of a non-Windows safe operating system, whereas Midori and Singularity are codenames for projects already being explored by the software giant.
SafeOS is mentioned in a Microsoft patent application unearthed by MA-Config, which involves a secure operating system put together by using techniques such as typed assembly language (TAL) and Hoare logic for an Automated, Static Safety Verifier in order to deliver highly automated, static verification of both type and memory safety.
Essentially, the new Microsoft platform concept involves a completely different architecture of the operating system, going beyond address-based memory protection.
œSafeOS, or a similar operating system constructed using the “Automated, Static Safety Verifier”, includes a “Nucleus” that provides access to hardware and memory, a “kernel” that builds services on top of the Nucleus, and applications that run on top of the kernel, reads an excerpt from the patent.
œThe Nucleus, written in verified assembly language, implements allocation, garbage collection, multiple stacks, interrupt handling, and device access.
œThe kernel, written in C# (or other language) and compiled to TAL, builds higher-level services, such as preemptive threads, on top of the Nucleus.
œA TAL checker then verifies the safety of the kernel and applications. Finally, a Hoare-style verifier with an automated theorem prover verifies both the safety and correctness of the Nucleus.
In the patent, Microsoft is underlining the fact that SafeOS is nothing more than a concept designed to illustrate the principle of an Automated, Static Safety Verifier used to bulletproof a platform.
There is no guarantee that the Redmond company will explore this type of OS going forward, or that building a fully functional operating system with the SafeOS concept at the core is even possible.
œit should be understood that while feature rich safe operating systems can be constructed using the “Automated, Static Safety Verifier”, in its current implementation, SafeOS is a small safe operating system that has a number of programmatic limitations.
œFor example, it lacks support for many common C# features: exception handling, for example, is implemented by killing a thread entirely, rather than with try/catch.
œIt lacks the standard .NET class library, since the library’s implementation currently contains much unsafe code.
œIt lacks dynamic loading of code. Although it protects applications from each other using type safety, it lacks a more comprehensive isolation mechanism between applications, such as Java Isolates, C# AppDomains, or Singularity SIPs, it is added in the patent.
Written by: mariusoiaga ; published in Softpedia
