Applying formal methods to an information security device: an experience report

One approach to assuring information security is to control access to information through an appropriately designed device. Acost-e ective way to provide assurance that the device meets its security requirements is to detect and correct violations of these requirements at an early stage of development: when the operational requirements are speci ed. Once it is demonstrated that an operational requirements speci cation is complete and consistent, that it captures the intended device behavior, and that the operational speci cation satis es the security requirements, this operational speci cation can be used both to guide development of implementations and to generate test sets for testing implementations. This paper describes the application of the SCR (Software Cost Reduction) requirements method and the NRL's SCR * toolset, which includes a set of veri cation and validation tools, to a US Navy communications security device. It reports on our success in proving that the operational requirements speci cation satis es a set of security properties. The paper also discusses the practicality and cost of applying formal methods to the development of security devices.