seL4 Secure Micro kernel

"A nippy microkernel mathematically proven to be bug free*, and used to protect drones from hacking, will be released as open source tomorrow."



Has anyone heard about or seen this? How applicable is this to the Pixhawk, Pi or BeagleBone flight controller efforts? The best bit is that it seems to assure that all user mode code execution is isolated from the Kernel in such a way as to prevent crashing the kernel. I don't think this actually prevents bad FC code but it sounds like it could be a step in the right direction surely.



Without reading too much into this I did note that in the video they seem to say that the software "detects" malicious groundstations by monitoring for those that attempt to authenticate with the wrong password too many times. They also said that the GCS link was encrypted. I think what they actually mean is that their software overlays encryption to MAV connections and the FC detects attempts to communicate over unencrypted links. I'd hate for this to be another WEP style weak cipher that encrypts with a shared key or worse still some kind of authenticated SSL style link using a password based challenge response in each conversation



More details here

fonte:seL4 Secure Micro kernel - DIY Drones