2 ms·

Can anyone more knowledgeable than me comment on whether I'm crazy to think 6500 lines seems amazingly tiny for a full blown hypervisor?!

• nickpsecurity 10y ago
  Most software is bloated with lots of features and doing too much in privileged mode. High-assurance security field keeps our privileged software tiny pushing everything else into either user-mode or separate, privileged components with clean interfaces that are easy to verify. Before this, there were separation kernels like INTEGRITY-178B that was EAL6+ verified for security due to being similarly small & easy-to-analyze. seL4 took it to next level with code & ASM verification but lacks many EAL6+ requirements. This one intends to boost productivity of code-level verification with DSL's. http://www.ghs.com/products/safety_critical/integrity-do-178b.html http://www.ghs.com/products/safety_critical/integrity-do-178... Note: The initial reason for keeping it small was that the formal tools just couldn't handle anything beyond 10,000 loc. Now, it's believed they might handle up to 100,000 with enough composition. Already partial verification, esp code-level, of large programs like Hyper-V w/ VCC. Full formal is work in progress at that level with tools like these going to be quite useful.