New techniques to strengthen the security of information systems
communications and aviation electronics. The work with Rockwell Collins involves applying the K-State research team’s verification tools to several systems being developed in U.S. Department of Defense security research projects.
Hatcliff said information leakage is a concern in many domains, like potential integration in the health care system with patients’ medical records. “Millions of dollars are being invested by federal and state governments to set up health information exchanges,” Hatcliff said. “The idea of such an exchange is that you have a technology organization that facilitates and mediates the exchange of patient medical information between a variety of parties. The challenge is that the information in patients’ records has different levels of sensitivity or security. These exchanges eventually are going to need a way to specify policies describing what information can be released and to whom, and the exchange will need to guarantee that those policies are adhered to.”
Hatcliff said K-State’s research shows promise for addressing these issues because it involves creating mathematical and logical models that can be used by special computer-based auditing programs to guarantee that an information system conforms to the stated information flow policy.
The researchers’ tools also provide graphical visualizations of information flowing through a system so that designers and auditors can more quickly understand a system’s information flow behavior. The research focuses on systems where very high levels of assurance are required, and it aims to prove conformance to information flow policies during a certification phase before a system is deployed.
“It’s pretty rare in the software engineering and verification research community that you receive a significant amount of money to fund basic research and also have a company that’s doing such advanced work fund you to take your basic research and apply it,” Hatcliff said.
The collaboration with Princeton University is with Andrew Appel, professor and chair of Princeton’s computer science department.
“We’re very good at building tools that help programmers actually apply some of these techniques to real programs, and Andrew’s very good at developing the underlying math and logic,” Hatcliff said. “We’re working together to come up with an even better collection of tools.”
Through collaboration stipulations, the universities will provide student visits and exchanges. The grant also funds work for four graduate students and two undergraduates at K-State. K-State’s research group has been awarded more than $12 million of research funding the past 10 years. The group’s tools have been used in numerous academic research groups and by various industries worldwide.
