Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

Using Dependence Graphs to Assist Verification and Testing of Information-Flow Properties

Reviewed Paper In Proceedings

Author(s):Mihai Herda, Shmuel S. Tyszberowicz, and Bernhard Beckert
In:12th International Conference on Tests and Proofs (TAP 2018)
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:10889
Year:2018
Pages:83-102
DOI:10.1007/978-3-319-92994-1_5

Abstract

Information-flow control (IFC) techniques assist in avoiding information leakage of sensitive data to an observable output. Unfortunately, the various IFC approaches are either imprecise, thus producing many false positive alerts, or they do not scale. Using system dependence graphs (SDGs) to model the syntactic dependencies between different program parts is a highly scalable approach that enables to check whether the observable output depends on the sensitive input. While this approach is sound, security violations that it reports can be false alarms. We present a technique to overcome these problems by combining two existing approaches in a novel way. We show how each security violation reported by an SDG-based approach can be used to create a simplified program that can then be handled with a second approach to prove or disprove the reported violation. As the second approach we use deductive verification and test case generation. We show that our approach is sound, and demonstrate its benefits by means of examples. We discuss the challenges of implementing the approach using JOANA and KeY.

BibTeX

@InProceedings{TAP18,
  author        = {Mihai Herda and {Shmuel S.} Tyszberowicz and Bernhard Beckert},
  editor        = {Catherine Dubois and Burkhart Wolff},
  title         = {Using Dependence Graphs to Assist Verification and Testing of Information-Flow Properties},
  booktitle     = {12th International Conference on Tests and Proofs (TAP 2018)},
  year          = {2018},
  series        = {Lecture Notes in Computer Science},
  volume        = {10889},
  publisher     = {Springer},
  doi           = {10.1007/978-3-319-92994-1_5},
  month         = jun,
  pages         = {83--102},
  abstract      = {Information-flow control (IFC) techniques assist in avoiding information leakage of sensitive
                   data to an observable output. Unfortunately, the various IFC approaches are either imprecise,
                   thus producing many false positive alerts, or they do not scale. Using system dependence
                   graphs (SDGs) to model the syntactic dependencies between different program parts is a highly
                   scalable approach that enables to check whether the observable output depends on the
                   sensitive input. While this approach is sound, security violations that it reports can be
                   false alarms. We present a technique to overcome these problems by combining two existing
                   approaches in a novel way. We show how each security violation reported by an SDG-based
                   approach can be used to create a simplified program that can then be handled with a second
                   approach to prove or disprove the reported violation. As the second approach we use
                   deductive verification and test case generation. We show that our approach is sound, and
                   demonstrate its benefits by means of examples. We discuss the challenges of implementing
                   the approach using JOANA and {\KeY}.},
  isbn={978-3-319-92994-1}
}