Integration of Static and Dynamic Analysis Techniques for Checking Noninterference

@incollection{BeckertHerdaKirstenTyszberowicz2020,
  author    = {Bernhard Beckert and
               Mihai Herda and
               Michael Kirsten and
               Shmuel Tyszberowicz},
  title     = {Integration of Static and Dynamic Analysis
               Techniques for Checking Noninterference},
  editor    = {Wolfgang Ahrendt and
               Bernhard Beckert and
               Richard Bubel and
               Reiner H{\"a}hnle and
               Mattias Ulbrich},
  booktitle = {Deductive Software Verification: Future Perspectives - Reflections
               on the Occasion of 20 Years of {\KeY}},
  pages     = {287--312},
  chapter   = {12},
  part      = {V: Integration of Verification Techniques},
  year      = {2020},
  month     = dec,
  abstract  = {In this article, we present an overview of recent combinations of
               deductive program verification and automatic test generation on
               the one hand and static analysis on the other hand, with the goal
               of checking noninterference. Noninterference is the non-functional
               property that certain confidential information cannot leak to
               certain public output, i.e., the confidentiality of that
               information is always preserved.

               We define the noninterference properties that are checked along
               with the individual approaches that we use in different
               combinations. In one use case, our framework for checking
               noninterference employs deductive verification to automatically
               generate tests for noninterference violations with an improved
               test coverage. In another use case, the framework provides two
               combinations of deductive verification with static analysis based
               on system dependence graphs to prove noninterference, thereby
               reducing the effort for deductive verification.},
  doi       = {10.1007/978-3-030-64354-6_12},
  series    = {Lecture Notes in Computer Science},
  volume    = {12345},
  publisher = {Springer}
}