Please use this identifier to cite or link to this item: doi:10.22028/D291-25715
Title: A uniform framework for the formal specification and verification of information flow security
Author(s): Mantel, Heiko
Language: English
Year of Publication: 2003
SWD key words: Informationsfluss; Possibilitätstheorie; Formale Spezifikationstechnik
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
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.
Link to this record: urn:nbn:de:bsz:291-scidok-2024
hdl:20.500.11880/25771
http://dx.doi.org/10.22028/D291-25715
Advisor: Jörg H. Siekmann
Date of oral examination: 11-Jul-2003
Date of registration: 26-Apr-2004
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
HeikoMantel_ProfDrJoergHSiekmann.pdf3,66 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.