Archive

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.

Review of the Ubuntu-powered Meizu Pro 5

Canonical has been talking about making Ubuntu on tablets and phones a reality now for several years, and in recent months we have finally seen a few devices come on the market. A review of the Meizu Pro 5, a Ubuntu-powered smart phone that is compatible with North American 4G networks, appeared on DistroWatch.The article covers how Ubuntu compares to Android and explores the differences between traditional apps vs Ubuntu scopes:

Scopes are a slightly unusual concept in the smart phone market, but I grew to appreciate the idea. What eventually gave me the "a-ha" moment when it came to scopes was when I realised scopes are for looking at information and apps for doing things. Scopes are always on, always waiting in the background to provide us with small bits of data. Applications are for performing tasks. A scope will tell me what is on my calendar for the day, an application will create new appointments. A scope will tell me who called me recently while an app will place a new call.

GPLGPU walkthrough

The goal was to publish source code to a GPU that is register compatible with the late 90's era Number Nine "Ticket To Ride IV" GPU. Although the project didn't meet its funding goal, the person behind it later published the code on github.

Despite the fact that this is an older design, it has lots of stuff that is worth studying. It's interesting to compare this design to the VideoCore GPU that I walked through in a previous post. While there are some fundamental differences, there are surprising number of functions that are similar, which shows how modern GPUs evolved from earlier ones.

A walkthrough of the GPLGPU as well as some history and backstory of the Number Nine "Ticket To Ride IV" GPU.

“Can someone explain the origin of the OS/2 table’s name?”

In a discussion at TypeDrawers, Greg Hitchcock (from Microsoft) shares a bit of the history regarding OS/2 table's name in the TTF font format:

Because the design of fonts between OS/2 and Windows was very similar (the same folks at Microsoft did most of the graphics for both OS/2 and Windows - with some input from IBM based on their FOCA values) we decided to consolidate the OS/2 and WIN tables into just one table - OS/2. This is why the spec says "...a set of metrics that are required by OS/2 and Windows." The parting with IBM occurred later in 1990. Microsoft had already made enough fonts using the OS/2 table that we decided it would be too expensive to rename the table to the WIN table.

Ultimately the OS/2 table has become somewhat of a catch-all for additional bits of data, which is why we are now on the 6th version of the table.

Oracle’s lawyer publishes op-ed on lost case

After Oracle's expected and well-deserved loss versus Google, Oracle's attorney Annette Hurst published an op-ed about the potential impact of the case on the legal landscape of the software development industry. The op-ed focuses on one particular aspect of Google's position, which author puts as following:

ecause the Java APIs have been open, any use of them was justified and all licensing restrictions should be disregarded. In other words, if you offer your software on an open and free basis, any use is fair use.

This position, as she claims, puts GPL in jeopardy: common dual-licensing schemes (GPL+proprietary license) depends on developers' ability to enforce the terms of GPL.

It is pretty obvious that the danger of this case for the GPL and the open source community is heavily overstated - the amount of attention this case have received is due to the fact that the developer community never really considered header files as copyrightable assets. The whole "GPL in jeopardy" claim, as well as a passage saying that "o copyright expert would have ever predicted would be considered fair", is merely an attempt to deceive readers.

The interesting bit is why Oracle's lawyer tries to pose her client's attempt at squeezing some coins from Google as an act of defending the free software community. Does Oracle still think the open source proponents may regard it as an ally, even after Sun's acquisition and the damage it dealt to OpenSolaris, OpenOffice and MySQL projects?

Linux 4.6 released

Linux 4.6 has been released. This release adds support for USB 3.1 SuperSpeedPlus (10 Gbps), the new distributed file system OrangeFS, a more reliable out-of-memory handling, support for Intel memory protection keys, a facility to make easier and faster implementations of application layer protocols, support for 802.1AE MAC-level encryption (MACsec), support for the version V of the BATMAN protocol, a OCFS2 online inode checker, support for cgroup namespaces, and support for the pNFS SCSI layout, and many other improvements and new drivers. Here is the full list of changes.

VMS Software releases OpenVMS 8.4-2

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

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.

Interview with Ray Tomlinson on Creeper/Reaper

It's been several weeks since Ray Tomlinson, best known for the invention of email, passed on. Email, however, represents only a very small portion of his work and contributions.

