Adam ; on the assumption you are not on luv-talk, I have forwarded the following: I thought the tale below; in which Linux turned out to be the insecure element; might be of amusement. In a conversation with a gentleman at the Nicta "TechShowCsae2014" yesterday; http://www.eventbrite.com.au/e/nicta-tech-showcase-2014-tickets-12119157727?... he was explaining his group's interest in secure and bug-free software; in the context of 'mission-critical' applications; particularly OS's. I thought 'mission-critical' had something to do with the military and large corporation's; but it turned out they are primarily looking at the OS's in vehicles and air-craft. Apparently there have been recent cases of the "OS's' of cars being cracked remotely; via the wireless immobilizing system and the brakes etc. being operated remotely ! Regardless; the story seemed to be that as aircraft move from mechanical to electrical control and from there to fly-by-wire and then fly-by-fiber networks; (removing hundreds of kilo-meters of fire prone complex, heavy wiring in the process); a huge requirement for secure and bug-free OS's arose. Since sequential bug removal is not a practical option :-) What he seemed to be claiming was his group had written a RT OS in C; and then compiled it for ARM processors. Where things seemed to become interesting was 1/ the C code was apparently subject to some kind of mathematical analysis which 'somehow' checked the code's logical integrity against the specification ? (Is this possible ?) 2/ the machine code from the compiler was then checked against the specification ? - I have no idea what this means !; anyway the assumption is that the compiler may introduce bugs, security holes. Apparently the resulting RT OS has very little functionality, which is remedied by supplying that functionality via Linux VM's Anyway to get to the end of the tale; where Linux turned out to be the insecure element !;they are employing 'Red-Teams' (Tiger-teams ?) of hackers to 'crack' the Linux VM's. This is not just pie-in-the sky stuff either; they had a quad-copter with such an add-on OS;as proof of concept. Apparently the OS is available as open-source and binary for ARM and x86 CPU's, but not in the above secure form at: http://sel4.systems regards Rohan McLeod