Let us begin
Thanks for visiting my blog! This post is an introduction of sorts, explaining what I'm doing, why I'm doing it and where I'm starting from.
So without further ado, what am I doing?
I'm going to write a working operating system which can run real workloads, written in FStar and Pulse, based on the SEL4 micro-kernel. My operating system will be secure for some formal definition of secure.
Why write an operating system?
- Operating systems are cool
- Formal verification is really cool
- SEL4 is very cool indeed
- I can
I care about writing safe and secure software, and I think understanding how things work is fun. Operating systems are pretty fundamental now society is more and more digitised (a mistake if you ask me, but there we go). Having secure operating systems that are usable outside of aerospace and defense can only be a good thing now that AI is accelerating vulnerability research. I have a long term interest in micro-kernels, so it'll be fun to go from knowing some of the theory to writing my own micro-kernel purely for it's own sake. I also want to learn how to write proof-oriented programs which are mathematically proven to be correct, safe and secure. I like doing a good job and this seems a good approach to me, but I also think this is where industry is headed so it's good to have the formal verification string in my bow.
If you'll indulge me, there are also some philosophical reasons I want to do this: a lot of the software stacks we use everyday are made up of legacy code, written in unsafe languages with a huge amount of inertia and technical debt. I argue we should burn it all down and start from scratch, because we now have the tools (FStar, Pulse, Everparse, Z3, etc) to do the right thing once at scale: let's write the essential stuff using proof-oriented languages, do a good job and then have fun breaking new ground. There are only so many decompression libraries the world needs.
I want to see if it's possible for one person to write a very basic formally verified operating system using relatively new tools and techniques which lower the barrier to entry. I don't expect it will ever be used, but hopefully in it's own small way it might inspire others to try to do the same thing for essential stacks. Bad code has disproportionate real world consequences, and everyday people should not have to bear the costs of our failures as a profession to meet standards required in any other engineering profession.
So that's the what and the why, lets see where I'm starting from: I have an undergraduate maths degree. I have roughly five years experience doing a combination of software development, reverse engineering and vulnerability research. I know some operating systems theory but have no formal training. Realistically I probably know enough to think I have an idea of what I'm doing all the while making fundamental errors - I suppose I'll find out along the way.
Finally, I also want to explore whether large language models will help or hinder me. Programming and mathematics are relatively constrained domains compared to other domains which deal with messy squishy stuff. Because of this LLMs may be able to help speed up the translation of well understood ideas into proof-oriented languages such as FStar. I want to see if that’s the case in practice. That said, there is emerging research which is starting to tease out the limitations of LLMs as a technology as well as the potential long term consequences of generative AI use on our ability to think critically for sustained periods of time (note: I’m not qualified to comment on this in any meaningful way and, as far as I know, the literature hasn’t reached a consensus yet). It’ll be interesting finding the right balance.
In future posts I'll talk about more of the background stuff, what FStar and Pulse are, why I’m using them, what they get me and give a brief overview of SEL4.