Interview with BI research group Verified System Design Automation
In this interview, the Verified System Design Automation research group at the Barkhausen Institut shares insights into its current work and research focus areas, with additional perspectives from individual group members.
“I always preferred correctness over performance. After all, what good is a system that performs particularly well in some cases but fails in all others?! Apart from that, I can see the beauty in a proof. An algorithm with impressive performance metrics is often replaced by another within just in a few months. A proof, however, remains valid.”
- Sebastian Ertel (Research Group Leader)
What is the research topic of your group?
The Verified System Design Automation team applies formal verification, a mathematical method for provably ensuring system properties. They frequently use theorem provers, which are software tools that help construct mathematical proofs and check their correctness. These methods support the design, specification, and implementation of programming languages, operating systems, and hardware.
In which project are you working currently?
Currently, the team is heavily involved in the Formula-V project. This project is set out to provide an almost gap-free verification of a unikernel running on top of an RISC-V processor.
"Towards the end of my bachelor's, I attended a seminar by the Turing award winner Silvio Micali, titled: "Proofs, Secrets and Computations". That event inspired me to investigate more the fields of logic and cryptography."
- Carmine Abate (Senior Researcher)
What is the connection between your research and everyday life? What problems and challenges are you trying to solve?
Our key objective is to make digital systems more trustworthy. Given the invasiveness of these systems into our day-to-day lives, our research impacts not only our lives but also those of many others. But formal verification is by no means as easy as counting to three. Designing a specification for a system and then proving that this system indeed follows this specification is a challenging process. We are trying to ease that burden by building compilers and automation into our verification tools.
“Formal verification is definitely not easy. There are moments when it feels like every proof fights back against you. But the satisfaction of finally solving a difficult problem and knowing that you’re strengthening the foundations of cryptographic security makes all the effort worthwhile. It’s the kind of work that’s challenging but deeply rewarding.”
- Sara Zain (Senior Researcher)