A uniform framework for the formal specification and verification of information flow security

Abstract

In this thesis, we elaborate a uniform basis for the systematic investigation of possibilistic information flow properties. These properties are suitable for specifying security requirements formally such that they can be verified with mathematical rigor. We analyze the variety of known properties, propose new ones, and develop techniques that simplify their verification. To this end, we introduce MAKS, a uniform framework for the investigation of information flow properties. The two basic ideas underlying MAKS are: firstly, to separate application specific aspects of an information flow property from more application-independent aspects and, secondly, to express the latter aspects by assembling primitive building blocks. This modular representation provides a basis for reducing complex reasoning about information flow properties to reasoning about conceptually simpler building blocks. Following this approach, we analyze several information flow properties from the literature, elaborate their advantages and disadvantages, and derive a taxonomy of these properties. In this process, we discover several novel information flow properties that constitute improvements of known ones. Moreover, we exploit the modular representation for developing verification techniques for information flow properties. In particular, we derive unwinding results that reduce the verification of information flow properties to the verification of simpler unwinding conditions. We also derive compositionality results that support the verification task to the verification of the individual system components. The applicability of our results is demonstrated by several examples and also by a complex case study from the area of language-based security.

Die vorliegende Arbeit präsentiert einen Ansatz zur systematischen Untersuchung possibilistischer Informationsflusseigenschaften. Diese Klasse von Eigenschaften eignet sich für die formale Spezifikation von Sicherheitsanforderungen hinsichtlich Vertraulichkeit und Integrität und ermöglicht es, solche Anforderungen mit mathematischer Genauigkeit zu beweisen. Die aus der Literatur bekannten Informationsflusseigenschaften werden in der Arbeit eingehend analysiert und verglichen, neue Eigenschaften werden synthetisiert, und es werden Verifikationstechniken für Informationsflusseigenschaften vorgeschlagen.