Abstract
Verläßlichkeit und Vertrauenswürdigkeit sind zunehmend entscheidend für die Anwendbarkeit und die Akzeptanz von Systemen der Informationstechnik. Zur Gewährleistung der Funktionssicherheit (Korrektheit), eines Teilaspekts von Verläßlichkeit und Vertrauenswürdigkeit, wurden in der Informatik verschiedene formale Methoden zur Programmverifikation entwikkelt. Im Beitrag wird zunächst wird ein Verifikationssystem für Programme in imperativen Programmiersprachen vorgestellt. Die zum System gehörende Sprache erlaubt die formale Spezifikation von Verläßlichkeitseigenschaften. Der Nachweis der Verläßlichkeitseigenschaften erfolgt durch Konstruktion und Beweis von Korrektheitskriterien (Verifikationsbedingungen). Die Anwendung von Sprache und System wird beispielhaft an einem Sicherheitsnachweis demonstriert. Es wird nachgewiesen, daß einfache Zugriffsfunktionen auf vertrauliche Daten dem Sicherheitsmodell von Bell und La Padula genügen.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Literatur
Bell, D.E. and LaPadula, L.J.: Secure Computer System: Unified Exposition and Multics Interpretation, ESD-TR-75–306, The MITRE Corporation, 1975.
Cheheyl, M.H. et al: Verifying Security, ACM Computing Surveys vol 13 no 3, 1981.
Damm, W. and Döhmen, G.: AADL: A Net-Based Specification Method for Computer Architecture Design, in: de Bakker, J.W. (ed): Languages for Parallel Architectures: Design, Semantics and Implementation Models, Wiley, 1989.
Goos, G. et al: DIANA An Intermediate Language for Ada, LNCS 161, Springer, Berlin 1983.
Gerhart, S.L. et al: An Overview of AFFIRM: A Specification and Verification System, Information Procesing 80, North Holland, 1980.
Good, D.I.: Revised Report on GYPSY 2.1 (Draft), Technical Report, University of Texas at Austin 1985.
Gramlich, B.: UNICOM: A Refined Completion Based Inductive Theorem Prover, system abstract, Proc. of 10th Int. Conf. on Automated Deduction, Kaiserslautern, 1990, to appear.
Hohlfeld, B., Jonsson, B., Kley, A.: PAS QUALE - Sprachbeschreibung, Technischer Bericht Nr. 12.020/89, Daimler-Benz AG, Forschungsinstitut Ulm, 1989.
Hoare, C.A.R. and Wirth, N.: An Axiomatic Definition of the Programming Language PASCAL, acta informatica 2, 1973.
IT-Sicherheitskriterien, Kriterien für die Bewertung der Sicherheit von Systemen der Informationstechnik (IT), Bundesanzeiger, Köln 1989.
Kersten, H.(ed): Sichere Software, Formale Spezifikation und Verifikation vertrauenswürdiger Systeme, Hüthig, Heidelberg 1990.
Käufl, Th.: Reasoning about Systems of Linear Inequalities, 9th International Conference on Automated Deduction, Lecture Notes on Computer Science, Berlin, Heidelberg, New York: 1988, Springer.
Lehmann, T. and Loeckx, J.: The specification language of OBSCURE, in Sannella, D. and Tarlecki, A.(eds.): Recent Trends in Data Type Specification, Lecture Notes in Computer Science 332, Springer 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hohlfeld, B. (1987). Werkzeuggestützter Nachweis von Verläßlichkeitseigenschaften. In: Pfitzmann, A., Raubold, E. (eds) VIS ’91 Verläßliche Informationssysteme. Informatik-Fachberichte, vol 271. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-76562-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-76562-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53911-7
Online ISBN: 978-3-642-76562-9
eBook Packages: Springer Book Archive