|
Joint work with Guttman and Thayer presented at ESORICS 2000 in Toulouse. Here is the abstract: The IP security protocols (IPsec) may be used via security gateways that apply cryptographic operations to provide security services to datagrams, and this mode of use is supported by an increasing number of commercial products. In this paper, we formalize the types of authentication and confidentiality goal that IPsec is capable of achieving, and we provide criteria that entail that a network with particular IPsec processing achieves its security goals. This requires us to formalize the structure of networks using IPsec, and the state of packets relevant to IPsec processing. We can then prove confidentiality goals as invariants of the formalized systems. Authentication goals are formalized in the manner of [Schneider96], and a simple proof method using ``unwinding sets'' is introduced. We end the paper by explaining the network threats that are prevented by correct IPsec processing. |
|
|
This is an extended abstract (one page) for a five-minute talk I gave at the IEEE Symposium on Security and Privacy in 2002. Here are the slides for that talk. This is joint work with Joshua Guttman. A brief description of the work: Access control is frequently used for basic security even when other measures are absent. Mandatory Access Control (MAC) systems address problems with traditional access control mechanisms by granting full authority over the policy only to a security administrator. Security-Enhanced Linux (SELinux) is an accessible MAC system based on the Linux operating system. SELinux is used by a growing community; however, the security policies can be somewhat complex. Our policy analysis work formalizes the security goals achievable via MAC, and provides a mechanism for formal assurance that a particular policy meets a set of such goals. (While we focus on SELinux, the ideas are applicable to other MAC environments.) Our methods of security policy representation and analysis are simple and powerful. Security goals can be translated into statements of temporal logic and verified via model-checking. Currently, implementation work is ongoing, with the finished tool expected by year-end. |
|
|
Joint work with Guttman presented at the VERIFY 2002 workshop, held at the Federated Logic Conference 2002 in Copenhagen. The abstract of the paper: Achieving a security goal in a networked system requires the cooperation of a variety of devices, each potentially requiring different configurations. Many information security problems may be solved given appropriate models of these devices and their interactions. We present a unique approach, eager formal methods, which front-loads the contribution of formal methods to problem-solving. With eager formal methods, we formally model the network and a class of practically important security goals. The models derived suggest algorithms which, given system configuration information, return security goals satisfied in the system. The formal methods provide rigorous justification, yet the algorithms are implemented as ordinary computer programs. We have applied this approach to several problems; in this extended abstract we briefly describe two: distributed packet filtering and the use of IP security (IPSec) gateways. We have developed and implemented solutions to these two problems separately. We also describe how to unify the two solutions, jointly enforcing these mechanisms on a single network. |