Integration of Static and Dynamic Analysis Techniques for Checking Noninterference

Book Chapter

Author(s):Bernhard Beckert, Mihai Herda, Michael Kirsten, and Shmuel Tyszberowicz
In:Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:12345
Part:V: Integration of Verification Techniques
Chapter:12
Year:2020
Pages:287-312
DOI:10.1007/978-3-030-64354-6_12

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.

BibTeX

@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}
}