DARPA Unveils Hack-Resistant Drone

savuporo (658486) writes with news based on the work of a DARPA project known as High Assurance Cyber Military Systems: "'The Pentagon's research arm unveiled a new drone built with secure software that "prevents the control and navigation of the aircraft from being hacked. ... The software is designed to make sure a hacker cannot take over control of a UAS. The software is mathematically proven to be invulnerable to large classes of attack,' [HACMS program manager Kathleen] Fisher said." This is currently being demoed on a quad-copter platform. It would be interesting to know the CPU architecture, chipset, programming language and the suite of communication protol this thing uses ."

Comments

Frosty piss

[Anonymous Coward]

There ain't no such thing as 'hacker-resistant'.

Re:Frosty piss

[The Snowman]

There ain't no such thing as 'hacker-resistant'.

Yep, I especially loved this gem from the summary:

The software is mathematically proven to be invulnerable to large classes of attack

Anyone who knows anything about software and crypto knows you cannot make the software "invulnerable" to attacks. You can greatly decrease the number of bugs and known attack vectors. You can make it infeasible to brute-force your system using a realistic amount of computing power. But you do not know what you do now know, and the system cannot be 100% secure.

I would love to see how they "mathematically proved" it is 100% secure (invulnerable, remember).

Re:Frosty piss

[LordLimecat]

Perhaps what theyre getting at is that there is a very limited network exposed portion of the software that is isolated from everything else, and is simply responsible for the creation of a control channel-- basically, a chip that just handles establishing the VPN, and allowing VPN'd comms in and nothing else.

It may be possible, in such a situation, to perform an audit which establishes that that code does exactly what it says it does, and nothing else. I understand such audits are possible, but generally very difficult with anything more complex than "hello world". Perhaps thats what they did here.

Re:Frosty piss

[sound vision]

The quote reads:
"The software is mathematically proven to be invulnerable..."
wait for it-
"...to large classes of attack."

Since he does say 'mathematically proven', probably he's referring to some cryptographic subsystem of the software, maybe even just the encryption algorithm itself. But whatever he is referring to, the statement is that it is invulnerable to some types of attack (not all types of attack). This is just standard propaganda designed to give the impression of "our forces are invincible!". In this case, the propaganda might even be factually correct, but the way it's phrased is designed to give people with poor reading comprehension the idea that the drones are invincible. Apparently, that is the meaning you took from it as well.

How long

[vikingpower]

before someone takes over one of these babies ? I mean - for a challenge, this is about the same thing as waving a kilogram of prime steak in front of a pride of lions...

This is just silly

[rebelwarlock]

How many ways is this ridiculous? In the summary alone, you have quite a lot of nonsense. First, they brag about secure software. Your software is supposed to be secure, especially for something like this. You don't get bonus points because you thought about security where weapons were concerned. That's like bragging about not shitting your pants. Of course their security software is designed to prevent hacking - that's the point. Then you have the mathematical proof, which is just a fancy way of saying they ran a code analysis tool and their software totes doesn't have buffer overflow vulnerabilities, guys! If they really got fancy with it, maybe they could test it against real life security penetration testers, but let's not get ahead of ourselves.

Re:This is just silly

[AmiMoJo]

Rather than bragging they should be hanging their heads in shame and apologising for the shoddy work they did. They already lost a few of these drones, including one hacked by Iran. Security should have been the first thing on their minds, not the last.

This is just silly

[craigminah]

No kidding. I wouldn't even say "he hasn't missed a field goal in 43 attempts, this is a chip shot" because you'll put a rook on it and fail somehow. Heck, the US Government can't even put up a fricking (healthcare) website so how can they expect to succeed at making a "hacker proof drone"? 'Mathematically-proven" is like using the word "clinical" in front of a toothpaste...means nothing other than to hype a product...

Re:"mathematically proven"

[arglebargle_xiv]

Beware of bugs in the above code; I have only proved it correct, not tried it -- Donald Knuth

aren't all drones designed to be hack resistant?

[Punto]

That summary says absolutely nothing. Are they implying that all previous drones have no security? Just connect to them and take over. Luckily some genius from DARPA came up with the brilliant idea of adding a password prompt.

