Lazy Self-Composition for Security Verification

Authors: Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta and Sharad Malik

Paper Information

Title:Lazy Self-Composition for Security Verification
Authors:Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta and Sharad Malik
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:information flow analysis, security verification, k-safety verification, taint analysis, self-composition, lazy self-composition, bounded model checking

ABSTRACT. The secure information flow problem, which checks whether low-security outputs of a program are influenced by high-security inputs, has many applications in verifying security properties in programs. In this paper we present lazyself-composition, an approach for verifying secure information flow. It is based on self-composition, where two copies of a program are created on which a safety property is checked. However, rather than an eager duplication of the given program, it uses duplication lazily to reduce the cost of verification. This lazy self-composition is guided by an interplay between symbolic taint analysis on an abstract (single copy) model and safety verification on a refined (two copy) model. We propose two verification methods based on lazy self-composition.The first is a CEGAR-style procedure, where the abstract model associated with taint analysis is refined, on demand, by using a model generated by lazy self-composition. The second is a method based on bounded model checking, where taint queries are generated dynamically during program unrolling to guide lazy self-composition and to conclude an adequate bound for correctness. We have implemented these methods on top of the SEAHORN verification platform and our evaluations show the effectiveness of lazy self-composition.

Talk:Jul 17 09:30 (Session 117A: Theory and Security)