Lazy Self-Composition for Security Verification

Verification of secure information flow plays an important role in protection of security and privacy in software applications. It can be reduced to safety verification, as shown by Barthe et al., where a “self-composition” of the program is created by duplicating the program on which a safety property is verified. Due to practical challenges of software verification on duplicated copies, Terauchi and Aiken proposed to use type-directed transformation during self-composition. However it relies on static type analysis which can be imprecise. To further reduce the cost of verification, we use an approach based on bounded model checking to encode symbolic and precise propagation of taint, enabling lazy self-composition that duplicates only the tainted parts of the program. Furthermore, we perform additional checks during bounded model checking to enable early termination of security verification, without needing to compute program invariants. We have implemented a prototype information flow checker in the SeaHorn verification platform, which uses Horn-clause based program representations and the Z3 SMT solver in the backend. We present experiments showing effectiveness of our approach on several examples.