Steve Lodin of Roche Diagnostics North America was kind enough to tell me about a newly published paper in the Feb 2005 issue of the International Journal of Information Security entitled "Rigorous Automated Network Security Management", by Joshua D. Guttman and Amy L. Herzog of The MITRE Corporation.
The paper's abstract:
Achieving a security goal in a networked system requires the cooperation of a variety of devices, each device potentially requiring a different configuration. Many information security problems may be solved with appropriate models of these devices and their interactions, and giving a systematic way to handle the complexity of real situations.
We present an approach, rigorous automated network security management, which front-loads formal modeling and analysis before problemsolving, thereby providing easy-to-run tools with rigorously justified results. With this approach, we model the network and a class of practically important security goals. The models derived suggest algorithms which, given system configuration information, determine the security goals satisfied by the system. The modeling provides rigorous justification for the algorithms, which may then be implemented as ordinary computer programs requiring no formal methods training to operate.
We have applied this approach to several problems. In this paper we describe two: distributed packet filtering and the use of IP security (IPsec) gateways. We also describe how to piece together the two separate solutions to these problems, jointly enforcing packet filtering as well as IPsec authentication and confidentiality on a single network.