Specification modeling and validation applied to a family of network security products

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. The author describes how the specification modeling and validation tools of the Interactive Specification Acquisition Tools (ISAT) suite are used to help validate members of a particular family of network security gateway products built using widely available open source technologies.