Skip to main content

Lazy self-composition for security verification

Author(s): Yang, W; Vizel, Y; Subramanyan, P; Gupta, A; Malik, Sharad

To refer to this page use:
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 lazy self-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.
Publication Date: 18-Jul-2018
Electronic Publication Date: 18-Jul-2018
Citation: Yang, W, Vizel, Y, Subramanyan, P, Gupta, A, Malik, S. (2018). Lazy self-composition for security verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10982 LNCS (136 - 156. doi:10.1007/978-3-319-96142-2_11
DOI: doi:10.1007/978-3-319-96142-2_11
Pages: 136 - 156
Type of Material: Conference Article
Journal/Proceeding Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Version: Final published version. This is an open access article.

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.