Title: Reusable tools for formal modeling of machine code

Speaker: Gang Tan (Lehigh U., USA)

　　    www.cse.lehigh.edu/~gtan

Time: 10:00, 24th July 2014

Venue: Seminar Room (334), 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract:

Recent successes in verification show how machine-checked proofs can be scaled to real software systems. But these proofs only establish correctness with respect to a model of the underlying machine on which the code executes, and unfortunately, the community lacks high-fidelity, carefully tested specifications of widely-used machines, such as the Intel x86 line of processors. In this talk, we discuss our efforts to construct tools for building, reasoning about, and validating models of widely-used processor instruction set architectures such as the x86. Specifically, we are (1) designing Domain-Specific Languages (DSLs) for writing specifications of machine models, (2) proving the correctness of those DSLs, (3) using the DSLs to build formal models of commonly used processors, and (4) using the formal processor models to develop verified machine-code analyzers.

This work is in collaboration with Greg Morrisett at Harvard University.

Biography:

Dr. Gang Tan is an assistant professor of Computer Science and Engineering and leads the Security of Software (SOS) Lab at Lehigh University, PA. He received his bachelor's degree from Tsinghua University in 1999 and his Ph.D. degree from Princeton University in 2005. Honors include an NSF CAREER award and a Francis Upton Graduate Fellowship. His research is at the interface between computer security, programming languages, and software engineering. He is especially interested in software security, investigating methodologies that help create reliable and secure software systems.