Skip to main content

Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis

Bichhawat, Abhishek, Rajani, Vineet, Garg, Deepak, Hammer, Christian (2014) Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis. In: PLAS'14: Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security. PLAS'14: Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security. . pp. 15-24. Association for Computing Machinery New York NY United States ISBN 978-1-4503-2862-3. (doi:10.1145/2637113.2637116) (KAR id:90566)

PDF Publisher pdf
Language: English
Download (302kB) Preview
[thumbnail of 2637113.2637116.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


Preventing implicit information flows by dynamic program analysis requires coarse approximations that result in false positives, because a dynamic monitor sees only the executed trace of the program. One widely deployed method is the no-sensitive-upgrade check, which terminates a program whenever a variable's taint is upgraded (made more sensitive) due to a control dependence on tainted data. Although sound, this method is restrictive, e.g., it terminates the program even if the upgraded variable is never used subsequently. To counter this, Austin and Flanagan introduced the permissive-upgrade check, which allows a variable upgrade due to control dependence, but marks the variable "partially-leaked". The program is stopped later if it tries to use the partially-leaked variable. Permissive-upgrade handles the dead-variable assignment problem and remains sound. However, Austin and Flanagan develop permissive-upgrade only for a two-point (low-high) security lattice and indicate a generalization to pointwise products of such lattices. In this paper, we develop a non-trivial and non-obvious generalization of permissive-upgrade to arbitrary lattices. The key difficulty lies in finding a suitable notion of partial leaks that is both sound and permissive and in developing a suitable definition of memory equivalence that allows an inductive proof of soundness.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1145/2637113.2637116
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Amy Boaler
Date Deposited: 04 Oct 2021 13:30 UTC
Last Modified: 06 Oct 2021 09:10 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year