Formal methods for verification of security functionality

The IT systems of the Swedish Armed Forces often have strong security requirements and there is thus a need for a high level of confidence that the systems work according to specification. To acquire a high level of confidence a thorough verification is needed. Software verification is a complex problem where many different methods and tools need to be used in concert in order to gain a high level of confidence in that the software is correct. Software correctness, regarding both functionality and IT security functions, is crucial when it concerns aspects like personal safety and protection of sensitive information. An extensive effort is usually required to acquire confidence in the quality of the software, especially since both specification and implementation must be examined in depth. This report presents a study that investigates how verification of source code can be carried out practically, using tools that employ formal methods. The work has focused on verifying some selected security features, i.e. individual aspects of IT-security functionality, based on two high-level security goals. The study used source code written in the C programming language that constitute a security component whose functions could fit many IT systems in the Swedish Armed Forces. The tools have a wide range of proof ability, which naturally reflects in the strength of the results produced by the tools. The proof ability also correlates with the complexity of using the tools, where stronger results require more effort from the user. The tools selected were ones that include formal methods considered appropriate for the verification problem, were mature and readily available, and offered support or an active user forum. The study's conclusion is that, using appropriate methodology and knowledgeable personnel, the use of tools employing formal methods can give increased confidence in verification of security-critical software. Formal methods are not appropriate to use solely in the audit phase, in which it can become timeconsuming to reverse engineer requirements and rewrite code. To fully appreciate formal methods as a technique for verification, the method should be incorporated in the development process to write formal requirements and verifiable code. In conclusion, we consider the workload and the difficulty level of using the tools as manageable under these circumstances.