BitBlaze & WebBlaze: Tools for computer security using SMT Solvers

This talk centers on the program analysis approach of deriving symbolic expressions of software behavior, and then automatically reasoning about those expressions using an SMT solver. This approach have proved very powerful in security applications, because it is both precise (avoiding approximation) and flexible (the same representation can support many kinds of queries). I'll cover some examples of how we use this class of techniques in our BitBlaze and WebBlaze projects, which target the security challenges of binary software and web software respectively. First I'll discuss approaches for finding buffer overflow vulnerabilities by combining static analysis with symbolic execution, and performing quantitative information flow measurement by viewing channel capacity as a #SAT problem. In the web context, character strings are a critical data type: I'll discuss how we dealt with them in analyzing a browser feature know as "content sniffing", and in searching for client-side vulnerabilities in JavaScript code.

Links to the projects discussed in the talk (the pages in turn have links to the publications):

• http://bitblaze.cs.berkeley.edu/sdse-testgen.html
• http://bitblaze.cs.berkeley.edu/influence.html
• http://webblaze.cs.berkeley.edu/2009/content-sniffing/
• http://webblaze.cs.berkeley.edu/2010/kudzu/

Speaker: Stephen McCamant, for Dawn Song & Prateek Saxena, University of California, Berkeley, USA

Stephen McCamant is a postdoctoral scholar at UC Berkeley, working with Prof. Dawn Song and the BitBlaze research group primarily on binary-level program analysis techniques for software security. From 2002 to 2008 he was a graduate student at the MIT's Computer Science and AI Lab. His research at MIT applied dynamic and static analysis techniques to the challenges of software engineering and security, including predicting incompatible software upgrades (using Simplify for behavioral subtyping), and software-based fault isolation (a basis for the Google Native Client system, including an ACL2-checked safety
proof).

Prateek Saxena is a Phd candidate at UC Berkeley. His research combines program analysis and formal methods to practical problems in computer security. He is actively involved in two umbrella research projects at Berkeley: BitBlaze and WebBlaze, which are platforms for binary analysis and web security respectively. His work on JavaScript symbolic execution and the Kaluza string decision procedure has received the AT&T best applied security research paper award for 2011. He is the recipient of the Symantec Research Fellowship 2011-12. He completed his MS from Stony Brook University in 2007.

Dawn Song is an associate professor of Computer Science at UC Berkeley. Prior to joining UC Berkeley, she was an Assistant Professor at Carnegie Mellon University from 2002 to 2007. Her research interest lies in security and privacy issues in computer systems and networks, including areas ranging from software security, networking security, database security, distributed systems security, to applied cryptography. She is the recipient of various awards including the MacArthur Fellowship, the Guggenheim Fellowship, the NSF CAREER Award, the Alfred P. Sloan Research Fellowship Award, the MIT Technology Review TR-35 Award, the IBM Faculty Award, the George Tallman Ladd Research Award, the Okawa Foundation Research Award, and the Li Ka Shing Foundation Women in Science Distinguished Lecture Series Award. She is also the author of multiple award papers in top security conferences, including the best paper award at the USENIX Security Symposium and the highest ranked paper at the IEEE Symposium on Security and Privacy.