Using Type Enforcement to Assure a Configurable Pipeline

J. Hoffman, P. Greve & R. Smith

Prior to the introduction of guard systems for electronic mail, guards tended to be overly specialized and not versatile enough for today's user community. This paper examines the use of type enforcement to create a highly assured yet configurable guard. Configurable indicates that the administrator is allowed to determine the set and sequence of filters. In order to do this, the administrator must be able to trust that the configuration provided will indeed be followed. This occurs by using highly assured or trusted components.

These trusted components are then linked together via type enforcement to form a pipeline, with one input channel for data to enter the guard, and one separate, connected output channel for data to exit the guard. These channels are connected via assured processes whose behavior is restricted by the type enforcement mechanism. Furthermore, type enforcement is also used to isolate many components of the guard, which simplifies the assurance arguments. This technology is applied in the latest operational guards developed by Secure