I remember watching a talk where a formal methods researcher was talking about how, with the help of some grad students, they rebuilt one of Boeing's helicopter

I remember watching a talk where a formal methods researcher was talking about how, with the help of some grad students, they rebuilt one of Boeing's helicopter drone's flight control systems to use sel4 in a collaboration with DARPA. From memory the external security researchers could easily compromise the existing software, but failed to penetrate into the formally verified sel4 rewrite, even when they were given backdoor access to one of the subsystems as a helping hand. Every time they tried to escape the subsytem, seL4 would reboot them, leading the security researchers to say that it was the most secure flight control system they'd ever tested. I'll see if I can dig it up - feel free to take it skeptically, I don't know how easy this experience was to reproduce. It was a pretty cool case study, however. Edit: This was the one! "Kathleen Fisher - From quadcopters to helicopters" https://www.youtube.com/watch?v=TH0tDGk19_c https://www.youtube.com/watch?v=TH0tDGk19_c Here's a mirror of an article from the ACM with more details: https://sudonull.com/post/3016 https://sudonull.com/post/3016