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.

Re:Frosty piss

[The Snowman]

Researchers are actually studying ways to "prove" software is correct. For example, VDM-SL: http://en.wikipedia.org/wiki/V.... The problem that I see is that they can't prove the proving software is correct.

We can prove software is correct. The problem is that it is equivalent to the halting problem, which is NP. In other words, it is infeasible to prove correctness for all but the simplest programs.

Re:Frosty piss

[Firethorn]

Anyone who knows anything about software and crypto knows you cannot make the software "invulnerable" to attacks.

Well, it's a good thing they only specify 'large classes' then, right? They aren't saying it's invulnerable.

Still, something as 'simple' as running a VPN type encryption system would make your system effectively invulnerable to 'large classes' of attacks.

Personally, I see using 2 keys per channel, an encryption and a separate authenticator. Encrypt everything you send the plane and any plaintext transmissions look like nonesense. Sign all your packets and it can reject stuff that doesn't have the proper signature.

The complicated part is ensuring you don't take up too much extra bandwidth with the security while maintaining good connections even through noise/jamming.

Re:Frosty piss

[Anonymous Coward]

Researchers are actually studying ways to "prove" software is correct. For example, VDM-SL: http://en.wikipedia.org/wiki/V.... The problem that I see is that they can't prove the proving software is correct.

We can prove software is correct. The problem is that it is equivalent to the halting problem, which is NP. In other words, it is infeasible to prove correctness for all but the simplest programs.

False.

1. It is possible to prove all but the infeasably complex programs are correct.

2. The halting problem is actually untrue in reality since it applies to a "turing machine" rather than a "computer". The two are NOT the same thing. Turning machines have infinite memory, computers have limits on RAM. There are a finite (though huge) number of states a computer can be in.

3. Although difficult, as long as you assume programs rely on defined behavior, the state of the machine can be limited in all but the most complex cases. Even if we can't solve /every/ time with a universal algorithm, it is feasable to write a program which returns "can stop", "wont stop", "might stop" ... etc. Even a result of "might stop" could be useful enough to indicate an error/ etc.

4. If we prove correctness of subcomponents, the correctness of composite components can be proved. Eventually even a large program can be proven correct this way. It's fully feasable.

Re:Frosty piss

[Anonymous Coward]

The important observation is that the halting problem applies to software in general. If you take some subset of software, like, say, the set of programs that will pass a competent code review, then you probably will be able to solve the halting problem for those pieces of software. When proving complete formal correctness of a program (something which is not done often because with current techniques it takes absurd amounts of time from people with very specialized knowledge), you often intentionally design the program along with the proof so it is easier to make the proof go through. The papers on the design of the seL4 proven correct microkernel are a very interesting view into this process.

