Claire Corlett

Fish Food, Fish Tanks, and More
How coders are creating software that’s impossible to hack | Kathleen Fisher

How coders are creating software that’s impossible to hack | Kathleen Fisher

HACMS is a program at DARPA that ran for four-and-a-half
years that was focused on using techniques from what is called the ‘formal methods community’,
so techniques based on math more or less, to produce software for vehicles that came
with proofs that the software had certain desirable properties; that parts of it were
functionally correct, that there were no certain kinds of bugs in the software. And the consequence of those proofs is that
the system is much harder to hack into. So the formal methods community has been promising
for, like, 50 years that they could produce software that provably didn’t have certain
kind of vulnerabilities. And for more or less 50 years they have failed
to deliver on that promise. Yes, they could produce proofs of correctness
for code but for ten lines of code or 100 lines of code—not enough code to make a
difference for any kind of practical purpose. But recently there have been advances in a
bunch of different research areas that have changed that equation, and so now formal methods
researchers can prove important properties about code bases that are 10,000 or 100,000
lines of code. And that’s still small potatoes compared
to the size of Microsoft Windows or the size of Linux which are millions, hundreds of millions
of lines of code. But when you start to get to 10,000 or 100,000
lines of code there are really interesting software artifacts that fit in that size. Things like compilers and microkernels, and
you can leverage those kinds of exquisite artifacts to build much more complex software
systems where only a small part of the system has to be verified to be functionally correct,
and then you can have lots of software running on top of it that doesn’t have that same
level of assurance associated with it but that you can prove: it doesn’t matter what
it does, it’s not going to affect the operation of the overall system. So, for example, HACMS researchers used the
high-assurance code and put it on a Boeing Unmanned Little Bird which is a helicopter
that can fly completely autonomously or it can fly with two pilots. And this helicopter has two computers on it:
one is the mission control computer that controls things like ‘fly over there and take a picture’
or ‘fly over there and take a picture’, and communicate to the ground station or the operator
who’s telling the helicopter what to do. It also has a flight control computer that
controls things like altitude hold and stability, sort of the mechanics of flying the helicopter
at any given time period. So the researchers put seL4 microkernel, which
is a verified microkernel guaranteed to be functionally correct, on the mission control
computer, and they used it to create different software partitions. So one of those partitions was responsible
for communicating with the ground station. Another one of those partitions was responsible
for operating the camera that the helicopter had. The researchers verified that the code in
the ‘communicate with the ground station’ was functionally correct and isolated from
the software in the ‘control the camera’ part. So the camera part was all the legacy software
that had previously been on the helicopter to control camera operation. They allowed the red team to additionally
put—the red team is a group of people who are charged with trying to take over control
of the helicopter against the wishes of the legitimate operator—so they’re trying
to hack in, take over control, disrupt the operation of the helicopter. So in this setting, the red team was allowed
to have root access, so unfettered access within the camera partition, and was charged
with: break out of this, take over control of the rest of the helicopter, disrupt the
operation of the helicopter in any way, corrupt the messages to the ground station—basically
interfere in any way you can with the legitimate operation of this helicopter. The red team had full access to the source
code. They understood all the design documents. They knew as much about the system as you
could reasonably expect to know. And after six weeks they were not able to
break out. They were not able to disrupt the operation
of the copter at all. All they could do was they could fork-bomb
themselves. They could basically crash their own process
but the rest of the helicopter would then notice that that process was crashed and restart
it again, restoring the operation of the camera. So that’s an example of where you could
use the formal methods-based techniques to create this kind of thin level at the bottom,
which was the seL4 microkernel, and then leverage that to produce the full functionality of
the helicopter. The camera functionality might come and go
as hackers break in or don’t break in but you’re guaranteed that the helicopter will
be still able to communicate to the ground station and fly appropriately.

