1. 22

  2. 10

    Experience writing verified software:

    We started to get used to the verified Nucleus code working the first time for each new feature we implemented. When we set up the first interrupt table, fault handling worked correctly the first time. When we programmed and enabled the timer, preemptive interrupts worked correctly the first time. In fact, after dropping the debugger stub, everything worked the first time, except (a description of toolchain bug follows).

    1. 6

      One thing I didn’t mention about this OS is it’s possibly an example of them learning from the past. When the pricks patented some of it, I looked for prior art knowing I saw Nucleus-style design before. Found it:


      That design was ahead of its time. They did a Nucleus kernel to handle the low-level parts of an OS so their OS or any other wouldn’t have to. It could be higher-level. The higher-level components would also be consistent since they shared critical features. Everything, even OS components, ran in its own process. Best: firmware was read-only with one source saying you had to physically swap it. No BIOS attacks or need for TPM. This was late 70’s to early 80’s.

      Some people at Microsoft maybe paying attention to good, prior work. They still don’t do the simple, ROM-based technique for tamperproof firmware. They’re all over the TCG/TPM/UEFI stuff instead. So, they’re safe down to the last… UEFI vulnerability? ;)

      1. 2

        I feel like some of these verified kernels have the advantage of lots of prior knowledge. In a way they know what works and what doesn’t and so the core design won’t need to be redone as much as if the concepts were totally new.

        If you end up verifying a design that ends up being poor, you just wasted a lot of effort.

        1. 4

          If you end up verifying a design that ends up being poor, you just wasted a lot of effort.

          That’s why this work concentrates on reducing effort. In fact, the paper discusses the experience of verifying a design that ends up being poor!

          This small verification time enormously aided the Nucleus design and implementation, because it gave us the freedom to experiment with different designs. Often we would finish implementing and verifying a feature using one design, only to become dissatisfied with the complexity of the interface or limitations in the design. In such cases, we were able to redesign and re-implement the feature in a matter of days rather than months, because we could make minor changes to large, Nucleus-wide invariants and then run the automated theorem prover to quickly re-verify the entire Nucleus.