Beta
×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

DARPA Unveils Hack-Resistant Drone

timothy posted about 4 months ago | from the nothing's-perfect dept.

Security 107

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

cancel ×

107 comments

Sorry! There are no comments related to the filter you selected.

Frosty piss (2, Insightful)

Anonymous Coward | about 4 months ago | (#47082013)

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

Re:Frosty piss (0)

Anonymous Coward | about 4 months ago | (#47082265)

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

Ofcourse there is.

Heck, even applying ROT13 on the stream would be enough to validate that 'hacker-resistant' claim.

The question is "how much is it 'hacker-resistant' ".

And that isn't easily quantifiable -- especially not time is also a factor: Basic DES was a good encryption. Nowerdays its classified as (at best) "weak".

If you mean that there is nothing as 'hacker proof', than I'll agree with you. Even though the breaking of a certain encryption might take longer than the rest of the humans existance. :-)

Re:Frosty piss (0)

Anonymous Coward | about 4 months ago | (#47084401)

Triple DES was and is still a very good cipher. The 56bit keyspace issue was not a weakness per se, but the preconidition for NSA to allow export. You can also easily modify DES to have much more keyspace and thereby make a very good cipher from it.

Re:Frosty piss (0)

Anonymous Coward | about 4 months ago | (#47082279)

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

...says the person who clearly does not know the difference between hack resisistant and hackproof...

Re:Frosty piss (-1)

Anonymous Coward | about 4 months ago | (#47082405)

...says the person who clearly does not know the difference between a double negative and a single negative...

Re:Frosty piss (-1)

Anonymous Coward | about 4 months ago | (#47082477)

Double negative sentences czech out to me just fine!

Re:Frosty piss (5, Insightful)

The Snowman (116231) | about 4 months ago | (#47082687)

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 (2)

LordLimecat (1103839) | about 4 months ago | (#47082945)

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 (0)

Anonymous Coward | about 4 months ago | (#47084419)

If you folks had a clue, you would know L4.

Here is another attempt from Germany to clean up the Bell Labs C/C++ mess:

http://sourceforge.net/p/sappeurcompiler/code-0/HEAD/tree/trunk/doc/SAPPEUR.pdf

Re:Frosty piss (2)

sound+vision (884283) | about 4 months ago | (#47083783)

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 (0)

Anonymous Coward | about 4 months ago | (#47084437)

Disregarding your cynicism, what it means is that these folks attempt to prove correctness of code, but are cautious folks and not Used Car Salesmen. Or, Unused Software Salesmen.

As I posted before, look at L4 and the compiler from INRIA before you continue to chicken crap.

Re:Frosty piss (0)

Anonymous Coward | about 4 months ago | (#47084033)

Formal verification is a thing that exists if you want to put in the legwork.

Re:Frosty piss (0)

Anonymous Coward | about 4 months ago | (#47084827)

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

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

Re:Frosty piss (1)

The Snowman (116231) | about 4 months ago | (#47085255)

Researchers are actually studying ways to "prove" software is correct. For example, VDM-SL: http://en.wikipedia.org/wiki/V... [wikipedia.org] . 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 [wikipedia.org] , which is NP. In other words, it is infeasible to prove correctness for all but the simplest programs.

Re:Frosty piss (1)

Anonymous Coward | about 4 months ago | (#47085829)

Researchers are actually studying ways to "prove" software is correct. For example, VDM-SL: http://en.wikipedia.org/wiki/V... [wikipedia.org] . 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 [wikipedia.org] , 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 (1)

Anonymous Coward | about 4 months ago | (#47086133)

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 [nicta.com.au] proven correct microkernel are a very interesting view into this process.

(Also, the halting problem is way harder than NP, it's recursively enumerable [wikipedia.org] , 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 (0)

Anonymous Coward | about 4 months ago | (#47086147)

The problem that I see is that they can't prove the proving software is correct.

Actually, I'd argue that the larger problem is being sure that you are proving what you actually want to prove. Proving software can be structured so the actual trusted portion can be very small. For example, the trusted kernel of Coq is tiny: I believe it's on the order of 100 lines of code. That have been scoured over by experts in formal correctness. I would be very, very surprised if it had a bug.

Re:Frosty piss (1)

Firethorn (177587) | about 4 months ago | (#47085497)

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.

Just because (0)

Anonymous Coward | about 4 months ago | (#47084407)

...you have only worked with commercial-grade shitball software (and most of FOSS is the same ) means very little.

See L4 from Uni Dresden for a counter-argument.

How long (4, Insightful)

vikingpower (768921) | about 4 months ago | (#47082019)

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 (1)

DaRanged (735002) | about 4 months ago | (#47082107)

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 (1)

Anonymous Coward | about 4 months ago | (#47082167)

Damnit!

Re:How long (1)

Meneth (872868) | about 4 months ago | (#47082645)

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

Land the drones (1)

seven of five (578993) | about 4 months ago | (#47083029)

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

Re:How long (0)

Anonymous Coward | about 4 months ago | (#47084989)

This season is the first season I've watched 24. Very disappointed with their technical advisors: saw Chloe enter a "secure" IP address (whatever that is) that started with 2.718 (don't recall the last two octets as I was too shocked by the second octet). 718? Really? How hard is it to create a real IP address?

Re:How long (1)

Anonymous Coward | about 4 months ago | (#47082119)

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

Mathematically assured software (0)

Anonymous Coward | about 4 months ago | (#47082497)

All software is mathematics...

All the phrase means is that the math has been proven correct. Now, until that proof has be rechecked by several dozen other mathematicians it isn't necessarily valid.

the problem with actually proving software isn't the mathematics... It is the time it takes to carry out the proof. And when the proof shows an error, it has to be redone after the error is "corrected".

So far, only trivial amounts of software have ever been mathematically proven. It helps to use a more mathematically oriented language (ML, camel...) for the software, as the language itself limits side effects (which are a disaster for proofs).

Re:How long (1)

rmdingler (1955220) | about 4 months ago | (#47082565)

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 (1)

TemperedAlchemist (2045966) | about 4 months ago | (#47082653)

This is DARPA we're talking about.

One does not simply out smart DARPA.

so now.. (2)

strstr (539330) | about 4 months ago | (#47082027)

If the government programs this thing to attack, it cannot be shutdown by outsiders, even if the attack is against their own citizens!

Got proof of them planning to assassinate and target USA citizens with this technology, just like they do their directed energy and weapons platforms @ http://www.obamasweapon.com/ [obamasweapon.com]

Beware the corrupt United States government, people..

Re:so now.. (-1)

Anonymous Coward | about 4 months ago | (#47082065)

Kill yourself, paranoid worthless piece of shit.

Scary (1)

Anonymous Coward | about 4 months ago | (#47082031)

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

Um.. (0)

Anonymous Coward | about 4 months ago | (#47082045)

How is a proof that one particular class of bugs won't affect a system the same as it being unhackable or invulnerable to being hijacked?

Evidently the have been paying attention then.... (0)

Anonymous Coward | about 4 months ago | (#47082055)

....to the latest 24 episodes

unhackable....Challange accepted (0)

Anonymous Coward | about 4 months ago | (#47082085)

nothing is unhackable.
if humans made it there is a flaw in it guaranteed.

Lets take for example the weakness of gps spoofing.
Apperantly Iran already done that with one of america's their top drones.

Just make the drone think its flying at an altitude of 100km and it will react by plowing itself into the ground

Re:unhackable....Challange accepted (1)

profplump (309017) | about 4 months ago | (#47082207)

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

"mathematically proven" (0)

Arancaytar (966377) | about 4 months ago | (#47082091)

What.

The only thing you can mathematically prove to be secure is the encryption, and strong crypto is the very least of what even a very cheap commercial drone should have.

Re:"mathematically proven" (0)

Anonymous Coward | about 4 months ago | (#47082139)

Actually, encryption can never be mathematically proven. There are no one-way functions, however, there are near impossible to reverse functions given our current knowledge of mathematics.

Re:"mathematically proven" (0)

Anonymous Coward | about 4 months ago | (#47082175)

Unless I'm mistaken, unconditional security (for now, only information theoretic security) is encryption that can be mathematically proven. It's just not generally used.

https://en.wikipedia.org/wiki/Information_theoretic_security

Re:"mathematically proven" (0)

Anonymous Coward | about 4 months ago | (#47084465)

If people here had a proper soviet or german education (yeah, both states have same drawbacks, essentially; other story), they would know about the OTP and they could reason that the OTP is actually feasible, given massive Flash chips.

But you know what ? Security-wise most people are about as intelligent as the one(!) japanese guy who devised the ciphers for their entire fleet. So the entirety of Japan was too dumb to use OTP ciphers like the Kiwis and American Britons did.

And yeah, Germans were not much better, but at least Enigmas and codebooks had to be captured for an entry.

That's the crypto side, which can be made perfect. The other side is code correctness (see the OpenSSL debacle). That can be done, too. See mathematical correctness proofs, L4 and the INRIA compiler efforts.

Finally, NSA-GCHQ will hate ALL of this, as it threatens their very existence. And NSA is connected to JCS and they have almost global reach, except for China and Russia. These have their own variants of a JCS and they don't want secure IT, either.

In other words: no way.

Re:"mathematically proven" (4, Funny)

arglebargle_xiv (2212710) | about 4 months ago | (#47082143)

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

Re:"mathematically proven" (2)

K. S. Kyosuke (729550) | about 4 months ago | (#47082369)

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

Re:"mathematically proven" (4, Informative)

DNS-and-BIND (461968) | about 4 months ago | (#47082517)

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" (3, Informative)

VortexCortex (1117377) | about 4 months ago | (#47082619)

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

Re:"mathematically proven" (0)

Anonymous Coward | about 4 months ago | (#47082609)

"Don't worry about the software implementation, we are outsourcing everything to India."

Re:"mathematically proven" (0)

Anonymous Coward | about 4 months ago | (#47082173)

Much more can be proven about a program, given extremely time consuming tedious effort.

https://en.wikipedia.org/wiki/Formal_methods

Formally verified (1)

Anonymous Coward | about 4 months ago | (#47085673)

By "mathematically proven" the article means "formally verified [wikipedia.org] " 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/ [smaccmpilot.org]

This is just silly (3, Insightful)

rebelwarlock (1319465) | about 4 months ago | (#47082095)

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 (0)

Anonymous Coward | about 4 months ago | (#47082123)

Formal methods are capable of much more than you imply. They are, however, extremely time consuming and generally not used for non-critical applications.

https://en.wikipedia.org/wiki/Formal_methods

This is just silly (4, Insightful)

craigminah (1885846) | about 4 months ago | (#47082125)

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:This is just silly (1)

VortexCortex (1117377) | about 4 months ago | (#47082635)

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 (1)

Anonymous Coward | about 4 months ago | (#47082737)

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 (0)

Anonymous Coward | about 4 months ago | (#47082837)

What I'm guessing they mean by mathematically proven is hardware verification or formalization. This means that the electronics are formalized into a logical system and analyzed by a proof-checker like Isabelle or HOL.

Re:This is just silly (1)

LordLimecat (1103839) | about 4 months ago | (#47083025)

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

Re:This is just silly (0)

Anonymous Coward | about 4 months ago | (#47084669)

Other things need to be either protected or assumed to be hackable. For example, you gain little by tightly locking the comms subsystem but having an entry through the automatic gain control software of the camera, which (transitively) allows for subverting the entire drone.

Or, whatabout the parser code of the GPS receivers ? Maybe lots of stuff against jamming, but no protection against protocol errors which enable an exploit. Or the AGC of the GPS receiver, can it be hacked ?

Whatabout those nice software-baed radars on the F22 and the F35. Are you sure nobody can fuck with those ? And if possible, are we sure the aircraft cannot be crashed in some sort of radar-based terrain following mode ? Ah, you use LANTIRN / infrared for terrain followiung. Are you sure LANTIRN code cannot be hacked with a $300 Laptop and a $3 laser pointer plus a $5 parallel cable and a 0.1$ transistor ?

Re:This is just silly (2)

AmiMoJo (196126) | about 4 months ago | (#47082187)

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 (0)

Anonymous Coward | about 4 months ago | (#47082443)

You don't get bonus points because you thought about security where weapons were concerned. That's like bragging about not shitting your pants.

Hardware, not software, but I suggest you never read Command & Control. It goes into some detail about the US military's ideas on the importance of securing nuclear weapons against theft, damage, accidental detonation...

Re:This is just silly (1)

PPH (736903) | about 4 months ago | (#47082951)

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

They load the software from 8 inch floppy disks.

You, Sir (0)

Anonymous Coward | about 4 months ago | (#47084503)

...are obviously clueless about the inner workings of ANY business, including the arms business. Cheap and quick wins ANY TIME over ANY THING. That is why they have complex manual procedures for things like nuclear weapons launch.

And sure as hell you will find lots of military officers who will know and accept this state of affairs. They will tell you that short time to delivery beats perfection. They will also say that "being affordable" is more important than "maximum quality".

Then there are the infantery captains and seagreants who assume their electronic gear is flawless. But they are not supposed to know reality.

aren't all drones designed to be hack resistant? (3)

Punto (100573) | about 4 months ago | (#47082155)

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:aren't all drones designed to be hack resistant (1)

Anonymous Coward | about 4 months ago | (#47082309)

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/

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

K. S. Kyosuke (729550) | about 4 months ago | (#47082431)

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.

Nice Dice. (1)

nospam007 (722110) | about 4 months ago | (#47082159)

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

AGAIN!

Re:Nice Dice. (0)

Anonymous Coward | about 4 months ago | (#47082285)

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

AGAIN!

I heard it was taken over by a secure drone.

Nice hack. So much for that resistant claim.

Re:Nice Dice. (1)

sound+vision (884283) | about 4 months ago | (#47083861)

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 (1)

Anonymous Coward | about 4 months ago | (#47082169)

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

Re:hehe (0)

Anonymous Coward | about 4 months ago | (#47082349)

Expose it to internet and make hacking contest, nice price for first to penetrate it

- I'm sure Iran is already doing this.

Perhaps... (1)

LongearedBat (1665481) | about 4 months ago | (#47082179)

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

Re:Perhaps... (1)

camperdave (969942) | about 4 months ago | (#47083031)

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

Publish the code (1)

throx (42621) | about 4 months ago | (#47082201)

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?

DARPA does do open source (0)

Anonymous Coward | about 4 months ago | (#47082717)

Most likely, they will open source the code. Most DARPA contracts have the provision that all your code will be open source; prevents the "government limited use license" problem, if nothing else. And, further, DARPA well understands that security comes from good design, not through obscurity.

Note though, that open source does NOT mean "not export controlled", so it might be "open to U.S. Persons" but that's still a lot of eyeballs.

Re:Publish the code (1)

Yaur (1069446) | about 4 months ago | (#47083797)

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

Mathematically proven? (0)

Anonymous Coward | about 4 months ago | (#47082203)

The article is light on detail. Wonder if they are using langsec?

Skynet? (0)

Anonymous Coward | about 4 months ago | (#47082223)

Could it be?

False security. (0)

Anonymous Coward | about 4 months ago | (#47082229)

n/t

Hackem' ??? (1)

tomhath (637240) | about 4 months ago | (#47082307)

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

At least they have a sense of humor.

Re:Hackem' ??? (1)

K. S. Kyosuke (729550) | about 4 months ago | (#47082437)

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

Re:Hackem' ??? (1)

drinkypoo (153816) | about 4 months ago | (#47082827)

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

found the key (1)

cellocgw (617879) | about 4 months ago | (#47082343)

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.

To quote the bard (1)

woboyle (1044168) | about 4 months ago | (#47082423)

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 (2)

VortexCortex (1117377) | about 4 months ago | (#47082831)

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 broke don't fix it), and now we have exponentially more CPU cycles compared to decades past so the inclusion of hash-table based maps is actually a bit moot at this point. So, the "academically provably correct" decision was actually detrimental in practical terms. They'd have had hast-tables in the STL long ago then we could have avoided a needles chunk of legacy maintenance headache.

In other words: The rule of thumb is: Rarely does any rule govern all thumbs. Common wisdom has typically been foolishly dumbed down. The wise avoid speaking in absolutist terms, there are almost always exceptions. While it's true that showing off the code would allow us to vet whether or not the code is secure, we're likely to miss at least some bugs anyway. It would be equally reassuring to have it vetted by a 3rd party and to listen to their B.S. saying it's secure... Time is a good test too, in practice. It would be prudent to proceed with caution; However, note that the current drones aren't very secure. You can crash them via jammer and tune into their video feed with your old school TV set, so any obscurity at all -- even an XORing everything with a single constant byte value -- would be better than the security we've currently got.

Note, they'd be correct in saying even just a constant-byte value XOR was "hack resistant" in "academically provably correct" terms, which is why one should typically expect BS.

Re:To quote the bard (0)

Anonymous Coward | about 4 months ago | (#47084487)

"Each stage of unknown cipher adds a few more bits of security in the selection of that cipher."

The point of a key is that it's unique. The algorithm isn't unique because it's shared by all the implementations, even if the algorithm isn't widely known. Which means an obfuscated chaining scheme doesn't actually add anything to the integrity of the system. You're just playing word games without understanding the meaning of the words.

And hash maps are security issues because of computational complexity attacks. Unless you use a randomized one-way hash seeded with a CSPRNG on every process startup, then it becomes a vector for denial of service attacks. People who blindly use hash tables because they're asymptotically O(1) are idiots. You use hash maps because you've already used a tree, proven that it's a bottleneck, have access to a safe hash library (or can prove that values to be hashed cannot be influenced from the outside), and are prepared to deal with out-of-memory errors when resizing the map (something which doesn't happen with a well designed trees, because the node should have been allocated with the element. I prefer trees because in complex algorithms utilizing multiple different trees and lists I can proof that they will come to completion without hitting any resource limitations, greatly simplifying error paths and resulting in cleaner, safer code).

All your bloviating tells me that you understand just enough of the concepts to be extremely dangerous, and not enough to understand the limitations of your knowledge which lead you to false conclusions.

Re:To quote the bard (0)

Anonymous Coward | about 4 months ago | (#47084501)

Also, your key extension theory is false. As a very basic example, let's say you chained ROT13, so that you performed ROT13 twice. What's the result? Plaintext.

If you chain different ciphers you have to prove that there's no underlying mathematical structures that interacts poorly when combined. Also, you forgot about things like side channel attacks that your little scheme could easily open up.

You clearly have no idea what you're talking about.

Don't hack my drone. (0)

Anonymous Coward | about 4 months ago | (#47082475)

That is great news if you have these drones you want to drop bombs on the heads of people and that they can't hack navigation of drones to drop bombs on your head is good news... it makes sense.

challenge acepted (0)

Anonymous Coward | about 4 months ago | (#47082561)

and from the headline factory that brought you "uncrashable car" and "unsinkable ship" comes....

Yeah, but what if you have the override device? (0)

Anonymous Coward | about 4 months ago | (#47082695)

10 drones at once! NOW!

Typical government/military software (0)

Anonymous Coward | about 4 months ago | (#47082721)

Hacked together out of open source components by people of varying abilities without regard to the licenses - because shooting someone with it isn't "distributing" the software.

Before you criticize... (0)

Anonymous Coward | about 4 months ago | (#47083103)

What they are probably saying is that they have formally proven that the software to be "correct," in operation- meaning it is mathematically proven to operate according to the defined requirements and has no side effects. This can be taken even further to mathematically prove that the software is free of commonly exploited vulnerabilities, such as buffer overflows, uninitialized variables, etc...

You can do this with tools like SPARK (an Ada dialect), or Frama-C. Typically functional languages are even more amenable to formal provability, but AFAIK, there are no functional languages that are suitable for hard realtime functionality.

So yeah, before you poo-poo the article, just realize that DARPA tends to do some pretty groundbreaking research and is generally far ahead of the curve set by the consumer/commercial world in these things.

Seriously people? (3, Interesting)

Typical Slashdotter (2848579) | about 4 months ago | (#47083591)

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 [wikipedia.org] is and reject that it is even possible is...disturbing. (See CompCert [inria.fr] 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? (1)

Anonymous Coward | about 4 months ago | (#47085017)

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? (1)

Anonymous Coward | about 4 months ago | (#47083781)

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.

I could tell you... (0)

Anonymous Coward | about 4 months ago | (#47084037)

" It would be interesting to know the CPU architecture, chipset, programming language and the suite of communication protol this thing uses .""

I could tell but then I'd have to kill you. Looking forward to your email.

"unveiled a new drone..." (1)

buybuydandavis (644487) | about 4 months ago | (#47084257)

"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 (1)

rossdee (243626) | about 4 months ago | (#47084399)

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

Re:Security of drones (0)

Anonymous Coward | about 4 months ago | (#47086291)

Hate to tell you that you can couple in an electromagnetic signal FROM BEHIND a dish-type directional antenna. Just use 1000Watt instead of 1 Watt. See the antenna gain charts.

Plus, you can always fly your trusted Mig25 above the drone and get the proper angle.

Mathematically proven... (1)

NonSenseAgency (1759800) | about 4 months ago | (#47084489)

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 (1)

nurb432 (527695) | about 4 months ago | (#47084575)

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.

TRANSEC can provide anti-spoofing (0)

Anonymous Coward | about 4 months ago | (#47085649)

Transmission Security via a time- or data count based pseudorandom number attached to each radio communication with the drone can provide anti-spoofing. The spoofer would have to provide messages including the just right 128 or 256 bit number, which changes for every message, or the drone would reject it. The pseudorandom number generator can be based on an initial "seed" that forms a kind of key, like a 128 or 256 bit encryption key, loaded before the drone takes off. This mechanism is quite robust because the spoofer's radio messages trying to gain control of the drone would be detected and rejected while the drone accepts legitimate messages. Perhaps earlier drones failed to have this mechanism?

E-bomb proof? (1)

Jim Sadler (3430529) | about 4 months ago | (#47085825)

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.

It has been possible for some time (0)

Anonymous Coward | about 4 months ago | (#47086181)

Given that the US DoD has an Ada Mandate, and their phrasing, I would not be surprised if they have used SPARK (https://en.wikipedia.org/wiki/SPARK_%28programming_language%29)

Load More Comments
Slashdot Login

Need an Account?

Forgot your password?

Submission Text Formatting Tips

We support a small subset of HTML, namely these tags:

  • b
  • i
  • p
  • br
  • a
  • ol
  • ul
  • li
  • dl
  • dt
  • dd
  • em
  • strong
  • tt
  • blockquote
  • div
  • quote
  • ecode

"ecode" can be used for code snippets, for example:

<ecode>    while(1) { do_something(); } </ecode>