86 comments on “How coders are creating software that’s impossible to hack | Kathleen Fisher

  1. Whenever someone talks to me about "hacking", I ask them to define hacking.

    The answer is typically either vague or nonsensical.

  2. This seems like something that will become more and more important as time goes on, especially as we put more and more of our identities and personal information into the form of computer data and utilize more and more autonomous vehicles. This also reminds me very much of Quantstamp who tries to algorithmically verify the security of ICOs, but I'm fairly non-technical so I could be wrong on that. Godspeed anti-hacker hackers! The world needs you!

  3. Unhackable = Impossible. This is just propaganda. Unless it works at the quantum level where uncertainty is a fundamental part of the coding, there is no such thing as an unhackable code.

  4. This was so technical I really don’t see how someone without any programming/ coding experience would understand the significance of this. Thanks for sharing!

  5. If you want to prove the correctness of your programs, simply program in Haskell. Basically proven as you write it.

  6. There is no software that "impossible to hack", that's just stupid to say.Computers are based on math,logic.If you say that you have created an impenetrable software system you're basically claiming to have achieved some kind of perfection,which i'm pretty sure you haven't.
    Just because you have a little helicopter running around with a system that has very few vectors of attack doesn't mean it is impenetrable.Also i'm pretty sure DARPA doesn't have around the best hackers on the planet, and even if they did that doesn't prove that your software is perfect.

  7. Will Facebook ever be hacker/ virus proof? Not likely, right? Hackers will always find a way to mutate any software security system,. I'm afraid. Why they do it maybe only they understand. The hackers are smart and stupid at the same time.

  8. Functional programming had been around since the 1930s, too bad programmers favor ease of use over correctness and immutability even when dealing with mission-critical systems.

  9. That's great, but what if the copter's software was quantum? Could this 'formal methods' people then prove that the copter isn't in a superposition of being and not being hacked? XD

  10. It's very easy to hack. Just wait for someone to leave their computer unattended and unlocked; post on their Facebook something silly. You are a certified hacker now.

  11. Hacking software isnt the main problem. People hack information and networks. Its your protocols that need updating and how information is sent and received. Just because your banking software, your OS, cant be hacked doesnt mean i cant just take the information as it travels across a network and what are you going to do if i have physical access to the device itself? If i can touch the device with my hands there is no way you are going to be able to secure it. That is security 101 you learn about that in first semester.

    All this will do is make it so gaming software and entertainment more secure. Congrats you protected a billion dollar industry, meanwhile millions of poor people are getting their information stolen and sold. Come on man…

  12. Oh yeah put anti-hacking/hacking-proof software on helicopters that can fly themselves at the same time you are developing real AI for the first time……What could go wrong?

    Instead of testing the software on helicopters, why cant we test it on a smart device that is connected to a network with (x) amount of processing power like a smart washer or TV……Those things are not only cheaper but they wont kill you when the military installs AI without telling you during one of it's 'tests'.

  13. "Hackers can't hack this because X!"
    Have you read the history of almost any software that had the intention to lockout hackers?
    "Oh Hackers can't hack the DVD because- oh wait they hacked it. Well they can't hack this– oh.."
    For a Big Think video this is weirdly ignorant.

  14. if you were a genius who could write a unique set of codes for your own usages and you didn't share it to anybody.

  15. This is very interesting. I haven't looked at the proofs, but if you think that security provided by modern cryptography hinges on the difficulty of certain mathematical problems, such as integer factorization and the discrete logarithm problem, then it's not impossible to imagine having similar assurances for small pieces of code that are critical to operation of a system. It remains to be seen how bulletproof they are and if mathematicians can find a weakness.

    Here's what it seems to be the paper:

  16. we need a computer to check the computer that makes sure the computer is doing the right thing, and then a group of people constantly checking that the checking computer is checking correctly, those people checking the checking computer need better computers.

    unhackable that should not be a word.

  17. she mentioned microkernel partitions. of course, *nix systems are monolithic. so i wonder, what OS was this helicopter using? HURD??

  18. One very important near term possible use, which I believe would fit the size limit. Solidity smart contracts (Ethereum).

  19. If a movie can be viewed, it can be copied. If music can be heard, it can be recorded. If a machine runs software, it can be hacked. It's only a question of time and diligence.

  20. It's easy to defend against known vulnerabilities. In fact, if you don't, you're a lazy programmer. It's not so easy to defend against unknown vulnerabilities. In the sense that you're using the word "hacking" that's the problem. So you defended 100k lines of code for 6 weeks? That's awesome, but most major programs are millions of lines of code.

    I'm sure we're all (those of us with a formal education in computer science) familiar with Greenspun's tenth rule of programming. One of my professor's was quite fond of reminding us about it. The idea is that any sufficiently complicated program has bugs. You reminded us many times that you can defend your technique with formal mathematics, but the same is true of my rebuttal.

    I'm sure the code you tested is locked up as tight as alcatraz (and if I had to guess I'd bet it took an obtrusively long time to accomplish that), but if it's sufficiently complicated there are bugs you failed to account for. Bugs that will eventually be discovered with a sufficiently motivated individual.

    That's the problem with our technology. It's layers and layers of abstraction. You made a partition that serves as a lock, which allegedly can't be penetrated. That's not so easy with things like the Internet. Because of the layered nature, you only need to penetrate a specific layer. Locking them all would take inordinate amounts of man hours, and probably complicate the transfer process. This is a problem that will continue to get worse with time; not better.

    Awesome idea. I think I'm just too pragmatic to believe it would serve any general application though.

  21. This is not practical for real world application because it takes a long time to produce verified code and it is only a micro kernel. Now think about the Linux kernel or even a phone kernel.

  22. NSA can hack anything because they got the blueprints of all the OS's and they have money to buy the best hackers.

  23. Bollocks. What one Man created the other one will try to bypass it. That’s how it works especially in IT. So many times we heard of “non-breakable” secure stuff and it was hacked. Reverse engineering is the key… How will you bypass this?

  24. You can hack everything that you can somehow connect to. To say something is "impossible to hack" is just bullshit. And yes when you have acess to a seperate System you can`t hack one that isn`t connected to this but you wouldn`t try it that way. You would try to attack the System that allows the ground to Control the helicopter or attack the way the helicopter communicates with the ground Control.

  25. as someone with a computer science degree can we agree to never use the word "coder", literally anything else is better. I work with code, yes, and dentists work with teeth, yet we don't call them toothers.

  26. It is time to apply formal methods to processor architecture, so that the CPU hardware is more robust. The vulnerability of speed optimizations is now laid bare.

  27. You know that 'hacking' is not going anywhere in the future because people that are 'protecting' us from the 'hacking' event don't say what hacking is…

  28. Nothing is as secure as she claims. It is just more secure than average, meaning as secure as most things should be at a minimum.

  29. I take it this was achieved to prevent an AGI uprising ^^ or will it be used so we wouldn't be able to hack AGI's which may turn out to be a flaw in itself -_-

  30. imo
    They proved that those "hackers" couldn't hack the system, not that all hackers won't be able to hack the system.
    It is entirely possible that there are better hackers out there.
    It is also possible that their testing was self serving in its outcome.
    Impossible is a big, carelessly used word.

Leave a Reply

Your email address will not be published. Required fields are marked *