网络空间安全之旅：从形式化方法、程序分析到数据分析——二进制漏洞检测实例
讲者：刘杨 博士，新加坡南洋理工大学助理教授
时间：6月16日（周五）上午 10:00am – 11:30am
地点：清华大学 FIT 3-225
演讲题目: Cyber-security, the journey from Formal Methods, Program Analysis to Data Analytics — with a Case Study on Binary Vulnerability Detection.
内容简介：
Cyber-security is a complex system research, which requires the knowledge across all layers of the computer architecture. In this talk, I would like to share our attempts to solve security problems using various techniques. Starting from formal methods, we have applied formal modeling and reasoning to security designs and implementations. These efforts lead to our recent research project “Securify: A Compositional Approach of Building Security Verified System”, which aims at building secure and verifiable systems ground-up. Security verification and building attack-free systems are very challenging tasks in the view of the size and the complexity of the systems. To solve the scalability problem, we start to explore various program analysis techniques with encouraging results.
Along the way, we have collected sizable samples, which are further used to improving security analysis, understand the security trend, attack attribution/correlation and eventually provide high-level intelligence. In this talk, I will use the binary vulnerability analysis as a running example to demonstrate the ideas of different approaches.
个人简介：
Dr Liu Yang graduated in 2005 with a Bachelor of Computing (Honours) in the National University of Singapore (NUS).
In 2010, he obtained his PhD and started his post doctoral work in NUS, MIT and SUTD. In 2011, Dr Liu is awarded the Temasek Research Fellowship at NUS to be the Principal Investigator in the area of Cyber Security. In 2012 fall, he joined Nanyang Technological University as a Nanyang Assistant professor. He is currently the director of the cybersecurity lab in NTU.
Dr. Liu specializes in software verification, security and software engineering. His research has bridged the gap between the theory and practical usage of formal methods and program analysis to evaluate the design and implementation of software for high assurance and security. His work led to the development of a state-of-the-art model checker, Process Analysis Toolkit (PAT). This tool is used by research institutions in over 80 countries for research and education. By now, he has more than 150 publications in top tier conferences and journals and is leading an active research team working on various cybersecurity problems.
个人主页: http://www.ntu.edu.sg/home/yangliu/
