Title: Coinductive unwinding of security-relevant hyperproperties: extended version
Authors: Milushev, Dimiter
Clarke, Dave
Issue Date: Aug-2012
Publisher: Department of Computer Science, KU Leuven
Series Title: CW Reports vol:CW623
Abstract: Unwinding relations have been widely used to prove that finite systems are secure with respect to a variety of noninterference policies. The latter are prominent instances of security-relevant hyperproperties. As hyperproperties are defined on potentially infinite systems, a new mathematical development is needed in order to (re)use unwinding relations for generic verification of security-relevant hyperproperties. In this paper we propose a framework for coinductive unwinding of security relevant hyperproperties. To illustrate the usefulness of the framework, we show that Mantel’s Basic Security Predicates (BSPs), the noninterference policies they compose, as well as their respective unwinding relations, have a meaningful coinductive reinterpretation. We prove that in a number of cases the coinductive variants of the unwinding relations imply the respective coinductive variants of the BSPs. Moreover, the latter can be used to compose high-level security-relevant hyperproperties for both finite and infinite systems. A number of the unwinding theorems also hold as expected. In conclusion, the proposed framework and results are useful both theoretically in the study of hyperproperties and in practice for verification of hyperproperties on potentially infinite systems.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW623.pdfDocument Published 691KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.