From What to How: A Taxonomy of Formalized Security Properties

TL;DR

This paper introduces a structured taxonomy of security properties within the SDLC, aiming to refine high-level security goals into detailed artifacts and verify them using formal methods for better alignment with system defenses.

Contribution

It proposes a novel SDLC taxonomy of security properties and a methodology for defining and verifying it using Event-B formal language.

Findings

The taxonomy aligns security properties with attacks and defenses.

Formal verification confirms the correctness of the taxonomy.

Enhances security requirements refinement in SDLC.

Abstract

Confidentiality, integrity, availability, authenticity, authorization, and accountability are known as security properties that secure systems should preserve. They are usually considered as security final goals that are achieved by system development activities, either in a direct or an indirect manner. However, these security properties are mainly elicited in the high-level requirement phase during the System Development Life Cycle (SDLC) and are not refined throughout the latter phases as other artifacts such as attacks, defenses, and system assets. To align security properties refinement with attacks, defenses, and system assets refinements, we propose an SDLC taxonomy of security properties that may be used in a self-adaptive context and present the methodology for defining it. To verify and check the correctness of the resulting taxonomy, we use the Event-B formal language.