Re: Whoa, hang on
Nobody has *ever* managed to make a computer system which they are *certain* is secure and is actually secure. Ever.
People regularly make a computer system which they are *certain* is secure, and it's always eventually hacked.
People have tried with formal proofs that their code does what they expect. But:
* People get the proofs wrong, leading to exploitable security bugs. (e.g. Tokeneer Project)
* You're often only proving your code matches the spec. Spec errors lead to exploitable security bugs. E.g. see Viper microprocessor
* You may have perfect high level or C code, then your compiler has a bug that leads to a security bug. (Viper had the hardware equivalent of this - their low-level "proven" design didn't match the hardware as manufactured)
* Even if the program is perfect, hardware has bugs that may lead to exploitable vulnerabilities (e.g. RowHammer, CPU errata)
The only way I'd trust a firewall between the aircraft control and passenger systems is if it was actually physically one-way data flow, e.g. there's a system connected to the aircraft control network that extracts the aircraft position/altitude/course and sends it down a one-way fibre-optic link to a separate system that's connected to the passenger network. That way, it's impossible for a hacker in the passenger systems to affect the aircraft control systems.
(By a "one way fibre optic link" I mean that the sending side has a LED or laser, but no light sensor, so it can't be affected by the system at the other end of the link).