Re:"mathematically proven"

[K. S. Kyosuke]

You're saying I shouldn't be flying that TeXcopter I built in my backyard?

Re:"mathematically proven"

[DNS-and-BIND]

That's a misquote, like "Play it again, Sam."

"Note that I have not tested this code, I have merely proven it correct."
--Donald Knuth

Re:"mathematically proven"

[VortexCortex]

"To determine who really rules, all you hafta do is ask: Who am I not allowed to misquote?"
- Voltaire

Re:To quote the bard

[VortexCortex]

While I agree, and in no way trust the words of defense contractors, this is a common sentiment that's usually applied a bit broadly. One must realize that all security is security through obscurity. Each bit of obscurity increases the effective security exponentially. Yes, it may very well be that not having access to the cipher algorithms in use only provides a few bits of security since they're likely using one of the existing cipher systems, however those are a few bits of security that do exist if not disclosed. Now, (this would be overkill), but let's say they are chaining multiple ciphers together, say, Plaintext -> RC4 -> AES -> Ciphertext, and lets say they repeat that loop N times. Apart from the ciphers themselves the number and order of ciphers and iterations of the loops adds a few more bits of security through obscurity. Each stage of unknown cipher adds a few more bits of security in the selection of that cipher.

Indeed, this is how a cipher itself is built up from the various cryptographic primitives such as mix-rows, S-boxes, XORs, Look-up-tables, processions along a curve, block-chaining strategies, etc. reversible input to output mappings. I've just abstracted the process of constructing a cipher and described it using ciphers themselves in a way that can increase security exponentially even if you do know the details of the ciphers, but without knowing the details we can consider the system that much more secure. If the machine falls into enemy hands or details are leaked then our "element of surprise" bonus to the security is lost, but while it is not divulged it demonstrably more secure -- The same is true of cipher keys themselves, knowing a little bit of the key doesn't break the security but it weakens it; So consider these secret bits part of the key. All security is security by obscurity.

Now, purely hypothetically, let's say I built such a system that uses dual key expansions to derive both the key to use for the ciphers but also to seed a good random number generator which is then used to select which ciphers to chain together and in what order (perhaps the running time of iterations is computed to provide a fixe CPU load). Now, since the cryptographic primitives and implementations themselves have all been hacked on and accepted within the security community, this method of ciphering would also be considered at least as secure without really needing to vet the process. At worst its exponentially more secure than the currently accepted ciphers widely used today.

Do I really need to have everyone hack on this system to assure you it's safe? No. Not really. I could reveal the details to some trusted 3rd party, maybe call him Bruce Security. or BS for short. Then BS can be sworn to secrecy, and yet without revealing the details publicly or hammering on it BS could tell you: "Yes, this system is very secure, even more secure than any crypto system currently in use in the industry." And he'd be right even if such claims on the surface seem highly unlikely due to your own assumptions.

I make a similar argument in the practical vs worst-case time (big O notation) when selecting algorithms. For example: Red-Black Trees were chosen for C++'s map implementation. It was the "academically" and "provably correct" choice not to include hash-maps in the implementation instead or in addition. Practical folks said: FUCK! I need a damn hash-table, because its practical key-location case runs in constant-time, and I need that speed (one of the main reasons folks choose a compiled language). So, everyone went off and made their own hash-table implementations for their maps, some folks even drug out their existing C implementations and used them. Later, since everyone was demanding the standards board pull its head from its ass and give us what we want, they finally added a hash-table implementation in C++2011. However, now we have a bunch of existing codebases using non-standard hash-map implementations which will remain in place (because if it's not brok

Seriously people?

[Typical Slashdotter]

I admit that the article doesn't go into any technical details, but the number of comments here that are completely ignorant of what formal verification is and reject that it is even possible is...disturbing. (See CompCert for a real-world example of this practice.) Since the article was so bad, I don't know what the team actually did, but "mathematically proven to be invulnerable to large classes of attack" is exactly the sort of prudent statement I would expect from someone who has done good work making a hardened system.