Security News > 2024 > January > Researchers develop technique to prevent software bugs

A team of computer scientists led by the University of Massachusetts Amherst recently announced a new method for automatically generating whole proofs that can be used to prevent software bugs and verify that the underlying code is correct.

"Reducing bugs in software, or even producing bug-free software, has been a holy grail of systems building for decades unfortunately, the state-of-the-practice in our society is that we expect all software to have bugs. Building bug-free software is just an incredibly difficult challenge."

The effects of buggy software can range anywhere from the annoying-glitchy formatting or sudden crashes-to potentially catastrophic security breaches or the precision software used for space exploration or controlling healthcare devices.

"These proofs can be many times longer than the software code itself," says Emily First, the paper's lead author who completed this research as part of her doctoral dissertation at UMass Amherst.

"Formal verification is one very promising method for building bug-free software. Engineers still build the software system, but with it, they build mathematical proofs that the software is correct. These proofs are quite hard to write, but there are ample tools that support this process, including specialized languages and theorem provers that then take the proof and machine-check it against the software to verify that the software is correct," commented Brun.

"Our work focuses on trying to automate the writing of these proofs. Baldur uses large language models to, given a mathematical theorem, automatically generate a proof of that theorem that a theorem prover can then verify. One benchmark, our method, combined with prior methods, generates proofs fully automatically 65.7% of the time, which is quite promising and would save engineers significant manual effort in writing these proofs," Brun concluded.

News URL

https://www.helpnetsecurity.com/2024/01/10/baldur-prevent-software-bugs/