Tingzhen Dong

Tingzhen Dong is a graduate student in electrical engineering and computer science rethinking formal verification methods to ensure security properties across the hardware-software stack. Speculative execution vulnerabilities pose serious threats to modern processors, yet providing rigorous guarantees that hardware defenses work correctly remains challenging due to out-of-order processor complexity. Tingzhen developed microarchitecturally guided unbounded model checking to prove non-interference properties on complex processors by introducing uninterpreted functions with history to abstract sequential modules like renaming stages and reorder buffers, dramatically reducing verification complexity. On the software side, he designed a typed assembly language framework with heuristic type inference to transform cryptographic programs at the assembly level, ensuring sensitive data segregation on the stack for coarse-grained hardware taint tracking—achieving security guarantees with only 1.2% overhead. As a MathWorks Fellow, Tingzhen will advance hardware verification and type-based program analysis, exploring how his techniques can scale security verification across processor architectures.