[nickpsecurity]

Thanks! Over time, I put together a lot of what I read in the thousands of CompSci, FOSS, and commercial works into a short summary of techniques for assuring software. We'll start with that:

https://pastebin.com/uyNfvqcp

So, there's a few concepts that apply here. You want the Trusted Computing Base, the part system depends on for security, to be as simple and easy to analyze as possible. The limit of verification that big spenders can afford is around 10,000 lines of code. You want it to be in a safe by default language (eg Ada + SPARK, Rust) or proven safe implementation (eg MISRA-C + RV-Match) that maps closely to resources of machine. Then, to catch leaks (important here), you must do a covert channel analysis of all shared resources in the system, esp memory or anything timed, to ensure an untrusted component can't acquire secrets from a trusted component. These were some basic requirements from 1980's security certification that prevented and detected problems in products from that time onward. One of biggest being cache-based, timing channels in VAX VMM in 1992.

Python doesn't map closely to hardware. Its implementation language isn't safe. You can't do covert channel analysis in it. It's also likely sitting on OS that's impossible to verify with tons of bugs each year. A nice, interim step before a verified OS is one we know they'll have trouble attacking or at least few can touch like OpenBSD. Currently, Rust or statically-analyzed C on OpenBSD for sender with full, memory safety for any components on Receiver and Transport. Simplified hardware that's up to date with hardware bugs. They need the extra work cuz the attackers will be hitting those with malicious input.