@ Paul Suhler and others
It's an interesting read. It looks like one source of the article was stumped by the halting problem and inspired into this stuff. Others worked around it. I'm sure we'll get some interesting stuff out of the research. However, to actually secure things, we've learned over the decades what it takes. Most of what's in an Orange Book B2 (EAL5-equivalent) system's assurance requirements is better than modern systems' security. We had plenty of EAL5-7 systems production ready (and used) in 90's.
The old efforts taught us about development and economics. DJB's qmail put some of these principles to work and has been used with few to no security issues for years. XTS-400's are still around with more apps than before doing MLS security. Aonix (Java) and Adacore (Ada/SPARKS) offer development platforms for embedded software that dodge many issues caused by C/C++. JX is a whole OS stack running on a JVM with security elements comparable to EAL5-6. Cutting edge developments aim to produce processors that enforce security at the word level.
Some random musings about high assurance and UAV security follow.
Controlling subversion and ensuring requirements are met.
Here's a modern example of an old concept that helps a lot. The concept was splitting the system into trusted and untrusted components, reducing the amount of trusted code, and making the underlying TCB small/strong. Orange Book did that with security kernels. MILS is more typical today. Microkernels and separate processors are other solutions. This concept can help solve MANY problems.
One problem that UAV's face is interfacing operators to control. Ideally, we can have fancy GUI apps with OpenGL on our favorite OS. Ideally, we have full-featured Linux/BSD type networking options and plenty of link transmission types on UAV. Ideally, external input that's malicious can't bust through the system on either end in a way that affects control. Reality: modern setups are far from ideal. Another reality: getting pretty close to ideal is actually easy using the concept I outlined above.
Pretend there's one UAV operator console, a single UAV, and one radio communication link just for conceptual simplicity. First, we put a dedicated gateway between the operator console and possibly malicious network. This gateway runs high assurance software (e.g. Aesec's GEMSOS or a SKPP kernel). It receives outgoing commands, performs sanity checks on them per a policy, and sends them through a VPN tunnel. Tunnel establishment is done in a very robust way. The gateway also receives information from UAV, performing minimal checks, and sends it to operator console. Separate Ethernet/Networking stacks are used for each side and data is copied between them by TCB.
Within OpGateway: UserIPPackets->UntrustedRedNetworkingStack->GuardProcess->TrustedCryptoCore->UntrustedBlackNetworkingStack->UntrustedBlackNetwork
(Incoming works similarly in reverse. Independent modules for functions like setting up VPN connections, auditing, etc. UAV's gateway is similar, but a more embedded design.)
NSA and high assurance system developers can do a design like this because it's the kind they've been doing for decades. Just use secure kernel for TCB, split everything else into untrusted/semi-trusted partitions, and use assured pipelines to move data. I'd isolate GPS into it's own partition. I'd also include a process that, much like Clive's ideas, occasionally peeks into the partitions to ensure nothing is amiss. All data transfered from an untrusted partition to a trusted one must use a simple data format that's easy to parse and inspect (not XML!).
So, let's look at the issues. A component fails? Damage is isolated into a partition. Monitor notices, optionally logs some info on it, restarts the partition, and system continues as usual. What of network attackers? Well, traffic goes over a VPN whose endpoints have simple networking subsystems that are also isolated. What about a UAV issue? The gateway TCB can host monitoring software that detects issues, performs auto fixes or simply alerts operators.
What about malware on operator machine? Well, that usually indicates organization security issues ;) but the architecture helps: commands are sanity checked; no malware will be uploaded; rogue comms can be caught by monitoring; a compromised PC can be shutoff and doens't even have direct connection ability to UAV. Recovery? Hypervisors or coprocessors might be used on either node to allow the gateway/monitor to push updates. So, can quickly patch console or hotfix UAV control in mid-operation. Also, makes managing typical updates easier.
(Anyone thinking about what this REALLY means for the console might see why I prefer a non-Windows/x86 solution to the problem. Ideally, we'd have a SOC with simpler-than-x86 processor, few errata, MMU, IOMMU, onboard crypto, a ROM with high assurance base secure loader, flash for storing signed firmware/system images, a dedicated IO link to gateway, and everything built on top of THAT.)
So, you may be thinking: great, all we need is to spend a few years building this gateway thing and port some UAV operator software to a SOC. No, it gets better: them doing this crap for decades means there's many actual commercial products, prototypes, partial designs and design guidance in Lessons Learned-type papers. Here's a few options below.
Aesec just presented a high assurance guard design with isolation, assured pipelines, and GEMSOS security kernel at MILCOM 2012. The XTS-400's STOP OS was originally B3/EAL6. It's been used in guards for a long time and has Linux compatibility layer. Nizza and Perseus security architectures were used to build complicated applications whose security-critical parts were isolated on a microkernel. SKPP-like platforms are available for this too: INTEGRITY-178B (certified EAL6+), LynxSecure, VxWorks MILS (in eval for EAL6+), PikeOS (partly verified through Verisoft), OKL4/Verified (EA7+ design/implementation, not certified). The old KeyKOS, LOCK, and related projects could do things like this. Boeing SNS server (A1/EAL7 design) is still around for defense use and Boeing proposed a secure networking architecture around it.
So, it's not that they don't have the technology. They just keep reinventing the wheel and not using what they already have. Even my design eliminates many problems they might have. Simply rewriting the operator console software in type safe language running on a Linux VM (or write-preventing kernel) with app whitelisting and USB ports disabled would help plenty. ;)
Honestly, I think these companies just aren't trying to make secure platforms. The intense competition in UAV IT space means they are more focused on features and time to market. Their pace or profit motive keeps them from embedded security into each step of the design. It's the same old problem that killed the A1/EAL7 VAX VMM Security Kernel project. The only time things were different was when NSA/DOD mandated high assurance products for critical stuff, promised to buy only those and actually bought/used them. The moment they started deploying Windows NT and low assurance security products in mass was when everyone stopped building secure stuff (per Bell).
All the security research in the world won't change economics and IT sociology. Defending networks and systems isn't as much of a technical problem as people think. It's usually just a management or customer choice. They usually choose against high security.