6 of 6Image
A screenshot of an seL4 microkernel instance; seL4 is 7500 lines of mathematically-proven C code. This removes one class of bugs and should make the kernel more secure. NICTA says that seL4 is impervious to buffer overflow attacks; however, mathematics cannot do away with human-injected design bugs.
(Credit: Chris Duckett/ZDNet.com.au)