Shuvendu Lahiri:
Unifying Type Checking and Property Checking for Low-Level Code in HAVOC

Abstract: We present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on complex, program-specific specific invariants that are difficult for traditional type checkers to express. Conversely, property checking for low-level code is challenging because it is difficult to write concise specifications that distinguish between locations in an untyped programs heap. We address both problems simultaneously by implementing a type checker for low-level code as part of our property checker HAVOC. We present a low-level formalization of a C program's heap and its types that can be checked with an SMT solver, and we provide a decision procedure for checking type safety. Our type system is flexible enough to support a combination of nominal and structural subtyping for C, on a per-structure basis. We discuss several case studies that demonstrate the ability of this tool to express and check complex type invariants in low-level C code, including several small Windows device drivers.

This is joint work with Jeremy Condit and Shaz Qadeer (MSR Redmond), and intern Brian Hackett (Stanford), and will appear in POPL09. The work is part of an ongoing effort of performing precise and scalable analysis of low-level systems code in HAVOC.

Bio:
Shuvendu Lahiri is a Researcher in the Software Reliability Research group at Microsoft Research, Redmond, since 2004. He obtained a M.S. and a Ph.D. in Computer Engineering from Carnegie Mellon University in 2001 and 2004 respectively, working with Randy Bryant. Earlier, he obtained his B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Kharagpur in 1999. He is currently interested in decision procedures, abstraction mechanisms and symbolic reasoning for verifying large-scale systems software. His Ph.D. dissertation "Unbounded System Verification using Decision Procedure and Predicate Abstraction" won the 2004-2005 ACM (SIGDA) Outstanding Ph.D. Dissertation in Electronic Design Automation.

Appointments: dcm@cs.cmu.edu

Maintainer [ Home > Seminar ]
`Last modified: Wed Oct 8 11:09:10 EDT 2008