Abstract:

Splice is a new programming framework that allows security-conscious applications to efficiently locate and delete a user’s in-memory state. The core technical challenge is determining how to delete a user’s memory values without breaking application-specific semantic invariants involving the memory state of remaining users. Splice solves this problem using three techniques: taint tracking (which traces how a user’s data flows through memory), deletion by synthesis (which overwrites each user-owned memory value in place, replacing it with a value that preserves the symbolic constraints of enclosing data structures), and a novel type system (which forces applications to employ defensive programming to avoid computing over synthesize-deleted values in unsafe ways). Using four realistic applications that we ported to Splice, we show that Splice’s type system and defensive programming requirements are not onerous for developers. We also demonstrate that Splice’s runtime overheads are similar to those of prior taint tracking systems, while enabling strong deletion semantics.

Paper