OS News Archive

Jehanne: a Plan 9-based operating system

Jehanne is a new distributed operating system designed for programmers. The core values that lead the development are simplicity and security. Jehanne is a fork of Harvey (which in turn is a fork of Plan 9 from Bell Labs merged with Nix's kernel sources) but diverges from the design and conventions of its ancestors whenever they are at odds with its goals. Read about development progress made in 2016.

Rux: a hobbyist microkernel written in Rust

Rux's goal is to become a safe general-purpose microkernel. It tries to take advantage of Rust's memory model - ownership and lifetime. While the kernel will be small, unsafe code should be kept minimal. This makes updating functionalities of the kernel hassle-free.

Rux uses a design that is similar to seL4. While there won't be formal verification in the short term, it tries to address some design issues of seL4, for example, capability allocation.

The code is very approachable for anyone interested in capability-based microkernel design.

Alexa: Amazon’s operating system

In short, Amazon is building the operating system of the home - its name is Alexa - and it has all of the qualities of an operating system you might expect:

  • All kinds of hardware manufacturers are lining up to build Alexa-enabled devices, and will inevitably compete with each other to improve quality and lower prices.
  • Even more devices and appliances are plugging into Alexa's easy-to-use and flexible framework, creating the conditions for a moat: appliances are a lot more expensive than software, and much longer lasting, which means everyone who buys something that works with Alexa is much less likely to switch.

It's definitely an interesting case to make - and Ben Thomspon does it well - but I still have a very, very hard time seeing voice-driven interfaces as anything but a gimmick at this point in time. Every point I made about this subject in the Summer of 2016 still stands today - limited functionality, terrible speech recognition, inability to deal with dialects and accents, and the complete and utter lack of support for people who live multilingual lives.

I can't hammer this last point home often enough: not a single one of the voice-driven interfaces we have today - Alexa, Siri, Google Now, Google Assistant, Cortana, whatever - support multilingual use. Some of them may allow you to go deep into a menu structure to change input language (while some, like smartwatches, even require a full wipe and reset), but that's not a solution to the problem of switching language sometimes even several times a minute, something multilingual people have to do dozens of times every day. And again - there are literally hundreds of millions of people who lead multilingual lives.

Heck, Alexa is only available in English and German!

If voice-driven interfaces are really as important as people make them out to be, they've got at least a decade of development ahead of them before they become actually useful and usable for the vast majority of the world.

Rust-based Redox OS 0.0.6 Released

Redox OS, a microkernel OS written in Rust, hast just released version 0.0.6, which includes bug fixes and and update to Rust.

From the project's 2016 in review post:

Today, we have a pretty mature project. It contains many core, usable components. It is already usable, but it is still not mature yet to be used as a replacement for Linux (like BSD is), but we’re slowly getting there.

The kernel was rewritten, a memory allocator was added, rendering libc out of the dependency chain, several applications were added, a file system were added, a window manager and display server was implemented, and so on.

Two old stories, more relevant today than ever

Me, almost seven years ago (2010), about the dearth of news about alternative operating systems:

OSNews has moved on. As much as it saddens me to see the technology world settling on Macwinilux (don't flatter yourself, those three are pretty much the same), it's a fact I have to deal with. It's my job to fill OSNews with lots of interesting news to discuss, and even though I would love to be able to talk about how new and exciting operating systems are going to take over the desktop world, I have to be realistic too. Geeks (meaning you and I) have made a very clear choice, and it doesn't seem like anything's about to bring back those exciting early days of OSNews.

Me, almost four years ago (2013), about why there are no mobile hobbyist operating systems:

So, what is the cause? I personally think it has to do with how we perceive our smartphones and tablets. They are much more personal, and I think we are less open to messing with them than we were to messing with our PCs a decade ago. Most of us have only one modern smartphone, and we use it every day, so we can't live with a hobbyist operating system where, say, 3G doesn't work or WiFi disconnects every five seconds due to undocumented stuff in the chip. Android ROMs may sound like an exception, but they really aren't; virtually all of them support your hardware fully.

With people unwilling to sacrifice their smartphone to play with alternative systems, it makes sense that fewer people are interested in developing these alternative systems. It is, perhaps, telling that Robert Szeleney, the programmer behind SkyOS, moved to developing mobile games. And that Wim Cools, the developer of TriangleOS, moved towards developing web applications for small businesses. Hard work that puts food on the table, sure, and as people get older priorities shift, but you would expect new people to step up to the plate and take over.

So far, this hasn't happened. All we can hope for is that the mobile revolution is still young, and that we should give it some more time for a new, younger generation of gifted programmers to go for that grand slam.

I sincerely hope so.

I don't know, for some mysterious reason I figured I'd link to these seven and four year old stories.

Harvey OS meets RISC-V

Ending this year, Ron G. Minnich has got Harvey running in RISC-V architecture, booting Harvey on Spike (ISA Simulator) and running rc shell on it. But he never rests and now is working on bringing it to QEMU and to FPGA. It's a big step for Harvey because we fixed some multiarch issues across the source and Ron found some bugs in timer interrupts in the hardware, so we all learned something.

What is Harvey OS?

Harvey is an effort to provide a modern, distributed, 64 bit operating system. A different environment for researching and finding new lines of work. It can be built with gcc and clang and has an ANSI/POSIX compliant subsystem.

Two news items about alternative operating systems in a row?

The year's off to a good start.

FreeDOS 1.2 released

The FreeDOS 1.2 release is an updated, more modern FreeDOS. You'll see that we changed many of the packages. Some packages were replaced, deprecated by newer and better packages. We also added other packages. And we expanded what we should include in the FreeDOS distribution. Where FreeDOS 1.0 and 1.1 where fairly spartan distributions with only "core" packages and software sets, the FreeDOS 1.2 distribution includes a rich set of additional packages. We even include games.

But the biggest change you are likely to notice in FreeDOS 1.2 is the updated installer. Jerome Shidel wrote an entirely new FreeDOS install program, and it looks great! We focused on keeping the new installer simple and easy to use. While many DOS users in 2016 are experienced DOS programmers and DOS power users, we often see many new users to FreeDOS, and I wanted to make the install process pleasant for them. The default mode for the installer is very straightforward, and you only have to answer a few questions to install FreeDOS on your system. There's also an "Advanced" mode where power users can tweak the install and customize the experience.

Great Christmas gift.

GNU Hurd 0.9, GNU Mach 1.8, GNU MIG 1.8 released

The GNU project has released GNU Hurd 0.9, GNU Mach 1.8, and GNU MIG 1.8. Hurd has been in development for a long time, and is supposed to - eventually - be the official kernel for the GNU operating system, a role currently unofficially filled by the Linux kernel. GNU Mach is a little bit different.

GNU Mach is the GNU distribution of the Mach microkernel, upon which a GNU Hurd system is based. The microkernel provides an Inter Process Communication (IPC) mechanism that the Hurd uses to define interfaces for implementing in a distributed multi-server fashion the services a traditional operating system kernel provides.

Genode 16.11 revisits low-level protocols

Following the feature-rich release in August, with the new version 16.11, Genode's developers took the chance to work on long-standing architectural topics, most prominently the low-level interplay between parent and child components. Besides this low-level work, the release features much improved virtual-networking capabilities. Originally introduced in the previous version, Genode's network-routing mechanism has become more versatile and easier to use. Further topics include the added support for smart cards, kernel improvements of the NOVA hypervisor, and a virtual file system for generating time-based passcodes.

The efficient interaction between user-level components is one of the most important aspects of microkernel-based systems like Genode. The design space for this interplay is huge and there is no widely accepted consensus about the "right" way. The options include message passing between independent threads, the migration of threads between address spaces, shared memory, and various flavours of asynchronous communication.

When the Genode project originally emerged from the L4 community, it was somehow preoccupied with the idea that synchronous IPC is the best way to go. After all, the sole reliance on unbuffered synchronous IPC was widely regarded as the key for L4's excellent performance. Over the years, however, the mindset of the Genode developers shifted away from this position. Whereas synchronous IPC was found to be a perfect match for some use cases, it needlessly complicated others. It turns out that any IPC mechanism is ultimately a trade-off between low latency, throughput, simplicity, and scalability. Finding a single sweet spot that fits well for all parts of an operating system seems futile. Given this realization and countless experiments, Genode's inter-component protocols were gradually shaped towards the combination of synchronous IPC where low-latency remote procedure calls are desired, asynchronous notifications, and shared memory. That said, Genode's most fundamental inter-component communication protocol - the interplay between parent and child components to establish communication sessions between clients and servers - remained unchanged since the very first version. The current release reconsiders the architectural decisions made in the early days and applies Genode's modern design principles to these low-level protocols. The release documentation contrasts the original design that was solely based on synchronous IPC with the new way. Even though the new version overcomes long-standing limitations of the original design, at the first glance, it gives the impression to be more complicated and expensive in terms of the number of context switches. Interestingly, however, the change has no measurable effect on the performance of even the most dynamic system scenarios. The apparent reason is that the parent-child interactions make up a minuscule part of the overall execution time in real-world scenarios.

Even though the architectural work mentioned above is fundamental to the Genode system as a whole, it is barely visible to users of the framework. With respect to user-visible changes, the most prominent improvement is the vastly improved infrastructure for virtual networking, which is covered in great detail in the release documentation. Further topics are the added support for using smart cards, a new VFS plugin for generating time-based passcodes, and updated versions of VirtualBox 4 and 5 running of top of NOVA. Speaking of NOVA, the release improves this kernel in several respects, in particular by adding support for asynchronous map operations. Each of the topics is covered in more depth in the release documentation.

New OS from Kaspersky Labs

Kaspersky Labs has developed its own operating system for switches and other networking devices.

First, it's based on microkernel architecture, which allows to assemble 'from blocks' different modifications of the operating system depending on a customer's specific requirements.

Second, there's its built-in security system, which controls the behavior of applications and the OS's modules. In order to hack this platform a cyber-baddie would need to break the digital signature, which - any time before the introduction of quantum computers - would be exorbitantly expensive.

Third, everything has been built from scratch. Anticipating your questions: not even the slightest smell of Linux. All the popular operating systems aren't designed with security in mind, so it's simpler and safer to start from the ground up and do everything correctly. Which is just what we did.

More details will follow soon, the company promises.

An extensible architecture for building certified concurrent kernels

Complete formal verification of a non-trivial concurrent OS kernel is widely considered a grand challenge. We present a novel compositional approach for building certified concurrent OS kernels. Concurrency allows interleaved execution of kernel/user modules across different layers of abstraction. Each such layer can have a different set of observable events. We insist on formally specifying these layers and their observable events, and then verifying each kernel module at its proper abstraction level. To support certified linking with other CPUs or threads, we prove a strong contextual refinement property for every kernel function, which states that the implementation of each such function will behave like its specification under any kernel/user context with any valid interleaving. We have successfully developed a practical concurrent OS kernel and verified its (contextual) functional correctness in Coq. Our certified kernel is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. To our knowledge, this is the first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking.

Some light reading for your late Tuesday afternoon.

Minoca OS goes open source

Minoca OS, which we talked about this past May, has gone open source.

Today we're thrilled to announce that Minoca OS has gone open source. We are releasing the entirety of the Minoca OS source code under the GNU GPLv3. We're excited to build a community of users and developers around this new operating system, and we need help. You can check out the source at https://github.com/minoca/os.

Here's a refresher on what Minoca OS is:

Minoca OS is a general purpose operating system written completely from the ground up. It's intended for devices looking to conserve power, memory, and storage. It aims to be lean, maintainable, modular, and compatible with existing software.

A complete rewrite of the Redox kernel

Redox, a Unix-like operating system written in Rust, recently rewrote its kernel:

Since August 13, the kernel is going through a complete rewrite, which makes the kernel space ultra-small (about the size of L4). Everything which can run outside the kernel in practice, will do so.

It is almost complete and will likely be merged in the coming week.

The reasons cited for the rewrite include memory management, concurrent design, SMP support, and 64-bit by default.

MenuetOS 1.23.60 released

Recent additions to MenuetOS include SMP support for up to 32 processors, support for 32GB RAM, support for time-critical, non-preempting processes, additions to window transparency, improved USB webcam and storage support, context-mixing compressor, WebCall (IP to IP with audio and video), streaming audio (internet radio) and video support - all written 100% in 64bit x86 assembly.

Genode 16.08 brings interactive and dynamic workloads to seL4

With the just released version 16.08, Genode makes the entirety of the framework's drivers, protocol stacks, and libraries available on the seL4 kernel. Thereby, the vision of a real general-purpose OS built upon a formally verified kernel suddenly becomes a tangible mission. Further highlights of the new version are the use of the framework to run VirtualBox 4 on the Muen separation kernel, an experimental version of VirtualBox 5 on top of the NOVA kernel, the added support for virtual networking and TOR, profound Zynq board support, and new tools for statistical profiling.

The seL4 kernel is universally regarded as the world's most advanced open-source microkernel - not by technical merits alone but by the fact that the kernel is accompanied by formal proofs of its correctness. However, to achieve this high level of assurance, the kernel's responsibilities had to be reduced to an extreme that goes even beyond traditional microkernels. In particular, the kernel leaves the problem of managing kernel memory to be solved at the user level. The problem still exists but it isn't considered the kernel's problem anymore. Consequently, this kernel design makes the creation of a scalable user land extremely challenging. For this reason, most use cases of seL4 remain solely static in nature, or combine static components with virtualization. The real potential of seL4 to scale towards dynamic systems remained untapped so far. Here is where Genode comes into play. Genode is designed as a dynamic user land for microkernels, which addresses the management of memory at the user-level via a unique resource-trading concept. It turns out that this concept is a suitable answer to the kernel-management problem posed by seL4. By completing the implementation of the framework's base mechanisms for this kernel, literally hundreds of existing Genode components become readily available to the seL4 community.

The Muen separation kernel is another take on the use of formal methods for assuring the absence of bugs in an OS kernel. In contrast to seL4, Muen applies different technologies (Ada/SPARK) and addresses static partitioned systems. A natural use case is the co-hosting of virtual machines. In a multi-level scenario, each virtual machine hosts a guest OS for editing documents at one security level. The separation kernel enforces the information-flow policy between the virtual machines. In such scenarios, the predominant guest OS is MS Windows. Consequently, Muen had to support the virtualization of such commodity OSes. Genode already solved this problem for another microkernel by making VirtualBox available on top of NOVA. So the idea was born to leverage Genode's version of VirtualBox on top of Muen - essentially using Genode as a runtime environment for VirtualBox. As crazy as it sounds - it works! The release documentation has a dedicated section that tells the full story. Speaking of VirtualBox, the ability to run VirtualBox directly on a microkernel is certainly a key feature of Genode. With Genode 16.08, a first version of VirtualBox 5 becomes available on the NOVA kernel.

The anecdotes above highlight the benefits of Genode's cross-kernel portability. The new version pushes this idea even further by attaining binary compatibility across all the supported kernels for a given CPU architecture. In fact, compiled once, an ELF binary of a regular component can be natively executed on kernels as different as seL4 and Linux as long as the component does not rely on a special feature of a particular kernel.

At a higher level, the current release extends the framework's library of ready-to-use building blocks in several areas. Most prominently, there are new network-related components for routing traffic, using TOR, and for distributing Genode over the network. Other added components are concerned with improving the use of Genode as a general-purpose OS, or to aid the optimization of components by the means of statistical profiling. Version 16.08 is further complemented with added board support for devices based on Xilinx Zynq, including drivers for GPIO, video DMA, SD cards, and I2C.

These and many more topics are covered in detail by the release documentation of version 16.08.