Abstract
This paper presents initial results in a comparative study of formal and conventional techniques in the design of a secure system component: a trusted gateway.
The operation of a trusted gateway is briefly introduced. The industrial context of its development is described, as is the form of the experiment. So far, part-formal and conventional design specifications have been produced for the trusted gateway from a common informal requirements document. As part of this process, queries have been raised against the informal requirements. These have been carefully logged, and form the subject of a preliminary analysis presented here. These first results suggest that the use of a formal specification language (in this case VDM-SL) leads to an an increased number of queries, and a bias in the specifier's concerns towards data rather than design issues.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. C. Bicarregui, J. S. Fitzgerald, P. A. Lindsay, R. Moore, and B. Ritchie. Proof in VDM: A Practitioner's Guide. FACIT. Springer-Verlag, 1994. ISBN 3-540-19813-X.
T. M. Brookes, M. A. Green, J. S.Fitzgerald, and P. G.Larsen. A Comparison of the Conventional and Formal Design of a Secure System Component. FACS Europe, March 1994.
T. Boswell. Specification and Validation of a Security Policy Model. In J. C. P. Woodcock and P. G. Larsen, editors, FME'93: Industrial-Strength Formal Methods, volume 670 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
ISO Document Number ISO/IEC JTC1/SC22/WG19/N-20 Information Technology Programming Languages — VDM-SL First Committee Draft Standard CD 13817-1, November 1993.
P. G. Larsen and P. B. Lassen. An Executable Subset of Meta-IV with Loose Specification. In VDM '91 — Formal Software Development Methods. Springer-Verlag, October 1991.
Office for Official Publications of the European Community. Information Technology Security Evaluation Criteria, June 1991.
P.T. Ward and S.J. Mellor. Structured Development for Real Time Systems, volume 1,2,3. Yourdon Press, Prentice-Hall, Englewood Cliffs, NJ, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fitzgerald, J.S., Brookes, T.M., Green, M.A., Larsen, P.G. (1994). Formal and informal specifications of a secure system component: first results in a comparative study. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_85
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_85
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive