The short version
Kinetic is an operating system (x86) I started working on around January 2007. It’s written in a combination of Assembly, C++, and Haskell (compiled with GHC). It’s the current manifestation of a long-time interest I’ve had in OS-level development.
The long version
After learning Haskell, I became fascinated by the idea of using monads to express security-related ideas in software. The idea is pretty simple: one can think of the IO monad as a type system contaminate that identifies all functions that interact with the program’s environment (such as those that print to the console, write to the network, etc). This is useful: a function cannot mutate the environment unless it has IO type. Contrast this with most languages (C++, Java, Scheme, Python, etc) where you need to examine a function’s implementation to be sure that it doesn’t mess with the environment.
So here was my thinking: if the operating system executed Haskell code directly, it could use the type checker to make conservative estimates about the program’s behavior. In particular, if we broke up the IO monad into several smaller parts — such as a Console monad, a Network monad, etc — then a program’s type would reveal it’s intentions. Policies could be set based on the type system. Wouldn’t that be neat?
For the most up to date, check the Kinetic category on my blog.
So that was the idea. In practice, I’m not there yet. Kinetic is something that I work on when I have time, and time tends to come in unexpected bundles when you’re a student.
Here’s where we’re at:
- Boots with Grub
- Has a PS/2 mouse and keyboard driver (written in Haskell)
- Has an SVGA driver for VMWare (written in Haskell with some bitmap handling done in C++)
- Has the beginnings of a GUI (written in Haskell), complete with font rendering (provided by FreeType)
What it looks like
Everyone likes screenshots, so here’s one of the GUI (notice the transparent mouse. Yup, I like to goof off.)
The next big thing to work on is getting Kinetic ready to run external binaries. I have a simple model in mind for this: programs are installed as source code, which is compiled at install-time. This gives Kinetic a chance to run the type checker on the program, which is the whole darn point of the thing. Once compiled, the host associates the program with its type signature, which allows runtime policies to be made that govern execution.
Since Kinetic is based on GHC, and GHC is able to bundle itself with the things it compiles, this should all be doable.