Predoctoral Fellowship for mathematically provable hardware design

The world depends on increasingly complex systems to transfer messages, store data, manage medical devices, and perform many other critical services. But the more complex a system, the harder it can be to foresee its bugs and vulnerabilities. Exhaustive testing of different input scenarios is by now notoriously difficult, incomplete, and ineffective.

CSE PhD candidate Aman Goel has been selected to receive a Rackham Predoctoral Fellowship to overcome this limitation through the design of provably correct complex systems. Goel works with advisor Prof. Karem Sakallah to explore algorithmic ways to automatically verify the correctness of complex systems more scalably.

To achieve this, Goel designs algorithms that can automatically identify all of the different scenarios that can arise as a system runs. It then picks out the scenarios that violate critical system properties and demonstrates when none of these violations are possible. In that way, the system can be checked for correctness, even in the face of something unexpected by the designers, the whole way through running a process.

“We incorporate often ignored high-level structural information available at the design level to identify interesting details and abstract away unimportant low-level specifics,” Goel says. “This helps in identifying functional errors before deployment and in avoiding loss of revenue, down-times, reputation, and malicious attacks.”

Systems verified this way close off unexpected bugs and errors left vulnerable by traditional testing, which is typically limited by the foresight and imaginations of developers. In mission-critical digital systems, this kind of airtight design becomes especially important.

Goel developed a hardware verifier called AVR (Abstractly Verifying Reachability) that can apply these algorithmic methods to complex system components, such as hardware circuits, cryptographic protocols and distributed systems. 

“This allows for mathematically provable guarantees and assurance against critical design errors,” Goel says.

AVR was evaluated to be the best bit-vector verifier in the prestigious hardware verification competition HWMCC last year. AVR was further used for verifying problems beyond the hardware domain, particularly to automatically verify distributed protocols. This led to the development of I4, in collaboration with graduate student Haojun Ma and his advisor Prof. Manos Kapritsos, as well as Prof. Baris Kasikci and Jean-Baptiste Jeannin. I4 is a proof-inference tool that exploits AVR’s verification capabilities to apply structure-driven verification techniques borrowed from finite-domain verification to automatically verify parameterized protocols.

Aman’s research has appeared at top-tier venues like NASA Formal Methods, DATE, SOSP, HotOS and TACAS. He also received the runner-up position at the CSE Graduate Student Honors Competition 2019 for outstanding PhD research.