From What to How: A Taxonomy of Formalized Security Properties

TL;DR

The paper tackles the challenge that security properties are treated as high-level SDLC goals and seldom refined through design and operation. It introduces an SDLC-aligned taxonomy of security properties, derived from CAPEC and ATT&CK, and formalizes it in Event-B to enable early verification and refinement across SDLC phases. The taxonomy serves to connect what to preserve with how to preserve, aligning requirements with architectural decisions and eventual implementation, with verification via Rodin and validation via ProB. While promising, the approach faces manual maintenance and non-exhaustive validation, and future work aims to automate updates and broaden scenario coverage including human factors.

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.

Figures (7)

• Figure 1: Security artifacts refinement model
• Figure 2: The long-term objective of the security properties taxonomy
• Figure 3: Extracting and verifying security properties process
• Figure 4: Machine seeing a Context
• Figure 5: The formalized taxonomy classification for the Integrity property and its descendants.