@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} }
Integration of Static and Dynamic Analysis Techniques for Checking Noninterference
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.