A multi-level secure message switch with minimal TCB: architectural outline and security analysis

The authors describe an architectural outline for a generic secure message switch. They highlight key security issues germane to the structure and functionality of a switch for routing messages of multiple sensitivity levels over communication media with multiple security levels. The design strives to minimize the trusted computing base (TCB) in order to facilitate formal and informal verification of security policies and to retain data integrity. In particular, the security policy was embedded in the type structure of a specification of the design in PAISLey. Special features of PAISLey´s type system then enabled PAISLey´s type checker to prove the security assertions automatically. The authors also discuss general design principles and a variety of security issues including unauthorized traffic analysis, covert channels, and denial of service