Government, Industry, and Academia: Teaming to 
Design High Confidence Information Security Applications




Taylor


Evaluation


This paper 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 Machine (AIM). 
Both MASK and AIM were jointly developed 
by Motorola and the National Security Agency 
(NSA). MASK provides process separation on the 
general purpose processor aboard the AIM chip, 
while AIM provides channel separation between cryptographic 
channels. Furthermore, the paper will begin by 
describing the separation kernel concept and its 
importance to information security. Next it will 
illustrate the Specware formal development methodology used 
in the development of MASK. Experiences and 
lessons learned from this formal development process 
will be discussed. Finally, the results of 
the MASK development process are described, project 
successes are discussed, and related MASK research 
is highlighted.