Aarhus University Seal / Aarhus Universitets segl

Formal Methods in Security Survey

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

In today’s world, critical infrastructure is often controlled by computing systems. This introduces
new risks for cyber attacks, which can compromise the security and disrupt the functionality of these systems.
It is therefore necessary to build such systems with strong guarantees of resiliency against cyber attacks.
One way to achieve this level of assurance is using formal verification, which provides proofs of system
compliance with desired cyber security properties. The use of Formal Methods (FM) in aspects of cyber
security and safety-critical systems are reviewed in this article. We split FM into the three main classes:
theorem proving, model checking and lightweight FM. To allow the different uses of FM to be compared,
we define a common set of terms. We further develop categories based on the type of computing system FM
are applied in. Solutions in each class and category are presented, discussed, compared and summarised.
We describe historical highlights and developments and present a state-of-the-art review in the area of FM
in cyber security. This review is presented from the point of view of FM practitioners and researchers,
commenting on the trends in each of the classes and categories. This is achieved by considering all types
of FM, several types of security and safety critical systems and by structuring the taxonomy accordingly.
The article hence provides a comprehensive overview of FM and techniques available to system designers of
security-critical systems, simplifying the process of choosing the right tool for the task. The article concludes
by summarising the discussion of the review, focusing on best practices, challenges, general future trends
and directions of research within this field.
Original languageEnglish
JournalFormal Aspects of Computing
Publication statusSubmitted - 4 Jul 2020

See relations at Aarhus University Citationformats

ID: 193489268