DARPA Unveils Hack-Resistant Drone 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 ."
Frosty piss (Score:2, Insightful)
Re:Frosty piss (Score:5, Insightful)
Yep, I especially loved this gem from the summary:
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: (Score:3)
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
Re: (Score:3)
"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!
Re: (Score:2)
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: (Score:1)
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 mo
Re: (Score:1)
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 desig
Re: (Score:2)
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
Re: (Score:1)
Re: (Score:1)
Well they did say invulnerable to large classes of attack, which already means that it's not "invulnerable" to all attacks.
How long (Score:5, Insightful)
Re: (Score:1)
Re: (Score:1)
Re: (Score:2)
Land the drones (Score:2)
Re: (Score:1)
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: (Score:2)
Many systems designed to be idiot-proof fail because they just keep making a better idiot.
Re: (Score:2)
This is DARPA we're talking about.
One does not simply out smart DARPA.
Scary (Score:1)
Either they're 50 years behind missile tech, or the abort signal of missiles can be hacked.
Re: (Score:2)
If only there was some sort of completely internal guidance system available for aircraft.
"mathematically proven" (Score:1)
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" (Score:5, Funny)
Re: (Score:3)
Re:"mathematically proven" (Score:5, Informative)
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" (Score:4, Informative)
"To determine who really rules, all you hafta do is ask: Who am I not allowed to misquote?"
- Voltaire
Formally verified (Score:1)
This is just silly (Score:4, Insightful)
Comment removed (Score:5, Insightful)
Re: (Score:2)
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: (Score:1)
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
Re: (Score:2)
'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: (Score:3)
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: (Score:2)
the US military's ideas on the importance of securing nuclear weapons
They load the software from 8 inch floppy disks.
aren't all drones designed to be hack resistant? (Score:4)
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: (Score:1)
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: (Score:2)
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. (Score:2)
Your Security Certificate ran out and nobody could be bothered to renew it.
AGAIN!
Re: (Score:2)
hehe (Score:1)
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... (Score:2)
Re: (Score:2)
Publish the code (Score:2)
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: (Score:2)
Hackem' ??? (Score:2)
The program, called High Assurance Cyber Military Systems, or HACMS
At least they have a sense of humor.
Re: (Score:2)
Re: (Score:2)
Or, obviously, hack microsoft. It's running Windows for Drones.
found the key (Score:2)
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 (Score:2)
Re: (Score:3)
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 n
Seriously people? (Score:4, Interesting)
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: (Score:1)
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? (Score:1)
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..." (Score:2)
"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 (Score:2)
The first thing I would do is have directional antennas and only accept commands from above (ie satellites)
Mathematically proven... (Score:2)
If it can be remotely controlled (Score:2)
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.
E-bomb proof? (Score:2)
Hacker Resistant Drone? (Score:2)