Security breaches have become a daily fact of life in the Digital Age, and large-scale attacks can compromise millions of users’ personal information, as has happened at Equifax (143 million accounts), eBay (145 million), Facebook (up to 50 million in September), and Yahoo, where 3 billion accounts were put at risk. The important role of the Internet in national infrastructure, including the power grid, air-traffic-control systems, and financial networks, has made it the target of sophisticated attacks as well.
Digital security break-ins cost approximately $109 billion in the United States in 2016, and are estimated to cost between $375 billion and $575 billion per year worldwide. Small wonder that governments and industry are committing enormous resources to gain the upper hand in the data-theft wars. Often, such entities work with university researchers like Tevfik Bultan and Giovanni Vigna. Part of a formidable group of professors in the Computer Science Department at UC Santa Barbara’s College of Engineering, they take complementary approaches to security work.
Bultan’s approach reflects what he describes on his Verification Laboratory (VLab) website as “an ongoing shift in focus from performance to dependability,” reflecting the fact that “the size and complexity of the software systems nowadays inevitably lead to errors during both design and implementation phases” — errors that can cause vulnerabilities that compromise data.
He works primarily on two main security fronts: automating the process of finding vulnerabilities in software and trying to develop hackproof software by proving that it has no vulnerabilities.Vigna comes at security from the opposite perspective, seeking to find and exploit vulnerabilities in applications before they are deployed. Both share the goal of enabling programmers to make their products more secure.
“I think Tevfik works more on making sure that a program cannot misbehave, while we look for ways to make a program misbehave,” Vigna says. “He wants to be able to prove that bad things can’t happen. It’s like going back to the origins of software engineering, where you have formal verification and you say, ‘I’m going to prove that when the elevator door is open, there is no way that an elevator car will not be in front of the door.’ We’re more on the hacker side, saying, ‘How can we screw up this elevator?’ But sometimes Tevfik does what we do, and sometimes we do what he does. The two approaches are closely related.”
Much of the work Bultan refers to as “finding exploits” is done manually, but he prefers to automate the time-consuming process of identifying vulnerabilities by taking what is called a formal-methods approach. “We extract a math-based formal-logic representation of the software and then build logic solvers — software that can analyze the logic formulas,” he explains.
In application, the importance of his formal-methods work is reflected in a pair of grants he received recently — one from Amazon and another from the National Science Foundation — to address security issues with cloud computing services such as Amazon Web Services, Inc.
One problem is that when companies put their data onto Amazon’s cloud servers, they have to set the access rights appropriately so that other cloud users can’t access their company data. But the rights aren’t always set up correctly, and data gets exposed. To add security, Amazon developed its own language so that companies have to write their access specifications in that language, but people still make errors that can give rise to vulnerabilities.
Amazon then used an approach called differential analysis, which Bultan had described in a journal article a decade earlier, to build an automated checker, called Zelkova, to determine whether access rights were set up correctly. Zelkova is good at reasoning about numbers but not as good at reasoning about text, called strings in the computing field, which are necessary in data-rights policies that, for instance, include people’s names.
String analysis is a fledgling area of research, and Bultan has co-authored the first book on the subject, String Analysis for Software Verification and Security (Springer, 2017). The Amazon and NSF research grants he re-ceived will enable him to extend his work on string analysis so that tools like Zelkova can become more effective in analyzing access policies.
“This is a great example of formal-methods techniques being applied in practice from the security perspective,” Bultan says. “It is nice to see industry build a formal-methods tool that is having a practical impact and was significantly influenced by the research we do here at VLab.”
Vigna’s work, too, finds abundant application in the world beyond academia, often for the Defense Advanced Research Projects Agency (DARPA), the Office of Naval Research, or the Army Research Office. In a recent $11.7 million DARPA grant, the lead PI, Fish Wang, an alumnus of the UCSB SecLab (run by Vigna and fellow Computer Science professors Christopher Kruegel and Dick Kemmer), and the five other co-PIs at the collaborating universities — four of whom also earned their PhDs in Vigna’s lab and one who worked as a postdoctoral researcher there — are pursuing what Vigna describes as “a new frontier in security and vulnerability analysis.”
He says that the basic idea of the project, called Computers and Humans Exploring Software Security (CHESS), is “to create a cyber system that can reason about a program. But it should also recognize when it encounters an obstacle that requires human intervention, and should be able to collect, in an intelligent way, those cognitive tasks that humans do better than machines do. It’s a changing perspective with respect to what can the automated and what can be orchestrated.”
According to the CHESS website, “The process requires hundreds, if not thousands, of hours of manual effort per discovered vulnerability.” Further, “Automated program analysis capabilities…cannot address the majority of vulnerabilities. CHESS aims to develop capabilities to discover and address vulnerabilities in a scalable, timely, and consistent manner.”
To summarize, Vigna says, “The programs are not yet smart enough.” The paradigm shift, until that changes, is to bring in humans on an ad hoc basis to bypass the problem and then give control back to the AI.
It’s called artificial artificial intelligence — AI with human helpers. Amazon has a simple version of it, called Mechanical Turk. The web-based service allows anyone to post a task that a machine cannot do, and then anybody in the world can choose that task and get paid a small amount for doing it.
But while Mechanical Turk simply provides a mechanism for humans to ask other humans to carry out a simple task, says Vigna, “Our system is able to carry out a security analysis, identify a situation in which the analysis is stalling, and ask for targeted help from a human to overcome the obstacle.” It’s a machine asking for human assistance.
Vigna, who directs the Center for CyberSecurity at UCSB (the website for which describes the “abysmal” state of security on the Internet), has also worked extensivly on smart-phone security.
“People don’t realize how much trust they put in their phones,” he says. “For instance, we trust the market and assume that when we download something from Google, we won’t be infected, but that’s not always the case. And there are applications that you trust will not grab something from the Internet and put it on your phone. But it gets done all the time. So we studied that, trying to look at the whole smartphone ecosystem to understand what the problems are.”
Vigna’s lab has also examined the many aspects of what he calls the “underground economy” of the Internet — people who try to sell users fake antivirus programs that actually infect computers, extortion schemes, laundering money via shipping mules, and the like.
Bultan, Vigna, and other computer-security experts know that, while cyberspace can seem like the Wild West, there is one simple step that all of us can take to protect ourselves, and that is to use two-factor authentication on all our devices. That single action, Vigna says, will eliminate more than ninety percent of account compromises — and avoid the need for an expert to restore order in your digital world.