Formal construction of the Mathematically Analyzed Separation Kernel

Author

Martin, W. ; White, P. ; Taylor, E.S. ; Goldberg, A.

fYear

2000

fDate

2000

Firstpage

133

Lastpage

141

Abstract

Describes the formal specification and development of a separation kernel. The Mathematically Analyzed Separation Kernel (MASK), has been used by Motorola on a smartcard project, and as part of a hardware cryptographic platform called the Advanced INFOSEC (INFOrmation SECurity) Machine (AIM). Both MASK and AIM were jointly developed by Motorola and the National Security Agency (NSA). This paper first describes the separation kernel concept and its importance to information security. Next, it illustrates the Specware formal development methodology that was used in the development of MASK. Experiences and lessons learned from this formal development process are discussed. Finally, the results of the MASK development process are described, project successes are discussed, and related MASK research is highlighted

Keywords

cryptography; firmware; formal specification; operating system kernels; smart cards; AIM; Advanced INFOSEC Machine; MASK development process; Mathematically Analyzed Separation Kernel; Motorola; National Security Agency; Specware formal development methodology; formal specification; hardware cryptographic platform; information security; smartcard project; Books; Certification; Context; Cryptography; Data security; Hardware; Information security; Kernel; National security; Operating systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 2000. Proceedings ASE 2000. The Fifteenth IEEE International Conference on

Conference_Location

Grenoble

ISSN

1938-4300

Print_ISBN

0-7695-0710-7

Type

conf

DOI

10.1109/ASE.2000.873658

Filename

873658