On an airplane, in a self-driving car or in sensitive online transactions: We are often dependent on digital systems working correctly. But how can this be guaranteed? Daniela Kaufmann from the Institute of Logic and Computation is working on new ideas to solve this task. 

If hardware, software or even a cryptographic system is examined by trying out all logical possibilities, the task quickly becomes unmanageably complex: an astronomical number of conceivable inputs would have to be tried out to guarantee correctness. Instead, Daniela Kaufmann wants to translate the system into algebraic formulas that can be used to work efficiently. The aim is to create tools for the hardware and software industry that prove the flawlessness of a computer system with mathematical precision. 

Trust is bad, control is necessary

If a system has already worked correctly with many different inputs, this does not mean that it will work correctly the next time you try a new input. "Again and again you find surprising errors," says Daniela Kaufmann. "For example, the famous Pentium bug that caused Pentium processors to deliver an incorrect result for very specific divisions in the 1990s. Or a recently discovered bug in a Linux kernel that allowed certain users to gain unauthorized root access." 

In a world where even our lives often depend on the correct functioning of logical systems, this is unsettling: In critical situations, you want mathematical proof that a computer system is guaranteed to provide the right answer in every conceivable situation. 

The automatic security guarantee

"What we need is a tool that automatically checks the correctness of other systems," says Daniela Kaufmann. "And there is: so-called SMT solvers can automatically determine whether a certain logical formula has a solution." So you have to translate a logical system, such as a part of a computer chip, into a logical formula, and ask the SMT solver the question: "Is there a possible situation in which this logical formula breaks the rules?" 

However, this is often extremely time-consuming. "An SMT solver formulates the logic at the bit level," explains Daniela Kaufmann. "For example, if two numbers are multiplied together, then this multiplication can be translated into logical relationships between the individual bits with which these numbers are encoded." But this transfers the rather simple operation of a multiplication into a quite complex system of logical links at the bit level. The mathematical structure of the original task is not used. 

"We don't completely decompose arithmetic parts of a system into logical statements about individual bits," says Daniela Kaufmann. "Instead, we preserve their algebraic structure and represent them as polynomials. We translate the logic of the circuits into mathematical expressions that can be used to calculate according to the usual rules of algebra." 

However, Daniela Kaufmann does not want to rely on existing algebra tools here: The algorithms that process these polynomials are to be tailored precisely to this area of application. "It is also important to note that with our method it will be possible to issue a kind of certificate," explains Kaufmann. "If our method says: Yes, this chip works correctly, then this is not just a judgment that you have to believe, but you get a verifiable mathematical answer that proves this correctness." 

Daniela Kaufmann

Daniela Kaufmann studied computational mathematics at the Johannes Kepler University Linz, where she received her doctorate with distinction in computer science in 2020. After several years as a university assistant in Linz, she worked at the Software Competence Center Hagenberg and as a postdoc at the Vienna University of Technology, among other places. 

Since 2024, she has been an FWF-ESPRIT research group leader there and heads the "CalgSAT" project, which combines computer algebra methods with SAT solving for automated mathematical reasoning. Her research focuses on the interface between symbolic computing, formal verification, and automated reasoning – in particular in the verification of arithmetic circuits, in computing in finite algebraic structures, and in machine-controllable proofs. 

Her dissertation was awarded the GI Dissertation Prize and the Heinz Zemanek Prize. With the ERC grant "POLARIS" (Advancing Polynomial and Logical Approaches for Trusted Automated Reasoning over Integrated Systems), she will now expand her team and translate her theoretical ideas into industrially usable tools.

Contact

Dr. Daniela Kaufmann
Institute for Logic and Computation
TU Wien
daniela.kaufmann@tuwien.ac.at

Text: Florian Aigner