Re:Antikernel: A Decentralized Secure Operating System Archi...
by aidenn0 on Friday June 18, 2021 @02:23PM
(#27553281)
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.
Re:Antikernel: A Decentralized Secure Operating System Archi...
by akkartik on Friday June 18, 2021 @03:56PM
(#27554275)
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.
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.