Montana State key player on $7 million contract for cybersecurity research

BOZEMAN - Montana State University researchers working to improve cybersecurity have won a major contract from the Defense Advanced Research Projects Agency that aims to automate threat assessment.

The contract is MSU's first cybersecurity project to receive funding from DARPA, which is the research arm of the U.S. Department of Defense. The $7.1 million, three-year contract was awarded to MSU's Harnessing Automation in Cybersecurity Reasoning Lab, also referred to as the HACR Lab, and the Virginia-based cybersecurity company Kudu Dynamics.

MSU will receive $780,000 to support the work of two graduate students in the HACR Lab, said Matt Revelle, the lab director and principal investigator on the contract. Revelle is also a computer science professor in MSU's Gianforte School of Computing, which is part of the Norm Asbjornson College of Engineering.

Funded by DARPA's Intelligent Generation of Tools for Security, or INGOTS, program, Revelle said the award boosts MSU's reputation and opens doors for students to be on the cutting edge of new research.

"It's kind of an endorsement that the university is capable of delivering what DARPA is looking for and will help MSU advance its reputation as a university that companies should target when recruiting cybersecurity experts," Revelle said.

The research could have significant impacts on cybersecurity and other fields. Broadly, the work seeks to better understand the impact of vulnerabilities in software and identify the vulnerabilities that are most severe.

A vulnerability is essentially a software bug that can be exploited by an attacker to do something they should not be able to do, such as access private information, Revelle said. Cybersecurity experts have honed ways to stop attackers from taking advantage of singular vulnerabilities. But a more difficult challenge is dealing with exploit chains, when attackers take advantage of the interplay between multiple vulnerabilities.

A cellphone is a good example of a system with multiple components, Revelle said. A phone has a primary processor running an operating system and software applications, along with a separate component handling cellular, Wi-Fi and Bluetooth connectivity.

"All of these things, they work together. So, if you find a vulnerability in one piece of that system, there might be something you can do to interact with another component of the system," Revelle said.

When that happens, this sequence of exploited vulnerabilities is called an exploit chain, and Revelle said these can be used to push a program or software into a state that it normally would never reach.

"And because you've done that, you've changed what the program can do in a small way," he said. "It's like you've rewritten the program, and you can use that rewrite to introduce a new vulnerability."

Historically, the threat posed by vulnerabilities has been rated with human-created scores that can be subjective. Revelle and his team are repurposing a process called formal verification to create a more objective assessment.

Formal verification is about proving the correctness of a computer system, Revelle said - it can be used to prove some aspect of the software, like "this program should never crash" or "this program should never read memory from an invalid location."

"Formal verification is normally used to prove some safety or security property about a program," Revelle said. "But what we're using formal verification to do is actually prove what can be done with some vulnerability."

That way, the researchers can stay one step ahead of attackers by better understanding the impacts of different bugs.

They are doing that by building a framework in Lean, a programming language and proof assistant tool. The framework, named Quarry, allows researchers to describe exploit techniques and prove whether the software being analyzed is susceptible to a related attack.

While Lean provides a powerful platform for automating this approach, the team is also extending this automation with the inclusion of large language models (LLMs) through an AI agent to help with discovering exploits. This would enable a powerful feedback loop where the AI agent can automatically generate proof fragments and the proof assistant can recognize when the AI agent has made a nonsensical suggestion.

"If we had the ability to take a piece of software and a vulnerability and then check to see all the different ways that vulnerability could be used to construct an exploit chain, it could be very useful," Revelle said. "It could provide additional information on how significant any new vulnerability is."

The technique also has applications outside of computer science, such as current research in generating mathematical proofs or theorems. Using both proof assistants and LLMs could help researchers prove concepts they couldn't before, Revelle said.

"The use of formal verification and proof assistants is about to blow up, especially if we start doing things like having this feedback loop between LLMs and formal verification tools," Revelle said. "That is something that has applications to not just computer security, but lots of other fields."

The DARPA contract was originally awarded in February, just over a year after Revelle founded the HACR Lab. He previously worked as a principal investigator for Kudu Dynamics, the project partner, on similar projects.