There have been several attempts of using memory safe languages in systems programming contexts.
This article aims to provide a rough overview of all major systems that have been implemeted in such languages, either completly or with large safe components.
Either fully safe with automatic memory management or compiler enforced rules that prevent typical memory corruption errors, or more classical system languages that already supported better type enforcement rules that C17 still misses.
Before delving into each specific language group, I would also suggest looking at Safe and Secure Drivers in High-Level Languages session from the 35c3 conference, organized by Chaos Computer Club.
Initially developed in 1961, using an Algol 60 variant with support for system level programming, known as ESPOL, MCP was the very first documented OS written in an high level language, without any use of Assembly language.
They managed to achieve this, by having hardware support for strong typed languages, while offering all required CPU instructions as compiler intrisics on the ESPOL compiler.
Eventually the ESPOL language got replaced by an improved version named NEWP.
NEWP is probably the first systems programming language to have the concept of UNSAFE code blocks for low level code capable of compromising memory integrity if not written properly.
Burroughs MCP platform still lives to this day as Unisys Clearpath/MCP.
THE multiprogramming system
The OS known as THE was developed in 1968 at Technische Hogeschool Eindhoven, by the likes of Edsger Dijkstra and fellow researchers.
It used a modified version of Algol 60, which was the only programming language available for userspace applications.
Muen Separation Kernel
The Muen is the world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level.
It is written in a mix of Ada and its verified subset, SPARK.
COSMOS was a community driven OS implemented in C#.
Helios was a managed OS developed at Microsoft Research, for distributed computing, based on the work done for Singularity.
Midori was another attempt at Microsoft Research to build upon the outcome of Singularity, done a couple of years before.
Although the project was done in secrecy, after the project's demise, one of the project leads, Joe Duffy, has written several blog entries describing the whole OS stack.
It was based on yet another C# variant, called M# or System C#, depending on the sources referring to it.
According to Joe Duffy, some of the C# features that we now take for granted, like TPL, async/await, span types, reference returns, were initially designed as part of Midori.
In addition to the blog entries, Joe Duffy has also done a couple of presentations on the subject, namely:
- Safe Systems Programming in C# and .NET
- RustConf 2017 - Closing Keynote: Safe Systems Software and the Future of Computing
Besides the already mentioned features that ended up on the official .NET Framework and .NET Core, another relevant feature was Bartok's replacement on Windows 10, now called .NET Native.
Singularity was developed by Microsoft Research as their first attempt for an OS written on a type safe language.
The OS made use of an extended version of C# for systems programming, named Sing#, where all code all statically, with a GC per process.
Currently the source code is still available at the Codeplex archive.
On Singularity, MSIL gets compiled into a variant called MDIL (Machine Dependent Intermediate Language) via a compiler named Bartok.
Incidently, when Microsoft released Windows 8 with the WinRT runtime, the OS stack made use of a similar MDIL format and Bartok compiler, whose roots can be tracked down to the Singularity project.
- BUILD 2012, Deep Dive into the Kernel of .NET on Windows Phone 8
- Mani Ramaswamy and Peter Sollich: Inside Compiler in the Cloud and MDIL
lilith is an interesting OS, still work in progress, developed in the Ruby inspired strongly typed AOT compiled language, Crystal.
Not to be mixed with Modula-2's Lilith, as the author did not had it in mind when coming up with the name.
Just like most memory safe system programming languages, Crystal makes use of automatic memory management.
Currently a couple of patches are required to Crystal's compiler, as means to make the capable to build the OS, however those changes might eventually land in upstream.
Biscuit is a monolithic POSIX-style kernel, initially presented at 13th USENIX Symposium on Operating Systems Design and Implementation.
Embedded Go is a bare metal implementation of Go targeting ARM microcontrollers like the Cortex-M3, M4, M7 and so forth.
Currently only supports a subset of the available standard library.
Fucshia's Garnet Layer
The new research OS being developed by Google, makes use of Go in a few key areas, across the low level Garnet layer.
Namely the TCP/IP stack, disk management utilities and a couple of other components.
The original annoucement post was done at Go developer's mailing list.
gVisor is a user-space kernel, used to provide a container runtime sandbox, with Docker and Kubernetes integration,
being used in some Google Cloud configurations, as per their annoucement post.
There is a InfoQ talk about its implementation as well, gVisor: Building and Battle Testing a Userspace OS in Go.
GERT is a modified version of Go that runs bare-metal on armv7a SOCs, it was developed as part of his author's master thesis.
The TinyGo project aims to provide bare metal support to target small IoT devices with Go.
Currently it supports as deployment targets:
- ARM (Cortex-M)
- AVR (Arduino Uno)
As of 2019 it has gotten official Google sponsorship.
TamaGo is a bare metal implementatio of Go for ARM SoCs, developed by F-Secure.
It was demoed at the 2019 edition of Computer Chaos Club (CCC), '36c3', at the talk TamaGo - bare metal Go framework for ARM SoCs..
Unik is a Go module for running Go programs as unikernels, without an underlying operating system.
Its main demo application is a functional Gio GUI program that demonstrates the virtio GPU and tablet drivers.
A tiny Arduino like system that can be programmed in uLisp, a Lisp variant for microcontrollers.
It supports all common Arduino shields, and has even some plotting functionality.
Cedar Programming Environment
The Cedar system developed at Xerox PARC was an evolution of the Xerox Development Environment (XDE) developed in the Mesa programming language for the Xerox Alto, which is why its implementation language got named as Mesa/Cedar.
The environment provided a similar experience to the Interlisp-D and Smalltalk systems in use at Xerox PARC, but with a strong typed language instead.
Cedar was deployed in production on the Xerox Star workstations and Pilot operating system.
Acorn Computers Ltd tried to create an OS based on a mix of C and Modula-2+, ARX, but failed to do so due to external factors.
Topaz was a distributed operating system for the DEC SRC Firefly multiprocessor, written in Modula-2+, which was kind of an evolution of Mesa/Cedar, as many of the designers worked on both languages.
Some information can be found on the The Topaz System: Distributed Multiprocessor Personal Computing and Experience with Garbage Collection for Modula-2 + in the Topaz Environment papers.
The SPIN OS was a microkernel based OS developed at University of Washington, including a POSIX layer compatible with DIGITAL UNIX.
It made use of the Modula-3 programming language, the sucessor to Modula-2+'s design, and was the best use case of the language before DEC got acquired by Compaq, followed up by HP, which kind of killed anything related to Modula-3.
Oberon was a simple workstation like OS, designed by Niklaus Wirth and Jürg Gutknecht, after Niklaus Wirth 2nd visit at Xerox PARC and experience with the Mesa/Cedar system.
A book was written describing the whole process, Project Oberon: The Design of an Operating System and Compiler, later a free version was made available as downloable PDF.
Several years later, Niklaus Wirth decided to revisit the project, and created a new version targeted at an FPGA based board instead of the original hardware. So a new book revision was made available, alongside the source code.
An Oberon fan later created a project page, and actual hardware, the OberonStation, sadly with very limited amount of units being made available.
The Wikipedia article provides a nice overview of all Oberon versions that existed.
A2, AOS, Bluebottle OS
A2 was written in an evolution of Oberon, named Active Oberon, and it represents the last iteration of Oberon based platforms as far as workstation workflows go.
The OS improvements were better support for concurrency, language level support for untraced references and inline Assembly.
Support for colour graphics, video, audio were also greatly improved.
MirageOS is an Unikernel, with some of tooling being part of Xen hypervisor.
Additionally its TCP/IP stack is used on Docker on the macOS platform, and there is a bare metal implementation targeted at the ESP32 embedded chip.
HalVM is an unikernel developed by the company Galois, for deployment in high security scenarions for their customers.
Around 2016 they have started working on the third version.
House is an OS written mainly in Haskell, with some extensions for low level access.
Although Android makes use of the Linux kernel and large sets of C++ code, the userspace is mostly Java based with severe limitations to native code, hence why I am listing it as part of Java based OSes.
JNode was a community driven project to create a Java based operating system.
This work has been the base of a research thesis JIKESNODE, which combined the Jikes selfhosted Java compiler with the JNode source base.
JX was a Java based OS developed for research regarding secured networked operating systems.
In a similar vein to Android, MicroEJ VEE, combines Java with C and C++ core components.
It provides an alternative implementation for Java native methods called SNI, and the ability to compile to native code as deployment method, in case the users decide to run the platform directly on the target hardware, also known as bare metal deployment.
Additional information can be found on the specifications section.
Amazon AWS Lambda containers
In December 2018, Amazon announced a revamped infrastructure for AWS Lambda deployments.
It makes use of Firecracker, a microVM implemented in Rust.
Just like Go, Rust is finding some love among Fuchsia developers.
Currently it is being used for several Fuschia modules, as seen on the Garnet layer source control repository.
Initially designed as a monolitic kernel, it was rebooted as an microkernel operating system.
As one can see on the project page. it already provides a good set of features as a desktop OS, with some POSIX compatibility.
KataOS and Sparrow
On the 4th October 2022, Google announced that they were also working on a Rust based OS for secure embedded development.
It is microkernel based, using the famous seL4 as the foundation, with the remaining infrastructure written in Rust.
RusytHermit is a rewrite from a previous unikernel project developed at RWTH-Aachen, originally written in C, into Rust.
Besides Rust, the kernel is also capable to run C/C++/Go/Fortran applications.
Chrome OS makes use of Rust on its Chrome OS Virtual Machine Monitor layer.
There is a Google IO 2019 talk, where the team goes into depth how it interoperates with gVisor, as means to run Linux code on a sandbox secured enviroment.