Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25715
Titel: A uniform framework for the formal specification and verification of information flow security
Verfasser: Mantel, Heiko
Sprache: Englisch
Erscheinungsjahr: 2003
SWD-Schlagwörter: Informationsfluss; Possibilitätstheorie; Formale Spezifikationstechnik
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: 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 zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-2024
hdl:20.500.11880/25771
http://dx.doi.org/10.22028/D291-25715
Erstgutachter: Jörg H. Siekmann
Tag der mündlichen Prüfung: 11-Jul-2003
SciDok-Publikation: 26-Apr-2004
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
HeikoMantel_ProfDrJoergHSiekmann.pdf3,66 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.