Matt Harren

UC Berkeley Computer Science Division
577 Soda Hall
(510) 642-8290
(312) 550-7790 (cell)
matth @ cs.berkeley.edu

My CV.

If you're looking for something in particular, just ask.  In the meantime, here are some assorted papers and projects:

• My current research involves verifying that assembly code respects certain high-level properties that were previously enforced only at the source-code level. Tools such as CCured and Cqual enforce various security properties for source code through static analysis and/or instrumentation, but we need ways to ensure that the resulting assembly code respects these properties as well. The project therefore involves elements of decompilation, proof-carrying code, and dependent types.
  
  • "Using Dependent Types to Certify the Safety of Assembly Code." Matthew Harren and George C. Necula. Static Analysis Symposium (SAS), 2005. [pdf] [ppt]
  • "Analysis of Low-Level Code Using Cooperating Decompilers." Bor-Yuh Evan Chang, Matthew Harren, and George C. Necula. Static Analysis Symposium (SAS), 2006. [pdf]
  
  
• Deputy is a dependent type system for systems programming. Deputy guarantees partial type safety in C programs using runtime checks and annotations on function interfaces, but without any changes to the representation of data structures. Click on the link to find out more or to download the tool.
  
  • "Dependent Types for Low-Level Programming." Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George Necula. European Symposium on Programming (ESOP), March 2007. [pdf] [extended version]
  • "SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques." Feng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals, Matthew Harren, George Necula, and Eric Brewer. OSDI 2006. [pdf]
  
  
• XJ is a new programming language I worked on at IBM's T.J. Watson Labs that integrates Java's imperative programming style with XML's data model. We believe current API-based technologies for accessing XML data from within Java programs are inadequate because the semantics of XML are too far removed from those of the host language. XJ extends Java to make XML a first-class feature of the language, including support for XPath and strong, static typing. We use existing XML standards such as XML Schema and XQuery as the basis for the semantics of XJ, while adding imperative features such as in-place updates of XML data.
  
  • " XJ: Facilitating XML Processing in Java." Matthew Harren, Mukund Raghavachari, Oded Shmueli, Michael G. Burke, Rajesh Bordawekar, Igor Pechtchanski, Vivek Sarkar. In WWW 2005, pp278-287. [pdf]
  
  
• CCured guarantees type safety and memory safety for legacy C programs by examining the source code and, where necessary, adding runtime instrumentation to prevent unsafe behavior. Our goal is a tool that is easy to use on new programs and whose runtime cost is small enough to be practical on deployed systems. My focus has been on ensuring compatibility with uninstrumented library code to which we want to link.  Check out:
  
  • "CCured in the Real World." Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, and Westley Weimer. ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2003.
  • "CCured: Type-Safe Retrofitting of Legacy Software." George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, and Westley Weimer. ACM Transactions on Programming Languages and Systems, 2005. [pdf]
  • "Lightweight Wrappers for Interfacing with Binary Code in CCured." Matthew Harren and George C. Necula. International Symposium on Software Security, 2003. [pdf] [extended version]
  
  
• Federations in Go.   Combinatorial game theory relies on our ability to decompose games into sums of smaller, independent games. But what if the subgames are not truly independent, and there are a few certain combinations of moves that will allow one subgame to affect another?
  
  This project looked at the independence problem of Go endgames. We wrote an extension to AnalGo, a software tool that assists with the analysis of endgames, that can reason about Go subgames that are "mostly" independent but may interact under some circumstances. The new extension allows users to declare federations of subgames which may affect each other. In these federations, users specify conditions under which subgames interact, and the effects that these interactions could have. Federations simplify analysis because the subgames can be dealt with independently by the user, and the software will account for any overlap.
  
  This is joint work with Elwyn Berlekamp and was presented at the Canadian Math Society's 2004 Summer Meeting.
  
  
• Scrash examines the security and privacy risks inherent in remote crash reporting systems which automatically send part of the core file back to the developer in the event of a program failure. We propose erasing any sensitive user information that may appear in the core file before it is included in a crash report. We do this by applying static analysis to the program to determine which areas of memory may hold sensitive information, and modifying the program to make these areas easier to find and delete after a crash.
  • "Scrash: A System for Generating Secure Crash Information." Pete Broadwell, Matthew Harren, and Naveen Sastry. 12th USENIX Security Symposium, August 2003.
  
  
• Previously, I worked on
  • "Complex Queries in DHT-based Peer-to-Peer Networks." Matthew Harren, Joseph M. Hellerstein, Ryan Huebsch, Boon Thau Loo, Scott Shenker, and Ion Stoica. International Workshop on Peer-to-Peer Systems (IPTPS), March 2002.