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

@InProceedings{TAP18,
  author        = {Mihai Herda and Shmuel 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}
}