Hanzhi Liu

Bio

I am currently a first-year PhD student in computer science at the University of California, Santa Barbara. My advisor is Prof. Yu Feng. I completed my B.E. in EECS at Shanghai Jiao Tong University, where I was advised by Prof. Qinxiang Cao.

Previously, I worked as an intern at Veridise, a blockchain security startup. During my time there, I focused on developing and implementing verification tools for smart contracts and zero-knowledge proofs.

Research Interests

I am interested in the field of program verification, which focuses on ensuring the functional correctness of programs at different levels of abstraction. My research experience includes working with language semantics, compiler optimizations, and practical applications of verification.

Additionally, I am intrigued by the potential of verification techniques to enhance the security and reliability of blockchain systems. As blockchain technology gains popularity and influence, I believe that incorporating verification methods can be beneficial in these systems.

Publications

[1] Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, Işıl Dillig, and Yu Feng. Certifying Zero-Knowledge Circuits with Refinement Types. To appear at S&P 2024. [PDF]

[2] Lingyun Zhou*, Kaiwei Wu*, Hanzhi Liu*, Yuanning Gao, and Xiaofeng Gao. CIRD-F: Spread and Influence of COVID-19 in China. J Shanghai Jiaotong Univ Sci, 2020, 25(2): 147-156.

(* means these authors contributed equally)

Tools

Coda | A domain-specific language for zero-knowledge proof circuits and its verification toolchain. I have successfully used this language and toolchain to formally prove the correctness of circuits within various projects, including CircomLib, Circom Pairing, Light Protocol, Semaphore, and Sismo.

CompcertA | A novel soundness framework to support verification-aided compilation optimization of Clight. I implemented a deeply embedded assertion language based on the Compcert memory model using separation logic and proved the soundness of the symbolic execution of this language on Clight. I also formally proved the soundness of alias analysis based on the framework and applied this optimization to a C implementation of Red-Black Tree.

Bug Reports

Circom Pairing: BigMod/BigMod2 incorrectly omits range checks on the remainder. PR-16

Compcert: Clight contains incorrect comments about the semantics of the loop statement. PR-427

Circomlib-ML: IsPositive() treats zero as a positive number. PR-3

Contact

Twitter | Where I post my thoughts on programming verification, blockchain security, and my life.

GitHub | I am a big fan of open source. I am one of the maintainers of Software Foundations (Chinese Translation) and Simple-XX.

Hanzhi Liu

Bio

I am currently a first-year PhD student in computer science at the University of California, Santa Barbara. My advisor is Prof. Yu Feng. I completed my B.E. in EECS at Shanghai Jiao Tong University, where I was advised by Prof. Qinxiang Cao.

Previously, I worked as an intern at Veridise, a blockchain security startup. During my time there, I focused on developing and implementing verification tools for smart contracts and zero-knowledge proofs.

Research Interests

I am interested in the field of program verification, which focuses on ensuring the functional correctness of programs at different levels of abstraction. My research experience includes working with language semantics, compiler optimizations, and practical applications of verification.

Additionally, I am intrigued by the potential of verification techniques to enhance the security and reliability of blockchain systems. As blockchain technology gains popularity and influence, I believe that incorporating verification methods can be beneficial in these systems.

Publications

[1] Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, Işıl Dillig, and Yu Feng. Certifying Zero-Knowledge Circuits with Refinement Types. To appear at S&P 2024. [PDF]

[2] Lingyun Zhou*, Kaiwei Wu*, Hanzhi Liu*, Yuanning Gao, and Xiaofeng Gao. CIRD-F: Spread and Influence of COVID-19 in China. J Shanghai Jiaotong Univ Sci, 2020, 25(2): 147-156.

(* means these authors contributed equally)

Tools

Coda | A domain-specific language for zero-knowledge proof circuits and its verification toolchain. I have successfully used this language and toolchain to formally prove the correctness of circuits within various projects, including CircomLib, Circom Pairing, Light Protocol, Semaphore, and Sismo.

CompcertA | A novel soundness framework to support verification-aided compilation optimization of Clight. I implemented a deeply embedded assertion language based on the Compcert memory model using separation logic and proved the soundness of the symbolic execution of this language on Clight. I also formally proved the soundness of alias analysis based on the framework and applied this optimization to a C implementation of Red-Black Tree.

Bug Reports

Circom Pairing: BigMod/BigMod2 incorrectly omits range checks on the remainder. PR-16

Compcert: Clight contains incorrect comments about the semantics of the loop statement. PR-427

Circomlib-ML: IsPositive() treats zero as a positive number. PR-3

Contact

Twitter | Where I post my thoughts on programming verification, blockchain security, and my life.

GitHub | I am a big fan of open source. I am one of the maintainers of Software Foundations (Chinese Translation) and Simple-XX.