That was the point of the research: throw away how everything has been done and explore what a clean slate redesign would look like if we had the benefit of 30-40 years of hindsight.

The easiest way to implement transparent paging would be to have a paging block that exposed the memory manager API (allocate, free, read, write) and would proxy requests to either RAM or disk as appropriate. But since I was targeting embedded devices, it was assumed that you would explicitly allocate buffers in on-die RAM, off-die RAM, or flash as required. The architecture was very much NUMA in nature.

The prototype made for my thesis only allowed the "terminate" request to come from the process requesting its own termination. It would be entirely plausible to add access controls that allowed a designated supervisor process to terminate it as well.

Remote memory can be inspected, but only with explicit consent. I had a full gdbserver that would access memory by proxying through the L1 cache of the thread context being debugged. (Which, of course, had the ability to say no if it didn't want to be debugged).

The goal was to have a system that had very small number of trusted hardware blocks which did only one thing, then build an OS on top of it microkernel style - except that all you have is unprivileged servers, there's no longer any software on top.

What was your plan to address things like hardware bugs/errata/updates? How could someone initiate a firmware flash in this sort of system?

Keep the hardware design as simple as possible, formally verify everything critical, then run the rest as userspace software and hope you got all the critical bugs.

The point wasn't to move everything into silicon, it was to move just enough into silicon that you no longer needed any code in ring-0.

As an example, the memory controller's access control list and allocator was a FIFO of free pages and an array storing an owner for each page. Super simple, very few gates, hard to get wrong, and easy to verify.

What about the more complex hardware such as the CPU? There are plenty of opportunities for mistakes there, some not so obvious (such as Spectre attacks). And I can't imagine you'd get away with completely isolating it like the memory.

My long term plan was actually to do a full formal verification of the CPU against the ISA spec and prove no state leakage between thread contexts, but I didn't have time to do that before I graduated

I deliberately went with a very simple CPU (2-way in order, barrel scheduler with no pipeline forwarding, no speculation or branch prediction) to minimize opportunities for things to go wrong and keep the design simple enough that full end to end formal in the future would be tractable. Spectre/Meltdown are a perfect example of attack classes that are entirely eliminated by such a simple design.

I was targeting safety critical systems where you're willing to give up some CPU performance for extreme levels of assurance that the system won't fail on you.

At what point does it become easier to formally verify the software than the hardware? Certainly it's easier to change the software than the hardware, so there is already incentive to not move things into hardware that need not be there.

Since software is so easy to change, nobody bothers verifying it. The more we put into software, the more room there is for cutting corners in testing because, "we can always send out a firmware upgrade later." Me, I'd rather go back to the old days when updates to hardware were expensive so you better get it right.

It's like writing with a ball pen vs a pencil. But you could be just as careful with a pencil. I'm just wondering if what you are proposing is the equivalent of runes.