A Few Remarks About Formal Development of Secure Systems

TL;DR

This paper reviews classical challenges in the formal development of secure systems to enhance confidence and better assess the reliability of formal methods in security-critical applications.

Contribution

It provides a critical review of common pitfalls and concerns in formal methods for secure system development, aiming to improve confidence in formal approaches.

Findings

Identifies key 'gotchas' in formal security development

Highlights the importance of careful specification and derivation

Suggests ways to assess confidence in formal methods

Abstract

Formal methods provide remarkable tools allowing for high levels of confidence in the correctness of developments. Their use is therefore encouraged, when not required, for the development of systems in which safety or security is mandatory. But effectively specifying a secure system or deriving a secure implementation can be tricky. We propose a review of some classical `gotchas' and other possible sources of concerns with the objective to improve the confidence in formal developments, or at least to better assess the actual confidence level.