This is a nice improvement over my own design for something similar and Rockwell-Collins' AAMP7G. The latter is a stack-based CPU with a built-in separation kernel whose hardware and microcode were mathematically proven to be correct and secure. NSA rated it at EAL7. That’s embedded and proprietary, though. Good we have a new one to play with that’s even more capable in theory.
Antikernel is a decentralized architecture with no system calls; all OS functionality is accessed through message passing directly to the relevant service.
So… a microkernel?
The hardware integration is pretty neat. This seems different from microkernels in that some of the services are implemented directly in verifiable hardware rather than in userspace software. For example:
To create a process, the user sends a message to the CPU core he wishes to run it on. To allocate memory, he sends a message to the RAM controller.
Sort of. Like a cross between them and separation kernels. The separation kernels are microkernels designed to be tiny, just enforce security + basic stuff, stop leaks, and easy to verify. Looks like they’ve made a separation kernel for a network on a chip model whose key components are implemented in hardware instead of software. Scheme protects both in regular operations and DMA instead of separate ones like in some schemes.
A side benefit is that the tooling for formal verification of hardware is really mature. There’s quite a bit of it. This one even went through Yosys, which is open-source. Same guy behind it as Icestorm FPGA project. This means the Qflow methodology that leverages it might be employed for an open hardware produced with open synthesis. At that point, it’s just verifying resulting transistors were what’s on the chip. Plus the analog stuff which is done by hand in CAD and Spice tools.
The dissertation with survey of other work and thorough details is here:
http://redmine.drawersteak.com/attachments/download/3/thesis-final.pdf
Code is supposed to be BSD licensed. Found a Github:
https://github.com/azonenberg/antikernel
This is a nice improvement over my own design for something similar and Rockwell-Collins' AAMP7G. The latter is a stack-based CPU with a built-in separation kernel whose hardware and microcode were mathematically proven to be correct and secure. NSA rated it at EAL7. That’s embedded and proprietary, though. Good we have a new one to play with that’s even more capable in theory.
So… a microkernel?
The hardware integration is pretty neat. This seems different from microkernels in that some of the services are implemented directly in verifiable hardware rather than in userspace software. For example:
“So… a microkernel?”
Sort of. Like a cross between them and separation kernels. The separation kernels are microkernels designed to be tiny, just enforce security + basic stuff, stop leaks, and easy to verify. Looks like they’ve made a separation kernel for a network on a chip model whose key components are implemented in hardware instead of software. Scheme protects both in regular operations and DMA instead of separate ones like in some schemes.
A side benefit is that the tooling for formal verification of hardware is really mature. There’s quite a bit of it. This one even went through Yosys, which is open-source. Same guy behind it as Icestorm FPGA project. This means the Qflow methodology that leverages it might be employed for an open hardware produced with open synthesis. At that point, it’s just verifying resulting transistors were what’s on the chip. Plus the analog stuff which is done by hand in CAD and Spice tools.