Checking Memory Safety with Blast

Abstract. Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. Blast constructs, explores, and rebstractions of the program state space based on lazy predicate ion and interpolation-based predicate discovery. We show how Blast can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use CCured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that Blast can remove many of the r...

• Type: Conference
• Year: 2005
• Where: FASE
• Authors: Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
• Keywords: Blast, FASE 2005, Run-time Checks, Software Engineering, Temporal Safety