While writing a research paper on possible new methods to reduce and eradicate malware, I came across a bit of intriguing history whose available details did not satisfy my curiosity, and I needed to know more than what the internet had to offer. The event in question was the creation of Creeper, a piece of software created in 1971 by Bob Thomas that, according to most sources, is the world's first computer virus. There hasn't been a lot of information available on the internet regarding Creeper except that it was created to "infect" computers running the TENEX operating system on ARPAnet. It would cause the machine to print "I'M THE CREEPER. CATCH ME IF YOU CAN." Then Ray Tomlinson created Reaper whose sole purpose was to seek out and remove Creeper from the machines it had "infected".

I wanted to know more, though. Why was Creeper created in the first place? Did it cause problems? Was it an annoyance to those managing the machines it affected? Should it really be considered the first virus (technically worm, if that)? In late 2014 I ended up finding Ray Tomlinson on LinkedIn of all places and asked him if I could ask a few questions about Creeper and Reaper. He very kindly obliged.

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.

Linux 4.5 released

Linux 4.5 has been released. This release adds a new copy_file_range() system call that allows to make copies of files without transferring data through userspace; experimental Powerplay power management for modern Radeon GPUs; scalability improvements in the Btrfs free space handling; support GCC's Undefined Behavior Sanitizer (-fsanitize=undefined); Forwarded Error Correction support in the device-mapper's verity target; support for the MADV_FREE flag in madvise(); the new cgroup unified hierarchy is considered stable; scalability improvements for SO_REUSEPORT UDP sockets; scalability improvements for epoll, and better memory accounting of sockets in the memory controller. There are also new drivers and many other small improvements.

There are also new drivers and many other small improvements. Here is the full list of changes.

Microsoft pushes ads for Windows 10 in a security update

Security update package MS16-023 for Internet Explorer doesn't only contain security patches, but also a few other things, including: "This update adds functionality to Internet Explorer 11 on some computers that lets users learn about Windows 10 or start an upgrade to Windows 10."

Ghacks.net writes:

Microsoft does not reveal what this means, or what this has to do with Internet Explorer. According to Woody Leonhard over at Infoworld, the update pushes a banner on Internet Explorer 11's New Tab Page advertising the company's new operating system Windows 10.

Unfortunately the ads can't be uninstalled without uninstalling the whole security update package.

Ray Tomlinson, Technological Pioneer, Dies at 74

The sad news promulgated several days ago that Ray Tomlinson passed away on Saturday, March 5th. Most known for his invention of email, Ray also contributed heavily to ARPANET, TENEX, and many other projects. He was one of the many great pioneers in the early days of digital computing technology who helped shape the world as we know it today. While much of his work and many of his contributions have already passed into obscurity due to the ever expanding, glamorous universe of modern technology, his memory still stands as a testament to what the people in our industry are capable of accomplishing even without any precedents.

So long, Ray, and thanks for all the email.

One of the stark realities that becomes more clear from Ray's passing is that many of the technological frontiersmen from the 60s and 70s are closer to the end of their lives than they are to their prime. Another decade or so, and the generation that largely laid the foundation upon which western society in many aspects currently rests will no longer be with us.

Genode 16.02 supports the RISC-V CPU architecture

With version 16.02, the Genode OS Framework moves beyond x86 and ARM CPUs and embraces the emerging open-source RISC-V hardware architecture. Furthermore, the release comes with the new ability to securely assign USB devices to virtual machines, and updates the Muen separation kernel and the seL4 microkernel.

Today's x86 and ARM-based commodity platforms have become increasingly opaque and infested with proprietary firmware. With new platforms becoming ever more complex and being equipped with mandatory companion processors like Intel's Management Engine, the trustworthiness of mainstream hardware becomes more and more uncertain. If those parts of the system become compromised, even a perfectly secure OS cannot protect the user's privacy and security. It goes without saying that this development is a strong concern of privacy advocates. The article Intel x86 considered harmful by Joanna Rutkowska substantiates those concerns extremely well.

RISC-V is a possible answer to the call for trustworthy hardware. In contrast to the CPUs of current-generation hardware, RISC-V is an open-source CPU architecture. The idea of open-source CPUs is not new. There exist numerous softcore CPUs like LatticeMico32 or OpenRISC. But in contrast to those projects, which are primarily targeted at FPGA platforms, RISC-V is designed to scale from deeply embedded systems to 64-bit general-purpose platforms. The prospect of a scalable and trustworthy hardware architecture motivated the Genode project to take a closer look. In the just-released version 16.02, RISC-V has been added as a supported architecture to Genode's custom base-hw kernel. Since the hardware is still in flux, the scope of the support is still somewhat limited. But Genode is already able to run on the official Spike simulator as well as on RISC-V as a synthesized FPGA softcore.

