|
|
|
|
|
|
by dahfizz
2701 days ago
|
|
|
Kind of a dumb question: have any operating systems been formally verified? Unless you are running an embedded application, verifying your software seems kind of pointless if you are still at the mercy of "unverified" system calls, memory manager, scheduler, etc etc. |
|
|
The standards there assume a TCB of about 10 kloc; 5kloc for the OS, 5kloc for each application. Separation is by static allocation—of disk space and memory usage, but also static time-domain multiplexing of CPU cores and IO lanes, with caches flushed on every context switch. They’re ferociously expensive to acquire in the first place, and then you take a huge operational penalty for running multiple applications.
There are very few problems for which this is a helpful solution—maybe not none, but very few when you could just buy several distinct computers, run them airgapped, and go about your business.