Static Taint Analysis for Bug Checking

Speaker: Chenyi Zhang

When: 10:00, Wednesday 30th January 2008

Venue: 78-420

Software bugs which can be exploited by user-input are regarded as security vulnerabilities. In this talk, we present Static Taint Analysis, a program analysis technique for computing user-input dependencies. Taint analysis is used as a preprocessing filter for ``parfait'' -- our static bug-checking tool. User-input dependence is defined as a Meet-Over-all-Paths (MOP) solution expressed in a data flow analysis framework, and later reduced into a graph reachability problem. This work has been done within the LLVM (low level virtue machine) framework which uses SSA (static single assignment) form.

Bio: Chenyi Zhang is a Graduate Intern at Sun Microsytems Laboratories in Brisbane, Australia, where he contributes to the Parfait project. He is a PhD student in the School of Computer Science and Engineering at the University of New South Wales. He is also a joint student in the Formal Methods group at National ICT Australia (NICTA). His PhD work applies Formal Methods on Computer Security, in particular Information Flow Analysis.

Hospitality: Cristina Cifuentes

Contact: Robert Colvin (SSE seminar co-ordinator) (robert@itee.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html