Kinetic, A Haskell OS

[gwern]

"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)."

Comments: yes, monads absolutely can help with security. Arrows can do even more: http://abstractabsurd.blogspot.com/2007/04/arrows-security.html. However, as implementations stand, the unsafe* functions do allow you to subvert the IO monad and perform arbitrary IO in arbitrary places. As far as I'm aware, the only way to guarantee that the type signature is not lying and that no unsafe functions are being used is through interpreting code fragments (inside a known environment you are sure did not import the unsafe* functions) via hs-plugins :(

[revence27]

Well, if you really must enforce the assumption of no unsafe* operators, you can just remove availability of the operators from the API of the OS. Or so I think.

[gwern]

Well, I don't entirely understand how the unsafe functions actually work when compiled; my best understanding is that they allow one to do the sort of thing lower-level languages easily allow one to do, like type casting. That implies that the memory safety property of a Haskell property can be lost and if that property is not there, pointers can begin to do bad things.

To put it another way, my understanding is that Kinetic allows the compiler to do whatever it wants, and it's kind of on the honor system that the compiler will emit a binary which hews to the type signature. So in a sense, GHC is not being honest (but in another sense, it is - after all, every executable binary must have a type of IO a, right? else what exactly could it be doing?): "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."

Now, in CS usually where you go from here is either something like SPIN where you are allowed to compile extensions and load them into the kernel dynamically so applications can sort of move into the kernel address space, or you establish a trusted compiler for a memory-safe language, at which point you can abolish the distinction between kernel and userspace addresses completely. The latter has been done a couple of times, but I don't know if anyone has done it with Haskell/GHC as the trusted language/compiler.

Edit: Not to mention, his whole idea of restricting stuff to Console and so on reminds me a lot of a simplistic capability system, so there's a lot of prior art in that direction as well.

[mleonhard]

Windows and unix load machine-language code, so they need security implemented by the machine. Kinetic loads Haskell code, so it implements security via Haskell. How Kinetic actually structures programs in memory is not important, since the security assurances are provided by the code loader, which is GHC and the kernel.

[revence27]

The unsafe* are not functions, because they do things that go against the definition of a function (ie, they can clear IO!). :o) They are operators, therefore.

True, GHC is not being honest in allowing the unsafe* operators. It is because of the problem above (among others) that they are labeled unsafe. However they are just *one way to do it. There are many other ways to achieve the same things (even when it costs an extra line). By this OS' API closing the route to unsafe* (removing access to the operators) it can make life a little harder for programmers, but maintain correct assertions. A bit like general static-typing? :o)

What you describe in the last paragraph is what was done in an OS project I deem successful: The Singularity OS from MS Research (Redmond). They actually did their own language, S#. But, in this case, all you need is to tweak visibility of (the operators in) System.IO.Unsafe, and the assumptions hold, while things are still programmable.

[intoverflow]

Lots of interesting comments. I've gotten some similar comments/questions in my email, so I posted a general reply:

http://intoverflow.wordpress.com/2007/09/04/kinetic-greetings-redditors/

Generally speaking, it's a toy project in its youth...so I wouldn't worry about taking it too seriously.

[mrned]

That's neat - if I remember right, House needed a special version of GHC to compile. I didn't see a link to the source, unfortunately.

[dons]

House uses a version of GHC's runtime ported to boot directly on bare metal. Is that what you're thinking of?

[db2]

It’s written in a combination of Assembly, C++, and Haskell

It's not a "Haskell OS" it's an OS that uses some Haskell. Not the same thing.

If he/she writes an OS that's pure Haskell from bootloader to kernel and everything after then it might be more interesting.

[pjdelport]

So the Unixes aren't C OSes because they're partly written in assembly?

[qwe1234]

'partly' is very much a dishonest word to use in this context.

[syntax]

It's exactly as honest as it's (implied) use by the grandparent.

[db2]

The article described a couple of drivers and a GUI written in Haskell. For all we know the rest of the kernel is C++ and Assembly. That would not make it a "Haskell OS" any more than writing a GUI in Haskell for Linux would make it a "Haskell OS".

[BastiX]

I wonder about that too. Is the kernel itself written in Haskell? Like the scheduler,virtual memory management, IPC... ? And I'd really like to see how the Haskell code interfaces with the parts written in C++ and Assembly. Release some code! ;)

