I will be joining the Department of Computer Science at Columbia University as an Assistant Professor in Spring 2026. I completed my Ph.D. at Purdue University under the supervision of Samuel Conte Professor Xiangyu Zhang. Prior to that, I earned my B.Sc. with Zhiyuan Honors from Shanghai Jiao Tong University (SJTU).
I study the reliability and performance of modern software systems, combining formal reasoning with data-driven methods to represent expert knowledge in scalable and precise ways. My research aims to push the boundaries of how we rigorously understand software behavior, by improving either (a) the precision of analyses in a sound manner or (b) the scalability of analyses in an unsound manner, while explicitly qualifying the degree of confidence in their unsoundness.
🎯 I'm actively looking for self-motivated students to join my research group at Columbia CS. Strong software engineering skills, experience with low-level systems, or a background in CTFs would be highly preferred.
📬 If you're interested in working with me, please drop me an email with (1) your CV and (2) a brief overview of your research interests and relevant background.
| May, 2025 | I will join the Department of Computer Science at Columbia University as an Assistant Professor! |
|---|---|
| May, 2023 | We have released our Web3 bug dataset, which has received stars on GitHub! |
The best way to reach me is via email.
If you're specifically interested in topics related to binary analysis or Web3, feel free to reach out to [email protected] or [email protected], respectively.
For other general inquiries, please contact [email protected].
Special Notes. Sometimes I might miss your email, so don't hesitate to follow up if you don't hear back for a while.
That said, I do have a small trick to help you craft your email in a way that will easily catch my attention. I've encrypted this tip using a customized script, mycipher.py. Below is the encrypted message (in hex format):
040fc29c860b901336eae5caaf6942d79591253e75716770e794a31b0643382099ab594d5a4a106348b91f1ea98a4286b664f899a1ad632503253d4c3c87e89b315f8180fe00765afb5c0f286c573b6dc36d408f809cc9a368d20793a6c8a6f65541bc5a5b04eb4c1bbcd8742f94f9a7616ce1f347775badeaf5ac4b80be8e4a7979ac88f170ba7f86a7ad379e4381ead39a7bc33a05ebe9b492fabbeb12f318aa1aef96a518f59d16da6daafd9e1f5c930e241894a558b5609fcfb5b4094adf3344188d58f68a9c4b5266816f547313163b62cfb314811ad7a30bad24cfaafc62a31abfba4f45b28bf8c57585a8e8fa30acf74d87804afa3e213c4ad1925570ae221dc5f440a3aa96d48d02c743de13fc878836571bfcb57cbab43316995c248bb649e78561c149545ababf35b0082fff118fb4b9addd888bb27b201395ee6839dfafe9601d948bafdb669087f0ea3b9a071f22e50b76795741fb163f13e4ca4c465838a29deb24db89fdb56729987a98df495375d813e3901a6ee2d19dcd5d179d7fd184938b37e5963a1c1889da013a1af9c5f6df86dbea83ffb85b85b861
Unfortunately, the secret encryption key in mycipher.py has been lost 😕, and all I have are a few known plaintext-ciphertext pairs in data. If you do manage to decrypt the instructions above 🕵️♂️, just follow what they say 🧩.
Keywords:
Behavioral Contract, Smart Contract, Runtime Monitoring
close
Abstract:
Ensuring the reliability of smart contracts is of vital importance due to the wide adoption of smart contract programs in decentralized financial applications. However, statically checking many rich properties of smart contract programs can be challenging. On the other hand, dynamic validation approaches have shown promise for widespread adoption in practice. Nevertheless, as part of the programming environment for smart contracts, existing dynamic validation approaches have not provided programmers with a notion to clearly articulate the interface between components, especially for addresses representing opaque contract instances. We argue that the ``design-by-contract'' approach should complement the development of smart contract programs. Unfortunately, there is limited linguistic support for it in existing smart contract languages.
In this paper, we design a Solidity language extension ConSol that supports behavioral contracts. ConSol provides programmers with a modular specification and monitoring system for both functional and latent address behaviors. The key capability of ConSol is to attach specifications to first-class addresses and monitor violations when invoking these addresses. We evaluate ConSol using 20 real-world cases, demonstrating its effectiveness in expressing critical conditions and preventing attacks. Additionally, we assess ConSol's efficiency and compare gas consumption with manually inserted assertions, showing that our approach introduces only marginal gas overhead. By separating specifications and implementations using behavioral contracts, ConSol assists programmers in writing more robust and readable smart contracts.
abstract ➲
Keywords:
Path Sampling, Abstract Interpretation, Binary Analysis, Data Dependence
close
Abstract:
Binary program dependence analysis determines dependence between instructions and hence is important for many applications that have to deal with executables without any symbol information. A key challenge is to identify if multiple memory read/write instructions access the same memory location. The state-of-the-art solution is the value set analysis (VSA) that uses abstract interpretation to determine the set of addresses that are possibly accessed by memory instructions. However, VSA is conservative and hence leads to a large number of bogus dependences and then substantial false positives in downstream analyses such as malware behavior analysis. Furthermore, existing public VSA implementations have difficulty scaling to complex binaries.
In this paper, we propose a new binary dependence analysis called BDA enabled by a randomized abstract interpretation technique. It features a novel whole program path sampling algorithm that is not biased by path length, and a per-path abstract interpretation avoiding precision loss caused by merging paths in traditional analyses. It also provides probabilistic guarantees. Our evaluation on SPECINT2000 programs shows that it can handle complex binaries such as gcc whereas VSA implementations from the-state-of-art platforms have difficulty producing results for many SPEC binaries. In addition, the dependences reported by BDA are 75 and 6 times smaller than Alto, a scalable binary dependence analysis tool, and VSA, respectively, with only 0.19% of true dependences observed during dynamic execution missed (by BDA). Applying BDA to call graph generation and malware analysis shows that BDA substantially supersedes the commercial tool IDA in recovering indirect call targets and outperforms a state-of-the-art malware analysis tool Cuckoo by disclosing 3 times more hidden payloads.