Besides the added RISC-V support, the second highlight of the current release is the new ability to securely assign USB devices to VirtualBox instances running on top of the NOVA kernel. With this feature, Genode becomes able to accommodate many typical desktop-OS work flows like transferring data via USB sticks, or obtaining pictures from a digital camera. Under the hood, the implementation is quite interesting as it successfully transplants the xHCI device model of Qemu to VirtualBox.

The third focus of version 16.02 is the update of the Muen and seL4 kernels. The Muen separation kernel has been updated to version 0.7, which greatly improves the interoperability with Genode's tooling. In fact, Muen can now be targeted with the same work flows as employed for all the other kernels. Genode's support for the seL4 kernel is still a rather experimental line of work. In this respect, the update to the kernel version 2.1 posed a number of interesting challenges with respect to the kernel-resource management. This discussion along with details about the many more improvements of the current release is covered in the official release documentation.

Ubuntu may ship ZFS as a module… Or not?

Ubuntu's announcement about inclusion of ZFS support in upcoming 16.04 LTS started an important discussion in opensource community: the license incompatibility between GPL and CDDL licenses may be an issue. Being a copyleft license, GPL requires that all works that are derived from GPL-licensed work are also distributed under terms of GPL. CDDL, the license of ZFS code, is also a copyleft license, and as such requires CDDL-licensed work be distributed "only under the terms of ." Although Ubuntu's ZFS code comes from OpenZFS project, Oracle is still one of the major copyright holders of the code base, and it does not seem likely to relicense its assets under GPL any time soon.

Dustin Kirkland of Ubuntu, the author of the announcement, explained Canonical's position, albeit light on details:

The CDDL cannot apply to the Linux kernel because zfs.ko is a self-contained file system module -- the kernel itself is quite obviously not a derivative work of this new file system. And zfs.ko, as a self-contained file system module, is clearly not a derivative work of the Linux kernel but rather quite obviously a derivative work of OpenZFS and OpenSolaris. Equivalent exceptions have existed for many years, for various other stand alone, self-contained, non-GPL kernel modules.

Software Freedom Conservancy (SFC), a non-profit with self-assigned mission of carrying on a crusade against GPL violations, quickly pointed out that the "obvious" conclusions of Canonical are not really all that obvious:

f ZFS were statically linked with Linux and shipped as a single work, few would argue it was not a "work based on the Program" under GPLv2. And, if we believe there is no legal difference when we change that linking from static to dynamic, we conclude easily that binary distribution of ZFS plus Linux - even with ZFS in a .ko file - constitutes distribution of a combined work.

Another non-profit organization - Software Freedom Law Center (SFLC) - provides yet another opinion on the matter. Eben Moglen points out that CDDL permits distribution of binaries under other licenses, so in case of Linux module GPL's requirements in case of binary module may be fullfilled by distributing it under GPL. Admittedly, this does not solve the issue of the license incompatibility of the code bases. The proposed solution is basically to ignore the wording of GPL's viral clause:

In this specific sense, then, the conduct which falls outside the words of GPLv2 falls within the "equity of the license," or its "spirit." As all Western legal systems have known since Aristotle, literal interpretation of any legal material will sometimes produce unintended unjust results, which can and should be corrected by the invocation of "equity." This present issue is evidently an example in which the tension between literal and equitable interpretation is raised, and it is the consensus of the kernel copyright holders' intention which determines which mode of interpretation is to be employed.

The issue of GPL compatibility and kernel modules' licensing arised before. For example, Linus Torvalds already noted that kernel modules are in "gray area" when it comes to the issue of derived worked. Using an example of Andrew filesystem he stated that external code base that was designed on different system and only required minimal porting effort due to interface similarities, in his opinion, was not a derived work of Linux. Even more appropriate example is Nvidia's infamous proprietary Linux driver, which interfaces the kernel via specially-crafted module that abstracts away Linux kernel implementation details, so that Nvidia's binary blob may still considered to be a self-contained work targetting module's interface, not the interfaces of Linux. This driver is widely used and generally tolerated by distributions.

