The Community for Technology Leaders
2018 IEEE Symposium on Security and Privacy (SP) (2018)
San Francisco, CA, US
May 21, 2018 to May 23, 2018
ISSN: 2375-1207
ISBN: 978-1-5386-4353-2
pp: 885-899
Ziqiao Zhou , University of North Carolina at Chapel Hill
Zhiyun Qian , University of California, Riverside
Michael K. Reiter , University of North Carolina
Yinqian Zhang , The Ohio State University
ABSTRACT
Noninterference is a definition of security for secret values provided to a procedure, which informally is met when attacker-observable outputs are insensitive to the value of the secret inputs or, in other words, the secret inputs do not "interfere" with those outputs. This paper describes a static analysis method to measure interference in software. In this approach, interference is assessed using the extent to which different secret inputs are consistent with different attacker-controlled inputs and attacker-observable outputs, which can be measured using a technique called model counting. Leveraging this insight, we develop a flexible interference assessment technique for which the assessment accuracy quantifiably grows with the computational effort invested in the analysis. This paper demonstrates the effectiveness of this technique through application to several case studies, including leakage of: search-engine queries through auto-complete response sizes; secrets subjected to compression together with attacker-controlled inputs; and TCP sequence numbers from shared counters.
INDEX TERMS
information-flow, noninterference, approximate-model-counting
CITATION

Z. Zhou, Z. Qian, M. K. Reiter and Y. Zhang, "Static Evaluation of Noninterference using Approximate Model Counting," 2018 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, US, , pp. 885-899.
doi:10.1109/SP.2018.00052
95 ms
(Ver 3.3 (11022016))