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 is a Professor in and the Chair of the Computer Science Department at Tufts. Previously, she was a program manager at DARPA where she started and managed the HACMS and PPAML programs, a Consulting Faculty Member in the Computer Science Department at Stanford University, and a Principal Member of the Technical Staff at AT&T Labs Research. Kathleen's research focuses on advancing the theory and practice of programming languages and on applying ideas from the programming language community to the problem of ad hoc data management. The main thrust of her work has been in domain-specific languages to facilitate programming with massive amounts of ad hoc data. Recently, she has been exploring synergies between machine learning and programming languages and studying how to apply advances in programming languages to the problem of building more secure systems.
Kathleen is an ACM Fellow. She has served as Program Chair for OOPSLA ICFP, CUFP, and FOOL, and as General Chair for ICFP 2015. She is an Associate Editor for TOPLAS and a former editor of the Journal of Functional Programming. Kathleen is a past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN) and past Co-Chair of CRA's Committee on the Status of Women (CRA-W). Kathleen is a recipient of the SIGPLAN Distinguished Service Award. She is Vice Chair of DARPA's ISAT Study Group and a member of the Board of Trustees of Harvey Mudd College.
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.
"They" has taken on a not-so-new meaning lately. This earned it the scrutiny it needed to win.
- Merriam-Webster has announced "they" as the word of the year.
- The selection was based on a marked increase in traffic to the online dictionary page.
- Runners up included "quid pro quo" and "crawdad."
A review of the global "wall" that divides rich from poor.
- Trump's border wall is only one puzzle piece of a global picture.
- Similar anxieties are raising similar border defenses elsewhere.
- This map shows how, as a result, "the West" is in fact one large gated community.
Facebook's misinformation isn't just a threat to democracy. It's endangering lives.
- Facebook and Instagram users have been inundated with misleading ads about medication that prevents the transmission of HIV (PrEP), such as Truvada.
- Over the years, Facebook's hands-off ad policy has faced scrutiny when it comes to false or ambiguous information in its political ads.
- Unregulated "surveillance capitalism" commodifies people's personal information and makes them vulnerable to sometimes misleading ads.
LGBT groups are saying that Facebook is endangering lives by advertising misleading medical information pertaining to HIV patients.
The tech giant's laissez-faire ad policy has already been accused of threatening democracy by providing a platform for false political ads, and now policy could be fostering a major public-health concern.
LGBT groups take on Facebook’s ad policy
According to LGBT advocates, for the past six months Facebook and Instagram users have been inundated with misleading ads about medication that prevents the transmission of HIV (PrEP), such as Truvada. The ads, which The Washington Post reports appear to have been purchased by personal-injury lawyers, claim that these medications threaten patients with serious side effects. According to LGBT organizations led by GLAAD, the ads have left some patients who are potentially at risk of contracting HIV scared to take preventative drugs, even though health officials and federal regulators say the drugs are safe.
LGBT groups like GLAAD, which regularly advises Facebook on LGBT issues, reached out to the company to have the ads taken down, saying they are false. Yet, the tech titan has refused to remove the content claiming that the ads fall within the parameters of its policy. Facebook spokeswoman Devon Kearns told The Post that the ads had not been rated false by independent fact-checkers, which include the Associated Press. But others are saying that Facebook's controversial approach to ads is creating a public-health crisis.
In an open letter to Facebook sent on Monday, GLAAD joined over 50 well-known LGBTQ groups including the Human Rights Campaign, the American Academy of HIV Medicine and the National Coalition for LGBT Health to publicly condemn the company for putting "real people's lives in imminent danger" by "convincing at-risk individuals to avoid PrEP, invariably leading to avoidable HIV infections."
What Facebook’s policy risks
Of course, this is not the first time Facebook's policy has faced scrutiny when it comes to false or ambiguous information in its ads. Social media has been both a catalyst and conduit for the rapid-fire spread of misinformation to the world wide web. As lawmakers struggle to enforce order to cyberspace and its creations, Facebook has become a symbol of the threat the internet poses to our institutions and to public safety. For example, the company has refused to take down 2020 election ads, largely funded by the Trump campaign, that spew false information. For this reason, Facebook and other social media platforms present a serious risk to a fundamental necessity of American democracy, public access to truth.
But this latest scandal underlines how the misconstrued information that plagues the web can infect other, more intimate aspects of American lives. Facebook's handling of paid-for claims about the potential health risks of taking Truvada and other HIV medications threatens lives.
"Almost immediately we started hearing reports from front-line PrEP prescribers, clinics and public health officials around the country, saying we're beginning to hear from potential clients that they're scared of trying Truvada because they're seeing all these ads on their Facebook and Instagram feeds," said Peter Staley, a long-time AIDS activist who works with the PrEP4All Collaboration, to The Post.
Unregulated Surveillance Capitalism
To be fair, the distinction between true and false information can be muddy territory. Personal injury lawyers who represent HIV patients claim that the numbers show that the potential risks of medications such as Turvada and others that contain the ingredient antiretroviral tenofovir may exist. This is particularly of note when the medication is used as a treatment for those that already have HIV rather than prevention for those that do not. But the life-saving potential of the HIV medications are unequivocally real. The problem, as some LGBT advocates are claiming, is that the ads lacked vital nuance.
It also should be pointed out that Facebook has taken action against anti-vaccine content and other ads that pose threats to users. Still, the company's dubious policies clearly pose a big problem, and it has shown no signs of adjusting. But perhaps the underlying issue is the failure to regulate what social psychologist Shoshana Zuboff calls "surveillance capitalism" by which people's experiences, personal information, and characteristics become commodities. In this case, paid-for personal-injury legal ads that target users with certain, undisclosed characteristics. It's been said that you should be wary of what you get for free, because it means you've become the product. Facebook, after all, is a business with an end goal to maximize profits.
But why does a company have this kind of power over our lives? Americans and their legislators are ensnared in an existential predicament. Figure out how to regulate Facebook and be accused with endangering free speech, or leave the cyber business alone and risk the public's health going up for sale along with its government.