This Article 
 Bibliographic References 
 Add to: 
A Formal Security Model for Microprocessor Hardware
August 2000 (vol. 26 no. 8)
pp. 702-712

Abstract—The paper introduces a formal security model for a microprocessor hardware system. The model has been developed as part of the evaluation process of the processor product according to ITSEC assurance level E4. Novel aspects of the model are the need for defining integrity and confidentiality objectives on the hardware level without the operating system or application specification and security policy being given, and the utilization of an abstract function and data space. The security model consists of a system model given as a state transition automaton on infinite structures and the formalization of security objectives by means of properties of automaton behaviors. Validity of the security properties is proved. The paper compares the model with published ones and summarizes the lessons learned throughout the modeling process.

[1] D.E. Bell and L. LaPadula, “Secure Computer Systems: Unified Exposition and Multics Interpretation.” NTIS AD-A023588, MTR 2997, ESD-TR-75-306, MITRE Corporation, Bedford, Mass. 1976.
[2] D.E. Bell, "Concerning 'Modelling' of Computer Security," IEEE Computer Society Symp. Security and Privacy, 1988, pp. 8-13, at p. 12.
[3] K.J. Biba, “Integrity Considerations for Secure Computer Systems,” NTIS AD-A039 324, MTR 3153, ESD-TR-76-372, MITRE Corporation, Bedford, Mass. 1977.
[4] “Towards a Logical Basis for Systems Engineering,” Calculational System Design, M. Broy ed., NATO ASI Series F, 1998.
[5] D.C. Clark and D.R. Wilson, “Evolution of a Model for Computer Integrity,” Technical Report, Invitational Workshop on Data Integrity, Section A2, pp. 1-3, 1989.
[6] D. Denning,"A lattice model of secure information flow," Comm. ACM, vol. 19, no. 5, pp. 236-243, 1976.
[7] J.A. Goguen and J. Meseguer, “Security Policies and Security Models,” Proc. IEEE Symp. Security and Privacy, pp. 11-20, 1982.
[8] Commission of the European Communities. Information Technology Security Evaluation Criteria (ITSEC), June, 1991.
[9] V. Kessler, “On the Chinese Wall Model,” Proc. Second European Symp. Research in Computer Security, pp. 41-54, 1992.
[10] V. Kessler and S. Mund, “Sicherheitsmodelle-Baupläne für die Entwicklung sicherer Systeme,” Siemens AG, Zentralabteilung Forschung und Entwicklung, München, 1993.
[11] V. Lotz, V. Kessler, and G. Walter, “Ein Formales Sicherheitsmodell,” internal report, 1999.
[12] J. McLean, “Reasoning about Security Models,” Proc. IEEE Symp. Security and Privacy, pp. 123-131, 1987.
[13] The MULTOS web site,
[14] L.C. Paulson, “The Inductive Approach to Verifying Cryptographic Protocols,” J. Computer Security 6, pp. 85-128, 1998.
[15] S. Schneider, “Security Properties and CSP,” Proc. IEEE Symp. Security and Privacy, 1996.
[16] S.W. Smith and V. Austel, “Trusting Trusted Hardware: Towards a Formal Model for Programmable Secure Coprocessors,” Proc. Third USENIX Workshop Electronic Commerce, 1998.
[17] Terry and P.S. Wiseman, “A New Security Policy Model,” Proc. IEEE Symp. Security and Privacy, pp. 215-228, 1989.
[18] W. Thomas, “Automata on Infinite Objects,” Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, Jan van Leeuwen, ed., Amsterdam 1990.

Index Terms:
Security, hardware, formal security models.
Volkmar Lotz, Volker Kessler, Georg H. Walter, "A Formal Security Model for Microprocessor Hardware," IEEE Transactions on Software Engineering, vol. 26, no. 8, pp. 702-712, Aug. 2000, doi:10.1109/32.879809
Usage of this product signifies your acceptance of the Terms of Use.