南京大学计算机科学与技术系软件新技术与产业化协同创新中心

摘 要：

Analyzing the behavior of a program running on a processor that supports speculative execution is crucial for applications such as execution time estimation and side channel detection. Unfortunately, existing static analysis techniques based on abstract interpretation do not model speculative execution since they focus on functional properties of a program while speculative execution does not change the functionality. To fill the gap, we propose a method to make abstract interpretation sound under speculative execution. There are two contributions. First, we introduce the notion of virtual control flow to augment instructions that may be speculatively executed and thus affect subsequent instructions. Second, to make the analysis efficient, we propose optimizations to handle merges and loops and to safely bound the speculative execution depth. We have implemented and evaluated the proposed method in a static cache analysis for execution time estimation and side channel detection. Our experiments show that the new method, while guaranteed to be sound under speculative execution, outperforms state-of-the-art abstract interpretation techniques that may be unsound.

报告人简介:

Meng Wu is a software engineer at the Blockchain team of Ant Financial(Shanghai),  where he works on securing a scalable and reliable industry-class Blockchain system. He earned a Ph.D. in Computer Engineering at Virginia Tech, advised by Prof. Chao Wang. His research utilizes formal methods and static analysis techniques to improve software safety and security.

时间： 11月2日(星期六)10:30

地点：计算机科学技术楼230室