Slashdot Mirror
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 ."
There ain't no such thing as 'hacker-resistant'.
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...
Religous speak to God. Insane are spoken to by God. When all shut up, one can finally hear Shostakovich in peace
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/
Beware the corrupt United States government, people..
Either they're 50 years behind missile tech, or the abort signal of missiles can be hacked.
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?
....to the latest 24 episodes
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
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.
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.
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...
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.
--
Stay tuned for some shock and awe coming right up after this messages!
Your Security Certificate ran out and nobody could be bothered to renew it.
AGAIN!
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 the computer is built using IC's, uses tape decks for storage and communicates via CB radio...?
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?
Fear: When you see B8 00 4C CD 21 and know what it means
The article is light on detail. Wonder if they are using langsec?
Could it be?
n/t
The program, called High Assurance Cyber Military Systems, or HACMS
At least they have a sense of humor.
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/
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.
https://app.box.com/WitthoftResume Code: https://github.com/cellocgw
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.
Sometimes, real fast is almost as good as real-time.
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.
Ezekiel 23:20
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.
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).
and from the headline factory that brought you "uncrashable car" and "unsinkable ship" comes....
10 drones at once! NOW!
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.
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.
The current season of 24 could be cut short if the US gov't simply landed the drones....
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.
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.
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.
" 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... 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.
The first thing I would do is have directional antennas and only accept commands from above (ie satellites)
...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.
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.
...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.
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.
---- Booth was a patriot ----
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?
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/
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.
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)
Full steam ahead, we'll be in New York for tiffin.
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.
-- 29A the number of the Beast
im pretty social engineering could find some good attack vectors for these "unhackable" drones..
and then when you cant hack the drone itself you hack its control structure.