The differences in these two positions reveal the two conflicting opinions on Linux copyright situation. SFLC is more concerned about the ability of opensource ecosystem to survive in face of fanatic GPL enforcement: their statements goes into painful details about difficulties that projects with permissive licenses are facing when they need to maintain the ports of their code in GPLed projects. If stictly enforced, GPL could hinder such projects to the point when whole ecosystem comes to net loss. Such situation could be particularly painful in cases like this, when the goals of GPL are met, but the legal mechanism that was chosen by opensource Foundation prevents both Linux and OpenZFS from cross-polination.

But on the other hand, making such excuses would open gates for projects that don't really contribute to the opensource, but only use it to their own benefit. While proponents of permissive licenses (myself included) don't find anything wrong with such outcome, GPL was specifically designed to prevent it, and that is why it is one of the most popular opensource licenses out there. Obviously, every concession weakens the position of those seeking GPL enforcement, including SFC, whose mission right now is endangered by both SFLC's and Canonical's views on ZFS integration into Linux. Being a self-styled GPL crusader with several battles already fought, SFC knows that the ZFS inclusion in Ubuntu may come at a price of legal actions lost, and potentially tolanted hackers driven out of opensource by frustration and disappointment.

There is another interesting angle to this situation: by now it is common knowledge that Sun Microsystems specifically designed CDDL to be incompatible with GPL, so that ZFS, while being opensource, could not be included with Linux. Shipping ZFS with Ubuntu would defeat this tactics and potentially remove motivation for such unfortunate choice of license for companies like Sun or Oracle, to benefit of all involved sides.

And yet another thing to consider: some (most?) jurisdictions explicitly require sticking with literal meanings of laws and contracts. This means that even if SFLC's position is defendable in United States, it might be dismissed in other parts of the world, giving Linux copyright holders ability to sue Canonical over copyright infringement. Given that Oracle holds copyright in both Linux and OpenZFS, and that it already demonstrated willingness to take legal actions against opensource projects, Canonical might still be under significant risk.

At any rate, the outcome of this discussion, if any, have potential to settle a long-standing issue in opensource community, and to make legal implications of using GPL more transparent and clear.

Implementing Mutexes in the QNX Neutrino Realtime OS

A mutex is a common type of lock used to serialize concurrent access by multiple threads to shared resources. While support for POSIX mutexes in the QNX Neutrino Realtime OS dates back to the early days of the system, this area of the code has seen considerable changes in the last couple of years.

Debian 8.3 released

The Debian project is pleased to announce the third update of its stable distribution Debian 8 (codename jessie). This update mainly adds corrections for security problems to the stable release, along with a few adjustments for serious problems. Security advisories were published separately and are referenced where applicable.

Linux 4.4 released

Linux 4.4 has been released This release adds support for 3D support in virtual GPU driver, which allows 3D hardware-accelerated graphics in virtualization guests; loop device support for Direct I/O and Asynchronous I/O, which saves memory and increases performance; support for Open-channel SSDs, which are devices that share the responsibility of the Flash Translation Layer with the operating system; the TCP listener handling is completely lockless and allows for faster and more scalable TCP servers; journalled RAID5 in the MD layer which fixes the RAID write hole; eBPF programs can now be run by unprivileged users, and perf has added support for eBPF programs aswell; a new mlock2() syscall that allows users to request memory to be locked on page fault; and block polling support.

There are also new drivers and many other small improvements. Here is the full list of changes.

Review: Mint 17.3 may be the best Linux desktop distro yet

Linux Mint 17.3 is the final Mint 17 release and should put to rest any worries about Mint's plan to stick with Ubuntu LTS releases for its base. Mint has done what it set up to do, namely improve the Cinnamon desktop to the point that it not only matches, but in many places far exceeds the user experience found in other options like GNOME, and especially, Unity.

Indeed, it's hard to look at Mint 17.3 without comparing it to its upstream base. While Mint has been continually working hard on the desktop and cranking out release after release, Ubuntu has stagnated. If Ubuntu wants to leapfrog past some of its pain points, its developers would do well to look downstream. Mint's package management tools are simpler, more comprehensive, and easier to use than anything Ubuntu offers. Mint also manages to do all this without anything even remotely close to the resources Ubuntu enjoys.