The story behind Genode's TrustZone demo on the USB Armory Dec 08, 2015Our latest article provides a look behind the scenes of the development of Genode's support for the USB Armory platform. The USB Armory is a computer in the form of a USB stick. It normally runs Linux. But thanks to the ARM TrustZone capabilities of the device, it is possible to run Genode behind the back of Linux. This is useful for shielding sensitive information like cryptographic keys from Linux by exposing it to Genode only and thereby drastically reducing the attack surface. Even in the event Linux gets compromised, e.g., by a vulnerability in the USB stack, the secrets remain protected. The article "The story behind Genode's TrustZone demo on the USB Armory" presents the adventurous story behind enabling this scenario. The biggest challenge was splitting the hardware platform into two worlds while maintaining the full functionality of Linux. The article goes on to explain the interplay between the secure world (Genode) and the normal world (Linux). Furthermore, it provides all the pointers needed to reproduce the scenario. Read the article... Genode OS Framework release 15.11 Nov 30, 2015The primary focus of version 15.11 is the use of Genode as a desktop OS. It vastly improves the GUI and audio stacks, features the port of Intel KMS from Linux, extends the support for the USB Armory and Xilinx Zynq-7000, and introduces new file-system infrastructure such as a VFS server. Whereas the previous release marked the point where the very first user adopted Genode as day-to-day OS, we maintained the direction to create a Genode-based desktop OS. Most improvements of the new version are related to this goal: The GUI and audio stacks have become much more modular, dynamic, and flexible. With a new copy-and-paste mechanism, we added a universally expected desktop-integration feature in a unique way that mitigates the misuse of the clipboard as a covert communication mechanism. Those higher-level features are complemented with profound low-level device-driver improvements, most noteworthy the addition of the Intel KMS driver. This driver allows us to drive multiple displays and switch screen resolutions on the fly. What high- and low-level components have in common, is the use of Genode's uniform configuration concept, which solves a variety of configuration problems with a single low-complexity mechanism. It allows us to modify all kinds of system configurations - ranging from the wireless driver to the style of window decoration - live by merely editing and saving text files. Even though the majority of improvements are attributed to the use of Genode as desktop OS, the release also covers other areas. Xilinx Zynq-7000 has been added to the supported platforms, TrustZone on the USB Armory received a lot of attention, and a new VFS server makes Genode's file-system infrastructure much more flexible. These and many more topics are covered in detail by the release documentation of version 15.11... Genode OS Framework release 15.08 Aug 31, 2015Version 15.08 marks the starting point of Genode used as day-to-day operating system, which underlines the maturity and scalability of the framework. A further highlight is the ability to execute Genode on top of the Muen separation kernel. Since the first release of Genode seven years ago, we dreamed of being able to use our OS technology as the underlying platform for our day-to-day computing needs. With the current version, the day has come: One of Genode's core developers has made the switch and others plan to follow soon. Hence, the use of Genode as day-to-day OS is the underlying theme of most improvements seen in the new version. It addresses long-standing deficiencies of the kernel-memory management of the NOVA kernel and Genode's custom kernel platform, extends the framework's system-monitoring and file-system abilities, and significantly improves the integration of VirtualBox with Genode. The second highlight of version 15.08 is the ability to execute Genode system scenarios on top of the Muen separation kernel. Compared to microkernels, Muen takes the ambition to reduce kernel complexity to an extreme. Written in the safe implementation language SPARK and with a code complexity of merely 5,000 lines, it lends itself to be high assuring about its correct behavior. From Genode's point of view, Muen represents an additional target architecture of the framework's custom base-hw kernel. The component isolation enforced by base-hw and the static isolation boundaries enforced by Muen represent two lines of defense for protecting security-critical system functions from untrusted components. More details about all the improvements are provided by the release documentation of version 15.08... Genode OS Framework release 15.05 May 26, 2015For the first time, a Genode release is accompanied by a book. Further highlights of the current release are vast improvements of our base-hw kernel, preliminary support for the seL4 microkernel, new device-driver infrastructure, and plenty of new device drivers. With version 15.05, we equip Genode users with comprehensive documentation in the form of the free book "Genode Foundations". The book covers the architecture in great detail, assists developers with the explanation of the development environment and system configuration, and provides insights behind the scenes of the framework. Furthermore, the book contains the specification of the framework's programming interfaces. Besides the documentation, the second highlight of the release is the base-hw kernel, which enables the execution of Genode without a 3rd-party microkernel. Our kernel, originally designed for the ARM architecture, has become able to run on the 64-bit x86 architecture, it received support for kernel-protected capabilities, and its scheduler got much more flexible. Even though we invest a lot of work in our custom kernel, the biggest strength of Genode is its ability to leverage the benefits of different kernels. With the current release, we introduce preliminary support to run simple system scenarios on top of the seL4 microkernel. With seL4, there is now the prospect of running Genode on top of a formally verified kernel. At the framework's architectural level, we took the opportunity to redesign the infrastructure for user-level device drivers. With this release, device drivers become subjected to rigid access control with respect to hardware resources. Along with this architectural change, there are massive improvements of the device driver support. There is a new AHCI driver, new audio drivers ported from OpenBSD, new SD-card drivers, added platform support for i.MX6, and support for message-signalled interrupts on x86-based machines. A detailed description of all the improvements is provided by the release documentation of version 15.05... Genode's core running on the seL4 kernel May 18, 2015In the third part of our seL4 article series, we describe the steps taken to run Genode's fundamental components on seL4. The article "Porting the core component" builds upon the experience gained from the first two articles to execute Genode-based systems on top of seL4. As for the previous articles, it is full of technical insights into both seL4 and Genode. Among the many challenges that had to be overcome are the management of capabilities and memory, the synchronous RPC communication between components, and the handling of page faults. As result, simple Genode system scenarios can be readily executed on top of the seL4 kernel. Read the article... All the steps described in the article can be followed in the topic branch https://github.com/nfeske/genode/commits/sel4 of the ongoing development. Furthermore, the principle support for seL4 will be featured in the upcoming Genode release 15.05. An in-depth look into the ARM virtualization extensions Mar 12, 2015Our new article explores the mechanisms of the ARM virtualization extensions and describes how Genode's custom base-hw kernel was turned into a microhypervisor. With the recently published version 15.02, Genode received support for ARM's virtualization extensions. While conducting this line of work during the year of 2014, we took the chance to thoroughly document the experience. The article "An in-depth look into the ARM virtualization extensions" presents the overall virtualization architecture and goes into detail about the virtualization of memory, CPU, interrupts, and time. Furthermore, it covers a series of experiments with I/O protection mechanisms. Read the article... Exercising the seL4 kernel interface Mar 10, 2015The second part of the article series about Genode on seL4 goes into detail about the kernel mechanisms for synchronous inter-process communication and the management of virtual memory. The article "Genode on seL4 - IPC and virtual memory" examines the most important mechanisms of the seL4 kernel. It covers synchronous inter-process communication between threads, the delegation of capabilities, and the management of virtual memory. Apart from presenting hands-on experience with using the kernel, it identifies potential challenges for using it as Genode base platform. Read the article... All the steps described in the article can be followed in the topic branch https://github.com/nfeske/genode/commits/sel4 of the ongoing development. Genode OS Framework release 15.02 Feb 27, 2015Version 15.02 extends the base-hw kernel with ARM-virtualization support, introduces a highly modularized tool kit for automated testing, adds support for the USB Armory platform, and improves the performance and stability of VirtualBox on Genode/NOVA. Most of the previous releases were motivated by our desire for features that we deemed as fundamentally important to use Genode as a general-purpose system. Now that we have reached most of the feature set that we longed after, the project adjusts its focus. According to our recently published roadmap, the underlying theme of the current development shifted towards the cultivation of the existing feature set rather than the introduction of new functionality. The current release perfectly reflects this change. It introduces a highly modular tool kit for scaling up the project's automated testing efforts and comes with stability and performance improvements all over the place. In particular, we are happy to report substantial performance gains of our version of VirtualBox running on NOVA. As a second focus of the version 15.02, our custom base-hw kernel platform received a lot of attention. The most prominent news is the added support for virtualization on ARM. This line of work has been conducted and refined over the time span of more than a year and took much of our prior experience with the NOVA virtualization architecture and ARM TrustZone into account. This experience resulted in a novel microhypervisor design with an extremely tiny foot print with respect to the added complexity on the account of virtualization support. In fact, less than 1000 lines of code had to be added to the root of the trusted computing base. Besides virtualization support, our kernel's scheduler got refined to take IPC relationships into account while additionally gaining support for the USB Armory hardware platform. These and many more improvements are covered in more detail by the release documentation of version 15.02... Road Map for 2015 Jan 14, 2015After brainstorming Genode's mid-term future on our mailing list, we finalized our road map for this year. The development during the past years was primarily driven by our desire for features. With respect to the feature set, we have eventually reached a state where Genode becomes viable as general-purpose computing platform. That said, we are still not there yet, because apart from a list of features, it is important how those features fit together and how easy it is to use them. Therefore, the focus for 2015 will be the consolidation and cultivation of the existing feature set. Still, there will be room for new developments, i.e., the use of Genode on the seL4 kernel. The new road map is available at https://genode.org/about/road-map. Genode at FOSDEM 2015 Jan 14, 2015With three talks, Genode will show a strong presence at this year's FOSDEM. The talks will cover an introduction of Genode, our line of work regarding VirtualBox on NOVA, and Genode's evolving GUI architecture. Keeping up with our tradition to participate in the worlds largest gathering of the open-source and free-software community, we are happy to announce three talks to be held by Norman Feske at FOSDEM 2015: Sunday 12:00 - 12:25 Genode - OS security by design Security devroom (AW1.120) Sunday 14:20 - 15:00 Transplantation of VirtualBox to the NOVA microhypervisor Virtualization devroom (UD2.120) Sunday 15:30 - 16:15 Introducing a radically componentized GUI architecture Microkernel devroom (K.3.201) More information about the talks (including abstracts) are available at the FOSDEM website. |
