A formal security model for microprocessor hardware

Author

Lotz, Volkmar ; Kessler, Volker ; Walter, Georg H.

Author_Institution

Corp. Technol., Siemens AG, Munich, Germany

Volume

26

Issue

8

fYear

2000

fDate

8/1/2000 12:00:00 AM

Firstpage

702

Lastpage

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

Keywords

automata theory; data integrity; formal verification; microcomputers; quality management; security of data; theorem proving; E4; ITSEC assurance level; abstract function; application specification; automaton behaviors; confidentiality objectives; data space; evaluation process; formal security model; hardware level; infinite structures; integrity; microprocessor hardware; modeling process; operating system; processor product; security objectives; security policy; security properties; state transition automaton; system model; validity proving; Access control; Application software; Context modeling; Data security; Formal specifications; Hardware; Learning automata; Microprocessors; Operating systems; Quality assurance;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.879809

Filename

879809