Kinetic

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:

  1. Boots with Grub
  2. Has a PS/2 mouse and keyboard driver (written in Haskell)
  3. Has an SVGA driver for VMWare (written in Haskell with some bitmap handling done in C++)
  4. 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.)

Kinetic Operating System 2007-03-13

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.

Leave a comment

12 Comments

  1. she

     /  5 August, 2007

    Nice, 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 ;)

  2. guest

     /  2 September, 2007

    Have 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

  3. From 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 :)

  4. Eli

     /  4 September, 2007

    It 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.

  5. mgsloan

     /  4 September, 2007

    Even 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.

  6. harb

     /  4 September, 2007

    Have you seen House? Its another OS written in haskell:
    http://programatica.cs.pdx.edu/House/

  7. guest

     /  4 September, 2007

    Hi,

    it would be most interesting to see the code, is it avaiable anywhere?

  8. guest

     /  4 September, 2007

    i 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?

  9. Aly

     /  7 September, 2008

    Wow, I didn’t understand much of what was going on, but it sounds like an awesome project!
    I like the transparent mouse :-)

  10. Leo

     /  19 February, 2014

    Where 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.

  1. Announcing Potential: x86-64 assembler as a Haskell EDSL « Integer Overflow
  2. Is There Any Operating System Built On Haskell or Lisp? « umurgedik

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: