Zusammenfassung
Methoden der Beschreibung von Computer-Systemen und deren Eigenschaften, des Nachweises solcher Eigenschaften und generell der Analyse von Systemen nennen wir formal, wenn sie sich der Sprache und der Methoden der Mathematik, insbesondere der mathematischen Logik, bedienen. Formale Methoden spielen in der Computersicherheit eine herausragende Rolle. Die Bedeutung formaler Methoden für den Nachweis, daß ein Computer-System gewisse Sicherheitsanforderungen erfüllt, ist schon früh erkannt worden. Entsprechend wurde in den Kriterien zur Bewertung der Vertrauenswürdigkeit von Computer-System sowohl für die USA [6] wie auch später für die Bundesrepublik [15] vorgeschrieben, daß bei der Entwicklung von Systemen, die eine der höchsten Qualitätsstufen erreichen sollen, die Anwendung formaler Methoden erforderlich ist.
Dieser Beitrag erörtert formale Methoden im Zusammenhang mit Computersicherheit. Insbesondere geht er darauf ein, warum formale Methoden für den Bereich der Computersicherheit besonders wichtig sind, welche Methoden hier relevant sind, wie der derzeitige Stand des Einsatzes solcher Methoden und zugehöriger Werkzeuge gesehen wird und wie die weitere Entwicklung aussehen könnte.
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.
Similar content being viewed by others
Literaturverweise
W. R. Bevier, W. A. Hunt, J.S. Moore, und W. D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411–428, Dec. 1989.
R. S. Boyer und J S. Moore. A Computational Logic. Academic Press, New York, 1979.
R. S. Boyer und J S. Moore. A Computational Logic Handbook. Academic Press, New York, 1988.
M. Cheheyl et al. Verifying security. Computing Surveys, 13(3):279–339, September 1981.
D. Craigen. m-EVES. In Proc. 10th National Computer Security Conference, pages 109–117, NBS/NCSC, Baltimore, September 1987.
Department of Defense Trusted Computer System Evaluation Criteria. Department of Defense December 1985. DOD 5200.28-STD (supersedes CSC-STD-001-83).
R.J. Feiertag. A Technique for Proving Specifications are Multilevel Secure. Technical Report CSL-109, SRI International, Computer Science Laboratory, January 1980.
R.W. Floyd. Assigning meanings to programs. In J.T. Schwartz, editor, Proceedings of a Symposium in Applied Mathematics, R.W. Floyd, American Mathematical Society, 1967. Vol. 19.
S.L. Gerhart, D.R. Musser, D.H. Thompson, D.A. Baker, R.L. Bates, R.W. Erickson, R.L. London, D.G. Taylor, und D.S. Wile. An overview of AFFIRM: a specification and verification system. In Information Processing 80, S.H. Lavington (Ed.), pages 343–348, October 1980. North Holland Publishing Company.
D. I. Good, R. L. Akers, und L. M. Smith. Report on Gypsy 2.05. Technical Report, Computational Logic, Inc., October 1986.
Guidelines for Formal Verification Systems. National Computer Security Center, April 1989. NCSC-TG-014 Version-1.
J. V. Guttag, J. J. Horning, und J. M. Wing. Larch in five easy pieces. Technical Report 5, DEC Systems Research Center, July 1984.
C. A. R. Hoare. An axiomatic basis of computer programming. Communications of the ACM, 12(10) 576–580, Oct 1969.
S. Igarashi, R.L. London, und D.C. Luckham. Automatic program verification I: logical basis and its implementation. Acta Informatica, 4:145–182, 1975.
IT-Sicherheitskriterien, Kriterien für die Bewertung der Sicherheit von Systemen der Informationstechnik (IT). hrsg. ZSI, Zentralstelle für Sicherheit in der Informationstechnik, Januar 1989.
R. A. Kemmerer. Verification Assessment Study Final Report. Technical Report C3-CR01-86 National Computer Security Center, Ft. Meade, MD., 1986. 5 Volumes.
H. N. Levitt, L. Robinson, und B. Silverberg. The HDM Handbook, vols. I, II, III. Technical Report, Computer Science Laboratory, SRI International, June 1979.
J. Loeckx und H. Sieber. The Foundations of Program Verification. Wiley-Teubner Series in Computer Science, B. G. Teubner, Stuttgart, 1984.
D. C. Luckham, F. W. von Henke, B. Krieg-Brückner, und O. Owe. ANNA — A Language for Annotating Ada programs. Lecture Notes in Computer Science vol. 260, Springer-Verlag, 1987.
L. Marcus, S. D. Crocker, und J. R. Landauer. SDVS: a system for verifying microcode correctness. In 17th Microprogramming Workshop, pages 246–255, IEEE, October 1984.
J. McLean. The specification and modeling of computer security. IEEE Computer, 23(1):9–16, Januar 1990.
D.R. Musser. Aids to hierarchical specification structuring and reusing theorems in AFFIRM-85. In Proceedings VERkshop III pages 2–4, Watsonville, CA., February 1985. Published as ACM Software Engineering Notes, Vol. 10, No. 4, Aug. 1985.
H. Partsch und R. Steinbrueggen. Program transformation Systems. Computing Surveys, 15(3):199–236, 1983.
F. W. von Henke, J. S. Crow, R. Lee, J. M. Rushby, und R. A. Whitehurst. The EHDM verification environment: an overview. In Proc. 11th National Computer Security Conference, NBS/NCSC, Baltimore, October 1988.
D. G. Weber und B. Lubarsky. The SDOS project — verifying hook-up security. In Proc. 3d Aerospace Computer Security Conference, pages 7–14, 1987.
Editor information
Rights and permissions
Copyright information
© 1991 Friedr. Vieweg & Sohn Verlagsgesellschaft mbH, Braunschweig
About this chapter
Cite this chapter
von Henke, F.W. (1991). Entwicklungstendenzen bei formalen Methoden im Bereich der Computersicherheit. In: Cerny, D., Kersten, H. (eds) Sicherheitsaspekte in der Informationstechnik. Vieweg+Teubner Verlag. https://doi.org/10.1007/978-3-322-83911-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-322-83911-4_10
Publisher Name: Vieweg+Teubner Verlag
Print ISBN: 978-3-528-05157-0
Online ISBN: 978-3-322-83911-4
eBook Packages: Springer Book Archive