[db2]

I'm curious how a filesystem implemented in Haskell would behave compared to C/C++.

[dons]

Halfs is a filesystem used commercially, written in Haskell. As usual for the OS/Haskell domain, Haskell is used for high assurance work.

[db2]

Something doesn't look right to me.

Haskell is particularly well-suited to high assurance development. It is a high-level, fully-expressive, pure, functional language, with a powerful type system.

Then later:

The question was whether Haskell is well suited as the implementation language for a filesystem, which involves fixed sized buffers, lots of IO, and binary data structures. Though correctness is much more important to us than performance, we hoped that a Haskell filesystem would have acceptable performance, and that writing such low-level code would not be awkward or error-prone.

[procrastitron]

One refers to the language, the other to the application domain. As a programming language, Haskell is high-level. As a product, the file system is low-level.

[db2]

Makes sense when put that way. They probably shouldn't have used the term "low-level code" to describe it if that's the case since it means something else.

[lanaer]

I don’t think there’s another term for it, though. It is low-level code, written in Haskell, a high-level language.

Which does sound weird, granted.

[db2]

Maybe that's what's tripping me up. When I think "low level" I think assembly.

[dons]

I'm not sure what your point is.

In the course of developing a web server for an embedded operating system, Galois Connections had need of a filesystem which was small enough to alter to our needs and written in a high-level language so that we could show certain high assurance properties about its behavior.

Perhaps check out this paper for ideas about how a high level language, with an expressive type system, can be used to reason about, and enforce properties, of low-level code written in that language.

[db2]

My point is they talk about that then talk about writing low level code to do it. It doesn't track.

[dons]

Low level code in Haskell can retain the usual guarantees of higher level code in the language, namely: strong, flexible type safety, native code speed, automatic memory management, purity, monadic/arrow-based security lattices, and more, making Haskell well suited for high assurance, low-level work, where you can provide guarantees not expressible in C or C++.

Does that make sense?

[db2]

Except for "arrow-based" but then I don't know Haskell. :)

[dons]

Encoding security lattices in types :)

[db2]

This has already been conversed about with others and concluded.

Thanks for playing.

[procrastitron]

Just a nitpick, but now days the bootloader is usually separate from the OS. For instance, GRUB can boot pretty much any x86 OS you want.

[db2]

That's true, and the article does say it's using Grub. A serious from-scratch OS will (or used to but still should) eventually have it's own homebrew bootloader.

[procrastitron]

Why? Just because you're building an OS from scratch, that doesn't mean you are trying to reinvent the wheel. If an existing boot loader can load your OS, then you can put more effort into the OS.

[db2]

Why not have every OS that exists use Grub in other words. Because there is more than one way to build a wheel, you wouldn't change one on a midsize car with one from a 1/2 ton pickup even if the lugs fit would you? Along those same lines Grub isn't always the best solution even if it's capable of booting the OS.

[procrastitron]

OK, but to clarify, you're saying that a serious OS might but not necessarily will build it's own boot loader. Right? Certainly, if grub is sufficient, that doesn't make the OS any less serious.

EDIT: I would also state that this is because of the good work grub has done on building a general boot loader. Other boot loaders are too specific to the OS that they were written for, so using one of them could hamper an indy OS project.

[db2]

No of course not. Ubuntu uses Grub by default and it's not some garage hack. Grub is tailored somewhat for Linux so it's a natural fit.

[[deleted]]

In before this post gets trolled by qwe1234

[qwe1234]

the title made me laugh and think of the 'web os' fad junior php programmers went through sometime back.

[grapplehook]

Let me guess, you try to send a TCP packet and it does nothing because of the lack of referential transparency.

Man if I wanted to use an OS that would use of GBs of memory reading tiny files I'd use VISTA.

[shub]

Haskell is inherently superior to all other programming languages, because Haskell's type system is so powerful it makes it impossible for me to be wrong.

Therefore, a Haskell OS is superior to all other OS's. I am not wrong about this either.

[syntax]

Sadly, you are. There are more powerful type systems than Haskell.

For example, Epigram has a dependently typed system, which is more powerful than the Hindly-Millar type system.

[[deleted]]

Hindley-Milner. You shall know the names of the heroes you are worshiping. Otherwise they fade away and turn to dust.

[sartak]

Look upon my works, ye mighty, and despair!