OS News Archive
Guest post by New OS from Kaspersky Labs
Submitted by 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.
MenuetOS 1.23.60 released
Guest post by 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.
Visopsys 0.8 released
Guest post by It's taken a while, but Visopsys 0.8 has been released. The GUI appearance has been updated, the infamous icons have all been replaced, and touch support has been added. There are a few new utilities, and in addition to all of the usual under-the-bonnet improvements, they've added OHCI (USB 1) support, completing the set of USB host controller drivers. There's a full changelog is and new screenshots.
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.
The Thor Operating System
Thor is an operating system created for learning purposes and for fun.
It is currently a 64bit OS written mainly in C++, with few lines of assembly when necessary.
There are lots of learning-oriented operating systems, and this is one of them. The more, the merrier.
Zuckerberg hopes to show off his Jarvis-like home AI next month
Facebook CEO Mark Zuckerberg is living at least a few years out ahead of anyone reading this post -- the founding executive told an audience in Rome (via Verge) today that he hopes to demonstrate his home’s artificial intelligence system, which controls things like air conditioning, lighting and more based on things like face and voice recognition.
The TechCrunch article is light on detail, but this project may be more interesting than it sounds at first blush. Zuckerberg isn't the first tech billionaire to sink a bunch of money into a fancy home automation project. Bill Gates famously did the same a couple of decades ago. High end homes all over the world have fancy and expensive home control systems, that provide their rich owners with frustration and hassle and absolutely confound houseguests. But these days, for a few hundred dollars, anyone can buy an Amazon Echo, any one of half a dozen automation hubs, and various switches, thermostats, and lightbulbs, and create a pretty nifty and convenient voice controlled home automation and entertainment system. Someone with the vision and the development budget that Mark Zuckerberg has at his disposal should be able, with readily available, inexpensive hardware, create something pretty amazing.
How (and why) FreeDOS keeps DOS alive
From a great interview with JImm Hall, founder of FreeDOS:
Hall said there are three key categories of people who use FreeDOS: People looking to run classic DOS games, businesses that need to support legacy applications and developers building embedded systems.
FreeDOS is a great project. DOS is still in use all over the place, and having it still actively developed means it'll be around for years to come.
PowerNex: kernel written in D
PowerNex is a kernel written in the D Programming Language. The goal is to have a whole OS written in D, where PowerNex powers the core.
Exactly what it is.
Genode 16.05 features revised API, Rust, and huge driver update
The Genode project has released the version 16.05 of the operating-system framework. The new version comes with a fundamentally reworked component API, basic support for the Rust programming language, new ACPI infrastructure, and upgraded device drivers for Intel wireless, Intel graphics, audio, and USB.
The Genode API and the programming styles for developing components evolved over the years. Being born out of the L4 community, the sole reliance on synchronous inter-component communication was deeply ingrained in the developer's mindset when the project was started ten years ago. It took the project a few years to overcome this misconception and embrace asynchronous communication primitives. Most modern Genode components use a mix of both synchronous and asynchronous inter-component interactions. At the API level, however, the two forms of communication remained to exist side by side instead of being integrated in one holistic design. With respect to programming styles, the project underwent a similar evolution. Coming from C-programming background, many parts of the original API resembled a C-ish programming style such as the prominent use of pointers, format strings, side effects via global function calls, or integer error codes. Over the years, however, the expressiveness of the C++ language got fully embraced and the programming style evolved towards functional programming.
Today, most modern Genode components are designed as single-threaded state machines, triggered only by signals and RPC requests originating from other components. There are almost no dynamic memory allocations. If so, allocations are not anonymous but accounted to a specific allocator. State is explicitly passed as arguments, not captured in the form of globally accessible objects. Thanks to this style, certain classes of bugs such as race conditions or memory leaks are greatly alleviated by design. Genode 16.05 cultivates the modern style of Genode components in the form of a fundamentally revised API. The new API is less complex, much safer, and easier to reason about. To account for this profound change, the release documentation is accompanied by a new edition of the "Genode Foundations" book (PDF).
The second major focus of the current release is the updated arsenal of device drivers. All drivers ported from Linux were upgraded to the Linux kernel 4.4.3. Specifically, the drivers are the Intel wireless stack, the Intel graphics driver, the USB driver, and the TCP/IP stack. Thereby, Genode users are able to leverage the same drivers as up-to-date Linux distributions but with each driver being encapsulated in a dedicated protection domain. The audio driver, which originates from OpenBSD, received an update to OpenBSD 5.9. The device drivers are complemented with new infrastructure that makes ACPI platform controlling and monitoring features available to Genode users.
Further highlights are the added ability to use the Rust programming language in Genode components and the enhanced support for using the GNU debugger on top of the NOVA microhypervisor. Details about all improvements and API changes are provided by the extensive release documentation of version 16.05.
Whither Plan 9? History and motivation
Plan 9 is a research operating system from Bell Labs. For several years it was my primary environment and I still use it regularly. Despite its conceptual and implementation simplicity, I've found that folks often don't immediately understand the system's fundamentals: hence this series of articles.
Bookmark this website, folks.
Minoca OS: operating system for connected devices
Minoca OS is a leading-edge, highly customizable, general purpose operating system. It features application level functionality such as virtual memory, networking, and POSIX compatibility, but at a significantly reduced image and memory footprint. Unique development, debugging, and real-time profiling tools make getting to the bottom of issues straightforward and easy. Direct support from the development team behind Minoca OS simplifies the process of creating OS images tailored to your application, saving on engineering resources and development time. Minoca OS is a one-stop shop for systems-level design.
Since this will be the main question: no, it is not open source (count the buzzwords). There's a free version that's free to use in non-commercial settings, and a pro version that isn't free, but does come with source access. So no, not open source - but not everything has to be. It's not like open source operating system folks are starved for entertainment in that department.
VMS Software releases OpenVMS 8.4-2
Guest post by As Mark Twain famously wrote, "...the reports of my death are greatly exaggerated". So with OpenVMS.
VMS Software, Inc. (VSI) today announced the worldwide availability of VSI OpenVMS Version 8.4-2 (Maynard Release) operating system for HPE Integrity servers. The Maynard Release is the second by VSI. The new OS is compatible with HPE Integrity servers running the latest Intel Itanium 9500 series processor, as well as most prior generations of the Itanium processor family. VSI also reconfirmed plans to offer OpenVMS on x86-based servers.
"This second release reaffirms our long-term commitment to the OpenVMS platform, and builds upon our highly successful first release of OpenVMS in June of 2015," said Duane P. Harris, CEO of VMS Software. "It is the first of many exciting improvements planned for OpenVMS, including future updates to the file system, TCP/IP, and other major improvements that we look forward to sharing with our customers as we work our way through the planned roadmap."
L4: lessons from 20 years of research and deployments
Guest post by NICTA, Australia's Information and Communications Technology Research Centre, has published a paper on the lessons learned by 20 years of work around the L4 microkernel.
Some of you may remember that NICTA has developped the seL4 microkernel, one of the first - if not the first - microkernel formally verified, an important stepstone in securing computing systems against whole classes of bugs and attacks.
The L4 microkernel has undergone 20 years of use and evolution. It has an active user and developer community, and there are commercial versions that are deployed on a large scale and in safety-critical systems. In this article we examine the lessons learnt in those 20 years about microkernel design and implementation. We revisit the L4 design papers, and examine the evolution of design and implementation from the original L4 to the latest generation of L4 kernels. We specifically look at seL4, which has pushed the L4 model furthest and was the first OS kernel to undergo a complete formal verification of its implementation as well as a sound analysis of worst-case execution times. We demonstrate that while much has changed, the fundamental principles of minimality, generality and high inter-process communication (IPC) performance remain the main drivers of design and implementation decisions.
Subgraph OS: open source OS that prioritizes security, anonymity
Subgraph, an open source security company based in Montreal, has published the alpha release of Subgraph OS, which is designed to with security, anonymity AND usability in mind.
"Subgraph OS was designed from the ground-up to reduce the risks in endpoint systems so that individuals and organizations around the world can communicate, share, and collaborate without fear of surveillance or interference by sophisticated adversaries through network borne attacks," its creators say.
Not the first time we've talked about it.
Sortix 1.0 released
I'm happy to announce the release of Sortix 1.0. This is the first self-hosting and installable release.
Sortix is a small self-hosting operating-system aiming to be a clean and modern POSIX implementation. It is a hobbyist operating system written from scratch with its own base system, including kernel and standard library, as well as ports of third party software.
We first reported on Sortix (version 0.9) a year ago.
How Genode came to the RISC-V CPU architecture
Submitted by As a follow-up to Genode's 16.02 release, the project just published an in-depth article describing the experience with the RISC-V architecture and the steps taken to enable Genode on this platform.
The article is targeted at enthusiasts interested in the practical use of RISC-V and can also be used as a guideline on how to bring Genode to a different CPU architecture.
Qubes OS 3.1 released
The major new architectural feature of this release has been the introduction of the Qubes Management infrastructure, which is based on the popular Salt management software.
In Qubes 3.1, this management stack makes it possible to conveniently control system-wide Qubes configuration using centralized, declarative statements. Declarative is the key word here: it makes creating advanced configurations significantly simpler. (The user or administrator needs only to specify what they want to get, rather than how they want to get it).