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?
Status
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)
Pretty modest.
What it looks like
Everyone likes screenshots, so here’s one of the GUI (notice the transparent mouse. Yup, I like to goof off.)
What’s next
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.
Integer Overflow 
she
/ 5 August, 2007Nice, hope some people can get interested once there is less time available – the monad type reminds me of logically grouping system stuff and similar components on a computer ;)
guest
/ 2 September, 2007Have you thought of use Xmod for the window manger?
It uses X11 function calls, but it could reduce the amount
of work needed to be done for a good GUI
intoverflow
/ 2 September, 2007From time to time I have considered the implications of working X11 into Kinetic. The biggest advantage is the wealth of graphics drivers that are available for the open source X11 implementations. The biggest disadvantage, however, is that X11 has many dependencies that would need to be resolved. It would be quite the task to support it.
I’ve recently been working on a console-based shell. I’m somewhat attracted to the idea of not having a GUI for the time being, simply because they require such a serious time investment.
Of course, if I were to use an X11-based window manager, I’d probably use xmonad :)
Eli
/ 4 September, 2007It certainly sounds like an interesting permutation of capability security. I’d like to see if you can invent some way to bend arbitrary x86 binary to use your type system.
Perhaps decompilation of x86 code into Haskell with appropriate monads? That would be a big project, but the ability to set program security parameters using a language type system could help immensely.
Kudos from a fellow OS geek.
mgsloan
/ 4 September, 2007Even if you don’t support X11, XMonad should be pretty easy to port over. Most of the code is non-X-specific.
Cool idea. Your current status specs sound quite like House, who borrowed lots of stuff from various sources, and credited them all. You might consider using some of their code, if you haven’t already.
harb
/ 4 September, 2007Have you seen House? Its another OS written in haskell:
http://programatica.cs.pdx.edu/House/
guest
/ 4 September, 2007Hi,
it would be most interesting to see the code, is it avaiable anywhere?
guest
/ 4 September, 2007i never said it was a good or bad idea to to attempt to port X11, but porting Xmonad to Kenetic would a good idea to do before creating your own GUI and create your own replacement for X11.
Xmonad is written in Haskell and the source is available. The source was also less than 500 lines for version 0.2 though it has grown.
How can people help you progress?
Aly
/ 7 September, 2008Wow, I didn’t understand much of what was going on, but it sounds like an awesome project!
I like the transparent mouse :-)
Leo
/ 19 February, 2014Where is the source code for this project? I was also wondering how you chose what kind of kernel to program. I have been very interested in the idea of an exokernel.