Online banking programs have to be able to do many things, ranging from transfers and account balance inquiries to money transfers. Long before programmers write the appropriate algorithms for processing input, they define which functionalities the program should have. To do this, they make use of various specification languages that allow them to describe the properties of programs at a higher level. "In the case of a banking app, for example, it must be defined that users do not learn any secret information, such as the account balance of other users," explains Raven Beutner. This secrecy property is called "non-interference" by researchers. The fact that a banking program exhibits this property in all executions must not only be assumed, but must also be able to be proven.
"We therefore look at how a program processes different inputs from users and how it behaves during program execution," Beutner explains. "For a large number of program properties, it is sufficient to look at a single program flow or at least a limited number of flows. Today, this can be done automatically in many cases with the help of special algorithms and tools." However, it becomes more difficult with so-called hyper-properties, which include the non-interference mentioned above. "This is a different class of properties. To prove them, we need to analyze and compare multiple program runs." Research has made progress in this area in recent years, but for many hyperproperties, existing methods are not yet sufficient for automatic testing, according to Beutner. "In our paper, we present a new technique for testing new classes of such properties."
The new method, which Beutner developed based on the work of and in cooperation with CISPA Faculty Prof. Bernd Finkbeiner, is expected to make it possible to automatically test more complex hyperproperties in the future. This new methodological approach contributes to the HYPER project initiated by Bernd Finkbeiner and his team, for which Finkbeiner was awarded an Advanced Grant from the European Research Commission. The stated goal of this project is to be able to mathematically formalize multilayered social concepts such as justice, explainability and privacy in the future and to prove them automatically in programs.
"With our approach, we have made a good first step for the automatic verification of even complex hyper-properties. But a lot of research is still needed to realize Bernd's vision," says Beutner. For example, he says, the implementation of the new approach, i.e., the practical implementation in real systems, is still prototype-like and thus not ready for practical use. "We just still have a lot to do. But our paper is a first step toward being able to automatically verify an even broader class of properties. The fact that we received a Distinguished Paper Award for it makes me very happy, of course. "
