Abstract
A high-bandwidth, always-on Internet connection makes computers in homes and small offices attractive targets for network-based attacks. Network security gateways can protect such vulnerable hosts from attackers, but differing sets of customer needs require different feature mixes. The safest way to address this market is to provide a family of products, each member of which requires little or no end-user configuration. Since the products are closely related, the effort to validate n of them should be much less than n times the effort to validate one; however, validating the correctness and security of even one such device is notoriously difficult, due to the oft-observed fact that no practical amount of testing can show the absence of security flaws. One would instead like to prove security properties, even when the products are implemented using off-the-shelf technologies that don?t lend themselves to formal reasoning. In this paper, I describe how I use the specification modeling and validation tools of the Interactive Specification Acquisition Tools (ISAT) suite to help validate members of a particular family of network security gateway products built using widely available open source technologies.