Montana State Breaks Into DARPA Research with $780K Cybersecurity Award
MSU researchers developing AI tools to stay ahead of cyber attackers

By Staff Writer
Aug 7, 2025
BOZEMAN — Montana State University has landed its first cybersecurity research contract from the Defense Advanced Research Projects Agency, securing $780,000 as part of a $7.1 million federal award that could boost the university’s standing in national defense research.
The three-year contract, announced Wednesday, was awarded to MSU’s Harnessing Automation in Cybersecurity Reasoning Lab and Virginia-based cybersecurity company Kudu Dynamics through DARPA’s Intelligent Generation of Tools for Security program.
“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,” said Matt Revelle, director of the HACR Lab and principal investigator on the contract.
Revelle, a computer science professor in MSU’s Gianforte School of Computing, said the funding will support two graduate students working on cutting-edge cybersecurity automation research.
Automating threat assessment
The research aims to solve a fundamental problem in cybersecurity: how to objectively assess the severity of software vulnerabilities before attackers can exploit them.
Currently, cybersecurity experts rely on human-created scores to rate threats, a process Revelle describes as subjective. His team is developing automated tools to provide more accurate, objective assessments.
“Historically, the threat posed by vulnerabilities has been rated with human-created scores that can be subjective,” Revelle said. “Revelle and his team are repurposing a process called formal verification to create a more objective assessment.”
The work focuses on understanding “exploit chains” — sequences where attackers link multiple software vulnerabilities together to breach systems in ways that individual bugs couldn’t accomplish alone.
Revelle uses smartphones as an example of vulnerable systems with multiple components.
“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,” he said. “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.”
When attackers chain these vulnerabilities together, they can push software “into a state that it normally would never reach,” essentially rewriting programs to create new security holes.
Staying ahead of attackers
The MSU team is building their solution using Lean, a programming language and proof assistant tool. Their framework, called Quarry, allows researchers to describe attack techniques and prove whether software is susceptible to related threats.
The researchers are also incorporating artificial intelligence through large language models to help discover potential exploits, creating what Revelle calls “a powerful feedback loop” between AI and formal verification tools.
“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 has applications beyond cybersecurity, including mathematical proof generation and theorem proving.
“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.”
Building research reputation
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 on similar projects.
Revelle said the award opens doors for students to work on cutting-edge research while positioning MSU as a destination for cybersecurity talent.
The contract represents MSU’s entry into DARPA-funded cybersecurity research, potentially setting the stage for future defense-related projects as the university builds its reputation in the field.
“The research could have significant impacts on cybersecurity and other fields,” according to the university announcement.
Don’t miss the week’s top Montana stories
Join readers across Montana who rely on WMN for independent reporting.
Unsubscribe anytime. Want to support WMN? Upgrade for $4/month →