Is there anything hackers can't hack? Now there is, thanks to a new way of coding.

Thanks to the beauty (and rigor) of formal mathematics, coders can now create hack-proof technology.

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.

Hackers thrive on human error, but a new method of coding is ending that. Recent developments by the HACMS (High-Assurance Cyber Military Systems) program at DARPA has allowed computer scientists to use mathematical proofs to verify that code—up to 100,000 lines of it at a time—is functionally correct and free of bugs. Kathleen Fisher, professor of computer science and former program manager at DARPA, explains how this allows coders to build a thin base of hyper-secure code that is 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." To illustrate this technology in the real world, Fisher tells the story of how this new method of coding defended a Boeing Little Bird helicopter from a "red team" of hackers charged with causing havoc in the system and bringing that baby down. So is there anything hackers can't hack? Now there is, thanks to the beauty (and rigor) of formal mathematics.


Compelling speakers do these 4 things every single time

The ability to speak clearly, succinctly, and powerfully is easier than you think

Former U.S. President Barack Obama speaks during a Democratic Congressional Campaign Committee rally at the Anaheim Convention Center on September 8, 2018 in Anaheim, California. (Photo by Barbara Davidson/Getty Images)
Personal Growth

The ability to communicate effectively can make or break a person's assessment of your intelligence, competence, and authenticity.

Keep reading Show less

Antimicrobial resistance is a growing threat to good health and well-being

Antimicrobial resistance is growing worldwide, rendering many "work horse" medicines ineffective. Without intervention, drug-resistant pathogens could lead to millions of deaths by 2050. Thankfully, companies like Pfizer are taking action.

Image courtesy of Pfizer.
Sponsored
  • Antimicrobial-resistant pathogens are one of the largest threats to global health today.
  • As we get older, our immune systems age, increasing our risk of life threatening infections. Without reliable antibiotics, life expectancy could decline for the first time in modern history.
  • If antibiotics become ineffective, common infections could result in hospitalization or even death. Life-saving interventions like cancer treatments and organ transplantation would become more difficult, more often resulting in death. Routine procedures would become hard to perform.
  • Without intervention, resistant pathogens could result in 10 million annual deaths by 2050.
  • By taking a multi-faceted approach—inclusive of adherence to good stewardship, surveillance and responsible manufacturing practices, as well as an emphasis on prevention and treatment—companies like Pfizer are fighting to help curb the spread.
Keep reading Show less

Preserving truth: How to confront and correct fake news

Journalism got a big wake up call in 2016. Can we be optimistic about the future of media?

Videos
  • "[T]o have a democracy that thrives and actually that manages to stay alive at all, you need regular citizens being able to get good, solid information," says Craig Newmark.
  • The only constructive way to deal with fake news? Support trustworthy media. In 2018, Newmark was announced as a major donor of two new media organizations, The City, which will report on New York City-area stories which may have otherwise gone unreported, and The Markup, which will report on technology.
  • Greater transparency of fact-checking within media organizations could help confront and correct fake news. Organizations already exist to make media more trustworthy — are we using them? There's The Trust Project, International Fact-Checkers Network, and Tech & Check.
Keep reading Show less