Technology being developed at the University of Kansas will make it easier and cheaper to build highly dependable, secure software, potentially saving billions of dollars annually. Andy Gill, an assistant professor in electrical engineering and computer science (EECS), recently received a $500,000 National Science Foundation grant to streamline tools for the development of high assurance computer systems. The innovative support tools will provide greater transparency and scrutiny when building critical components for large complex systems, dramatically reducing the all-too-common bugs and glitches that occur in current software.
When programmers build software, they first must determine how it will be used and then how it will function. They should then evaluate the software to ensure the description and function match, but this step is cumbersome and expensive. All too often, crude testing methods are used instead, inadvertently neglecting to test critical corner cases that later result in bugs in real-world deployment. A National Institute of Standards and Technology study found that software defects cost the economy $60 billion annually and account for 80 percent of software development costs.
Gill is building the Haskell Equational Reasoning Model-to-Implementation Tunnel (HERMIT) to improve software correctness. HERMIT mathematically, or formally, analyzes each step of development, providing rigorous connections between system requirements and the programming details of a real application. While system requirements and programs are typically written in two different computer languages and often evaluated in a third, HERMIT provides a common foundation that generates evidence that the description and action match. These continuous checks and balances make much it harder for errors to be introduced, and HERMIT’s precise documentation style allows any pesky bugs to be caught early in the process.
“When we are talking about building large systems with millions of lines of code, finding errors can be very difficult. Unreliable software hurts companies’ reputations and costs them customers,” said Gill, who conducts his research at KU’s Information and Telecommunication Technology Center (ITTC). “HERMIT uses new ideas from software engineering and mathematics to make the evaluation of high-assurance software development more manageable.”
As well as helping with software development, Gill hopes HERMIT can be customized for developing hardware solutions. Gill gave an invited talk at the NSA-sponsored High Confidence Software and Systems conference in Maryland last year about the precursor to HERMIT that generated a hardware-based signal decoder. While collaborating with EECS Associate Professor Erik Perrins on the implementation of a system that helps correct naturally occurring errors in noisy transmissions, Gill applied the HERMIT rules by hand, leading to an efficient design and a more reliable decoding system.
Before joining the KU faculty, Gill was involved in a previous commercialization cycle of technology developed in academia. Gill was a principal project scientist for the PacSoft research group in the Oregon Graduate Institute of Science and Technology. Together with colleagues from PacSoft, Gill commercialized a software engineering method developed at the Graduate Institute and other academic institutions, building a software engineering firm with 40 employees. Gill hopes to repeat this success with HERMIT.