Nondeterministic Admissible Interference
Дата
Авторы
Mullins,John
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
In this article we address the issue of confidentiality of information in the context of downgrading systems i.e. systems admitting information flow between secrecy levels only through a downgrader. Inspired by the intuition underlying the usual definition of admissible information flow, we propose an analogue based on trace equivalence as developed in the context of concurrency theory and on a modification of the usual definition of purge function. We also provide unwinding conditions to guarantee a consistent and complete proof method in terms of communicating transition systems. We take advantage of this framework to investigate its compositionality issues w.r.t. the main operators over communicating transition systems. We conclude the article with a short presentation of this work s most promising aspects in the perspective of future developments.
Ключевые слова
specification techniques , program verification , security models , information flow properties , confidentiality , noninterference , intransitive noninterference