Author: 

Thomas Jensen

Title: 

A mechanized semantics of taint analysis. 


Abstract:

We present a formalization of the dependency analysis underlying taint
tracking. The formalization is based on the recent notion of
pretty-big-step semantics, is expressed as a succession of
instrumented semantics, and has been mechanized inside the Coq proof
assistant.