(Also, the halting problem is way harder than NP, it's recursively enumerable, which is sorta like NP in that elements of the set can by verified by a program except unlike NP which requires the program run efficiently (polynomial-time), recursively enumerable has no time limit, which is why you can't use that program to prove a negative: you can't distinguish waiting for the program to finish eventually from a program that will actually never finish.)

Re:Frosty piss

[jayesel]

Seems to me it's typical hubris from govt.

Re:Frosty piss

[ItzRobZ]

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

Well they did say invulnerable to large classes of attack, which already means that it's not "invulnerable" to all attacks.

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...

Re:How long

[DaRanged]

Have they learned nothing from 24 and Jack Bauer? ...or how long until something really 'bad' is orchestrated and they will blame hackers for it?

Re:How long

[Anonymous Coward]

About a couple of hours after 1 gets downed and it's found out that they all use the same key or password. 'Mathematically assured software' is very vague, it would be nice to know more details. The red team exercises need explanation too, if it was a black box exercise then its likely that there's a bug somewhere deep in an obscure code-path.

TL;DR secure embedded computing LOL

Re:How long

[Anonymous Coward]

Damnit!

Re:How long

[rmdingler]

In the real World, -resistant is not the same thing as -proof.

Many systems designed to be idiot-proof fail because they just keep making a better idiot.

Re:How long

[Meneth]

Yeah, TFA seems like propaganda related to the current season of 24, where American military drones are hacked by terrorists.

Re:How long

[TemperedAlchemist]

This is DARPA we're talking about.

One does not simply out smart DARPA.

Scary

[Anonymous Coward]

Either they're 50 years behind missile tech, or the abort signal of missiles can be hacked.

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.

Re:This is just silly

[VortexCortex]

Well, I think this is a bit different. Such comments may be apt to other offerings, but this uses industrial strength military grade antibacterial hypoalergenic drone security best practices.

Re:This is just silly

[Anonymous Coward]

So, I am a computer engineer working on this. The big 9 digit ones are very well protected by design practices that are even more anal and nitnoid than security hardened software design. The 8 digit ones pay lip service, and the smalls should never have been allowed to fly with the software they carry, nor should anyone who did any of the architecture ever be allowed near an airplane. There's a reason that an airplane GPS costs 100 times that of a handheld; there's a lot of procedure and testing to validate airworthiness in any digital fly by wire airplane, and it's missing in most UAVs. Even the small missiles like hellfires have a much more robust software design than the quad-copters.

Re:This is just silly

[PPH]

the US military's ideas on the importance of securing nuclear weapons

They load the software from 8 inch floppy disks.

Re:This is just silly

[LordLimecat]

'Mathematically-proven" is like using the word "clinical" in front of a toothpaste...means nothing other than to hype a product...

Er, no. Thats not what it means.

It means someone did an audit of something, and proved that that one piece does what its supposed to. Theyre probably talking about the crypto or comms bits.

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.

Nice Dice.

[nospam007]

Your Security Certificate ran out and nobody could be bothered to renew it.

AGAIN!

Re:Nice Dice.

[sound vision]

Jesus... sometimes this place is worse than the web hosting customers I deal with. "What do you mean the SSL expired? I didn't know it had to be renewed! Why wasn't I notified!!" "Sir, the certificates come with an expiration date the moment they're issued..."

hehe

[Anonymous Coward]

Mathematically proven? Since when has reality ever been that simple... Expose it to internet and make hacking contest, nice price for first to penetrate it and your have some real world testing...

Real world hackers have much more ideas how to hack something then some pentagon development lab...

Perhaps...

[LongearedBat]

Perhaps the computer is built using IC's, uses tape decks for storage and communicates via CB radio...?

Re:Perhaps...

[camperdave]

Of course it is built using ICs. You don't expect them to solder together billions of individual transistors, do you?

Publish the code

[throx]

If it's properly secure then open source the code. Security is in the algorithm, not the implementation.

Why not just use a one-time-pad? Get the launch crew to type it in on mission start?

Re:Publish the code

[Yaur]

What, besides a OTP is "mathematically proven" to be secure? Probably that is what they are using, though hopefully with a hardware entropy source and some physical connection required to replace the key data. Biggest issue here would be getting the grunts in the field to actually replace the key unless doing so is required to get it to launch. OTOH "mathematically proven" could just be technobable that means "built on problems that are assumed to be hard."

Re:unhackable....Challange accepted

[profplump]

If only there was some sort of completely internal guidance system available for aircraft.

Hackem' ???

[tomhath]

The program, called High Assurance Cyber Military Systems, or HACMS

At least they have a sense of humor.

Re:Hackem' ???

[K. S. Kyosuke]

It sounds like "Hackmas" to me - the hacker's equivalent of Christmas. So, yes, it feels sort of incongruous.

Re:Hackem' ???

[drinkypoo]

Or, obviously, hack microsoft. It's running Windows for Drones.

Re:aren't all drones designed to be hack resistant

[Anonymous Coward]

That has been the case with the video feeds coming out of drones: http://www.wired.com/2009/12/insurgents-intercept-drone-video-in-king-sized-security-breach/

found the key

[cellocgw]

Turns out they're using the same key as the old DVD players. You can get that from the usual sources, including a few slashposters' signature lines.

Re:"mathematically proven"

[K. S. Kyosuke]

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

To quote the bard

[woboyle]

According to Bruce Schneier, anybody can write an encryption algorithm that they cannot hack, but until the algorithm is published and "in the wild", that's as much as you can say about it. So yes, let us see the protocols, algorithms, and code and then we can say whether or not it is "unhackable". My guess... not very.

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

Re:aren't all drones designed to be hack resistant

[K. S. Kyosuke]

Are they implying that all previous drones have no security? Just connect to them and take over.

That's the guiding principle behind the Free War movement, as conceived by the "Make War, Not Love" anti-hippies at the DoD.

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

Land the drones

[seven of five]

The current season of 24 could be cut short if the US gov't simply landed the drones....

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.

Re:Seriously people?

[Anonymous Coward]

Typically formal verification is done against the specification to prove that it meets the specification correctly. That's all well and good. However, it also assumes that the formal specification contains no flaw, holes, etc. For any complex system, and this is one, designing a specification without flaws is, at least, very difficult.

Beyond that, the biggest security threat is the wetware and testing wetware for security issues is NOT mathematically possible.

But how well is it shielded?

[Anonymous Coward]

Glad the software will be un-hackable as it crashes to earth, when someone paints it with a large antenna and car battery blasting EM noise.

"unveiled a new drone..."

[buybuydandavis]

"unveiled a new drone... built with secure software that prevents the control and navigation of the aircraft from being hacked"

So, um, what does that imply about the *existing* drones?

I sure do hope they explain in detail the current vulnerabilities in the current models that they've overcome with their shiny new solution.

Security of drones

[rossdee]

The first thing I would do is have directional antennas and only accept commands from above (ie satellites)

Mathematically proven...

[NonSenseAgency]

I can mathematically prove that you are a figment of my imagination. This is like that old saying about logic...it's a way of going wrong with confidence. Obviously some PR flake wrote the press release, no sane engineer would ever have made such statements.

If it can be remotely controlled

[nurb432]

It can be attacked.

The only chance you have is raising the bar so high no one can practically manage it, but never think it *cant* be done or it will bite you in the ass.

Formally verified

[Anonymous Coward]

By "mathematically proven" the article means "formally verified" and it means that there is a machine-check mathematical proof that states that under certain assumptions (hardware is correct, etc), the software on the system would fullfill its specifications, regardless of anything and everything else that may be going on. This can be hacked only if the attacker is able to either subvert some of the assumptions, or if the specification itself is too weak. Both are at least a theoretical possibility, but it is indeed "hack-resistent" (while not necessarily 100% hack-proof). And by the way, the code is all open source - see http://smaccmpilot.org/

E-bomb proof?

[JimSadler]

I wonder if they can shield these drones against an e-bomb. In a way if you knock out navigation while a drone is over friendly areas you turn the drone into a random, terror, device. I suspect that trying to shield a drone from an e-bomb would be very difficult. Apparently the Air force is able to shield war planes against electronic shock but they have many redundant systems whereas drones might not be able to carry all of the shielding and backup systems. When we invaded Iraq we probably had an e-bomb capacity that could shut down every car with almost any kind of electronics. In a high traffic city the congestion would be a real problem for mobilizing their military. It is not as if all those cars and trucks would start after a while. They would all need repairs.

Hacker Resistant Drone?

[Optali]

I assume you meant to write Hack Resistant Drone Control System, innit? Sounds rather useless, gimme a glaive beam and a chain ion and I will take care of the hack myself.