Software verification is crucial to ensure system correctness. We  leverage hardware/software model checking techniques for automata based string constraint solving to ensure the security of web services. Also, we build a sound software verification framework to detect vulnerabilities of iOS mobile apps, and block chain and smart contract systems. We reveal previously unknown vulnerabilities in public applications.

For verifying iOS Apps, we provide static analysis for systematic API vulnerability checking in iOS executables. A key feature is the ability to construct string dependency graphs for parameters of dynamically loaded classes and invoked methods. For verifying smart contracts, the EVM opcode runs on a stack-based virtual machine.  We generate the control flow graph for program analysis.

Most malicious behaviors and violations of security policies are related to the loaded classes and invoked methods of mobile applications. We develop an end to end tool called BinFlow for iOS API vulnerability detection.

Moreover, block chains and smart contracts have been deployed widely in fintech. Massive gas consumption causes unexpected exceptions. We present symbolic gas vulnerability detection.