With powerful computers in nearly every back pocket, the 21st century is indelibly shaped by the software that processes everything from entertainment to education.
When this software works well and securely, it’s very easy to take for granted. However keeping software security safe, reliable and secure is by no means an easy task. Code complexity, software size and finite resources all present barriers to verify that software behaves as intended.
Assistant professor of computer science Elena Sherman is determined to change this with the support of a five-year National Science Foundation CAREER award of more than $470,000.
The key to software verification is computation of program invariants. Program invariants are summaries of possible program behaviors, which help a software engineer to generate, debug and optimize the software. Unfortunately, current methods for computing these invariants are not keeping pace with software complexity. An additional problem is that while better strategies for developing program invariants are available, they are too difficult for most engineers to apply without highly specialized training.
Sherman’s goal is to develop new techniques to compute program invariants more efficiently and accurately, and develop a framework that will empower engineers to find the best methods to perform software verification using computed code invariants.
“We need to figure out what those actual programs do before we can ask if they are secure or not,” said Sherman. “And the technique that I work with, called static analysis, that’s able to reason out all the possible ways your program can work and operate without actually executing the program.”
In addition to carrying out this research, Sherman also will be offering educational sessions for professional programmers through Boise State’s Center for Professional Development. These courses will give participants a greater understanding of how to use static analysis tools and better prepare them to improve the quality of their software. She said she is particularly eager as an educator to have the opportunity to teach adult and second-degree learners.
“There are lots of static analysis commercial tools, but it’s very difficult for people who just have a computer science degree, or who don’t even know what it is, to use them. Basically it’s very, very essential for improving the quality of your software in general, and identifying what’s going on with defects we have,” explained Sherman.
Sherman’s interest in static analysis techniques actually arose when she took a compiler class, and her mentor explained that a computer bug could be found and remedied without running the program.
“It was kind of fascinating, just the concept that you can take a program code, design algorithms to look at it and say, ‘Actually your program is going to crash at some executions,’” said Sherman. “And I also like the theory. We have so many programs I can actually implement the theoretical concepts in my tool and analyze programs.”
Sherman is one of five College of Engineering faculty awarded a NSF Career Award in 2020. Go here to learn more.
