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 leverage MATLAB’s HDL Verifier for hardware verification and Polyspace Code Prover to advance type-based program analysis, while also exploring how his verification techniques could be integrated into these tools to scale security verification across processor architectures.