中央研究院 資訊科學研究所

Automatic analysis of integer-manipulating programs is a main problem in program analysis. Such programs are a basic building block of more complex imperative programs (e.g. with linked lists or strings) since analysis of the latter can often be reduced to analysis of the former (e.g. by some variants of counter abstractions). Since they are already Turing-complete, the challenge is to devise approximation
techniques that give useful answers in many cases. In this talk, I will present an automata-based approach to statically analyse programs with numeric data types (based on Minsky's counter machines as the basic model). I will then introduce an approximation technique for analysing Minsky's machines (called "reversal-bounded analysis") that turns out to be sufficiently powerful for identifying erroneous runs for a large class of programs. Our technique reduces the analysis to an SMT problem, which can then be solved using highly-optimized SMT solvers like Microsoft Z3. We have implemented a prototype and shows the efficacies of the technique on a few interesting examples (e.g. buffer overflow vulnerabilities derived from Linux device drivers). This is a joint work with Matthew Hague, which has partly appeared in CAV'11 and CAV'12.

 

Anthony W. Lin received his PhD from University of Edinburgh's School of Informatics in 2010 under the supervision of Leonid Libkin and the co-supervision of Richard Mayr. His PhD thesis concerns generic and specific techniques for infinite-state model checking. He is currently an EPSRC Postdoctoral Research Fellow at Oxford University Department of Computer Science. His main interests lie in developing theoretically sound and practically applicable techniques in formal verification (especially with applications in program analysis and more recently on language-based security), utilizing techniques from logic and automata. He was awarded LICS 2010 Kleene Best Student Paper Award for his paper titled "Parikh Images of Grammars: Complexity and Applications".