Safe to the Last Instruction

Chris Hawblitzel and I just submitted the camera-ready version of our PLDI 2010 paper Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System.

The main idea is as follows. Much of traditional operating systems verification is quite difficult because the projects verify properties of low-level code. Microsoft's Singularity project aims to make the verification process easier by verifying an operating system written in a higher-level, type-safe language (C#) that provides memory safety properties for free. The problem here is that OS's necessarily have low-level code--for instance, context-switching code involves moving the stack pointer. We propose a verification approach that involves designing the OS around a small low-level "Nucleus" that we verify using Hoare logic, verifying the interface between the Nucleus and higher-level, type-safe code, and writing the rest of the OS using the higher-level language. We describe Verve, a prototype OS verified automatically end-to-end for type safety.

Abstract below; paper here:

Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code.We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. Our techniques and tools mechanically verify the safety of every assembly language instruction in the operating system, run-time system, drivers, and applications (in fact, every part of the system software except the boot loader). Verve consists of a “Nucleus” that provides primitive access to hardware and memory, a kernel that builds services on top of the Nucleus, and applications that run on top of the kernel. The Nucleus, written in verified assembly language, implements allocation, garbage collection, multiple stacks, interrupt handling, and device access. The kernel, written in C# and compiled to TAL, builds higher-level services, such as preemptive threads, on top of the Nucleus. A TAL checker verifies the safety of the kernel and applications. A Hoare-style verifier with an automated theorem prover verifies both the safety and correctness of the Nucleus. Verve is, to the best of our knowledge, the first operating system mechanically verified to guarantee both type and memory safety. More generally, Verve’s approach demonstrates a practical way to mix high-level typed code with low-level untyped code in a verifiably safe manner.

Chatroulette!

In the last couple of weeks I've spent a bit of time on Chatroulette, a site where you can video chat with random strangers in sequence, moving on to each next chat by clicking "Next." Here is a great video explaining how it works. Jon Stewart has a hilarious piece about it as well.

Bold Sell public speaking competition

Yesterday I attended the finals of the Bold Sell Competition, where contestants have to pitch a product they've never seen before using 6 slides they see as the audience sees them. (The organized has a blog post about this here.) This year's competition, a collaboration between the MIT Sloan Sales Club and the Harvard Business School Public Speaking Club, was completely hilarious. Contestants had to sell products from sinus-cleaning snakes to human-powered transport balls with all kinds of wacky target markets (a young Bill Gates sitting by CRT running an early version of Microsoft; a jail-bound Martha Stewart), revenue models, marketing teams (male dancers wearing only shiny lame shorts), competitive advantages (http://xkcd.com/210/), and descriptions of the competition. Below I include the video of the first place winner from this year; there are more videos here. There is a video of last year's winner here.

Desk in the closet

Thanks to my college roommate Aliza for sending me this. As Aliza says, I was about six years ahead of the trend by having my desk in the closet of our "study room"* freshman year. Also of note is the fact that freshman year of college was six years ago...

* That's a whole suite of stories in itself.

My first aerial acrobatics class!

Sunday I had my first aerial acrobatics class at Aircraft Aerial Arts* with Jill Maio. It was so much fun! The class consisted of three women (including me) who had never been on the equipment (corde lisse, aerial silk, and static trapeze) before. Jill (patiently) taught us basic skills such as how to climb the ropes, how to pose on the silks, how to go upside-down, and how to do seated and standing poses on the trapeze. I was able to do much more than I had expected--and it wasn't scary at all! I signed up for a 7-class introductory series this March through April. Cirque du Soleil, here I come!

* This place is really convenient--it is a 5-minute walk from Inman.

A.R.T.'s Donkey Show

Saturday I went to the American Repertory Theater's Donkey Show, which "tells the story of A Midsummer Night's Dream through the great 70s anthems." My friend Firth accurately describes it as "just kind of a big party." The show takes place at the Oberon, which has a stage in front of a large open dance floor area. There are raised platforms where audience members can rise to dance with glitter-covered "fairies" before the show. The show happens not just on the stage, but on the catwalk around the club and on the raised platforms as the audience dances to retro disco hits such as "We are Family" and "Ring My Bell" around the performance. After the show (at least, the 10:30 show) the DJ keeps the glitter-covered audience dancing for another hour before they kick everyone out. If you go, I recommend dressing 70's disco! (And I definitely recommend going!)

I posted pictures here.