From What to How: A Taxonomy of Formalized Security Properties

• URL: http://arxiv.org/abs/2505.14514v1
• Date: Tue, 20 May 2025 15:42:08 GMT
• Title: From What to How: A Taxonomy of Formalized Security Properties
• Abstract summary: We propose an SDLC taxonomy of security properties that may be used in a self-adaptive context.<n>We use the Event-B formal language to verify and check the correctness of the resulting taxonomy.
• Score: 0.13124513975412253
• License: http://creativecommons.org/licenses/by-sa/4.0/
• 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.

Related papers

• Safin-1: Safety from Within through Memory-Native State Evolution [51.221955257147414]
  Safin-1 is a family of foundation models realizing this principle through memory routing and state evolution.<n> Safin-1 is built on Memory-Anchor Routing across Context History (MARCH), a network architecture that maintains structured memory states.<n>We investigate this interface on downstream safety tasks through a Safety State, demonstrating effective state-based adaptation with substantial safety improvements.
  arXiv  Detail & Related papers  (2026-08-31T13:48:48Z)
• Towards Trustworthy Embodied Intelligence: A Systems Framework and Graded Trustworthiness Levels [53.63220028820581]
  Embodied intelligence integrates learned perception and decision making with real-time computation, control, and physical interaction.<n>We define trustworthy embodied intelligence as the sustained capacity to execute specified tasks reliably.
  arXiv  Detail & Related papers  (2026-07-28T17:50:44Z)
• SeClaw: Spec-Driven Security Task Synthesis for Evaluating Autonomous Agents [87.26967184869198]
  SeClaw is a framework that combines specification-driven security task synthesis with execution-based security evaluation for Autonomous agents.<n> benchmark covers risks arising from resources, user tasks, environments, and intrinsic agent behaviors.
  arXiv  Detail & Related papers  (2026-06-01T14:23:42Z)
• Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin [0.9339654135645749]
  Security is critical for everything relying on modern digital systems.<n>Tools such as ProVerif and Tamarin are widely employed to perform automated verification.<n>This work advances the state of the art by bridging the gap between theoretical security property definitions and their practical, executable verification models.
  arXiv  Detail & Related papers  (2026-05-28T06:57:08Z)
• Referential Security as a New Paradigm for AI Evaluations [5.748110232428846]
  We propose referential security as a new paradigm for AI evaluation.<n>This approach reframes model identity as an empirically verifiable property and separates referential stability from the substantive security claims it conditions.
  arXiv  Detail & Related papers  (2026-05-25T10:24:10Z)
• SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
  Reasoning language models (RLMs) are increasingly used in programming.<n>Yet, even state-of-the-art RLMs frequently introduce critical security vulnerabilities in generated code.<n>We present SecPI, a fine-tuning pipeline that teaches RLMs to internalize structured security reasoning.
  arXiv  Detail & Related papers  (2026-04-04T04:29:11Z)
• A Framework for Formalizing LLM Agent Security [46.86073273904095]
  Security in LLM agents is inherently contextual.<n>Existing definitions of security attacks against LLM agents often fail to capture this contextual nature.<n>We present a framework that systematizes existing attacks and defenses from the perspective of contextual security.
  arXiv  Detail & Related papers  (2026-03-19T21:01:49Z)
• ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification [37.252166064253196]
  ATLAS bridges standardized threat modeling and property-based formal verification for System-on-Chip (SoC) security.<n>By combining asset-centric analysis with threat model templates and multi-source context, ATLAS automates the transformation from vulnerability reasoning to formal proof.
  arXiv  Detail & Related papers  (2026-03-01T16:20:47Z)
• Contextual Safety Reasoning and Grounding for Open-World Robots [79.98924225712668]
  CORE is a safety framework that enables online contextual reasoning, grounding, and enforcement without prior knowledge of the environment.<n>We provide probabilistic safety guarantees for CORE that account for perceptual uncertainty.<n>We demonstrate through simulation and real-world experiments that CORE enforces contextually appropriate behavior in unseen environments.
  arXiv  Detail & Related papers  (2026-02-23T15:51:23Z)
• PoSafeNet: Safe Learning with Poset-Structured Neural Nets [49.854863600271614]
  existing approaches often enforce multiple safety constraints uniformly or via fixed priority orders, leading to infeasibility and brittle behavior.<n>We formalize this setting as poset-structured safety, modeling safety constraints as a partially ordered set and treating safety composition as a structural property of the policy class.<n>Building on this formulation, we propose PoSafeNet, a differentiable neural safety layer that enforces safety via sequential closed-form projection.
  arXiv  Detail & Related papers  (2026-01-29T22:03:32Z)
• LAsset: An LLM-assisted Security Asset Identification Framework for System-on-Chip (SoC) Verification [1.7639836127386677]
  LAsset is a novel framework that identifies security assets from both hardware design specifications and register-transfer level (RTL) descriptions.<n>It achieves high classification accuracy, reaching up to 90% recall rate in system-on-chip (SoC) design, and 93% recall rate in IP designs.
  arXiv  Detail & Related papers  (2026-01-06T00:53:23Z)
• Generalized Security-Preserving Refinement for Concurrent Systems [36.14488865240512]
  We present a refinement-based compositional approach to prove that IFS properties are preserved between implementation and abstraction.<n>We apply our approach to verify two non-preserving case studies against a collection of security policies.
  arXiv  Detail & Related papers  (2025-11-10T09:06:01Z)
• Beyond Algorithmic Proofs: Towards Implementation-Level Provable Security [1.338174941551702]
  We present Implementation-Level Provable Security, a new paradigm that defines security in terms of structurally verifiable resilience against real-world attack surfaces during deployment.<n>We present SEER (Secure and Efficient Encryption-based Erasure via Ransomware), a file destruction system that repurposes and reinforces the encryption core of Babuk ransomware.
  arXiv  Detail & Related papers  (2025-08-02T01:58:06Z)
• Provably Secure Retrieval-Augmented Generation [7.412110686946628]
  This paper proposes the first provably secure framework for Retrieval-Augmented Generation (RAG) systems.<n>Our framework employs a pre-storage full-encryption scheme to ensure dual protection of both retrieved content and vector embeddings.
  arXiv  Detail & Related papers  (2025-08-01T21:37:16Z)
• LLM Agents Should Employ Security Principles [60.03651084139836]
  This paper argues that the well-established design principles in information security should be employed when deploying Large Language Model (LLM) agents at scale.<n>We introduce AgentSandbox, a conceptual framework embedding these security principles to provide safeguards throughout an agent's life-cycle.
  arXiv  Detail & Related papers  (2025-05-29T21:39:08Z)
• Towards Safety Reasoning in LLMs: AI-agentic Deliberation for Policy-embedded CoT Data Creation [70.62656296780074]
  We propose AIDSAFE: Agentic Iterative Deliberation for Safety Reasoning, a novel data generation recipe.<n>A data refiner stage in AIDSAFE ensures high-quality outputs by eliminating repetitive, redundant, and deceptive thoughts.<n>Our evaluations demonstrate that AIDSAFE-generated CoTs achieve superior policy adherence and reasoning quality.
  arXiv  Detail & Related papers  (2025-05-27T21:34:40Z)
• A Framework for the Security and Privacy of Biometric System Constructions under Defined Computational Assumptions [1.5446015139136167]
  This paper introduces a formal framework for constructing secure and privacy-preserving biometric systems. By leveraging the principles of universal composability, we enable the modular analysis and verification of individual system components.
  arXiv  Detail & Related papers  (2024-11-26T11:10:11Z)
• SafetyAnalyst: Interpretable, transparent, and steerable safety moderation for AI behavior [56.10557932893919]
  We present SafetyAnalyst, a novel AI safety moderation framework.<n>Given an AI behavior, SafetyAnalyst uses chain-of-thought reasoning to analyze its potential consequences.<n>It aggregates all harmful and beneficial effects into a harmfulness score using fully interpretable weight parameters.
  arXiv  Detail & Related papers  (2024-10-22T03:38:37Z)
• Realizable Continuous-Space Shields for Safe Reinforcement Learning [13.728961635717134]
  We present the first shielding approach specifically designed to ensure the satisfaction of safety requirements in continuous state and action spaces.<n>Our method builds upon realizability, an essential property that confirms the shield will always be able to generate a safe action for any state in the environment.
  arXiv  Detail & Related papers  (2024-10-02T21:08:11Z)
• Data Reconstruction: When You See It and When You Don't [75.03157721978279]
  We aim to "sandwich" the concept of reconstruction attacks by addressing two complementing questions.<n>We introduce a new definitional paradigm -- Narcissus Resiliency -- to formulate a security definition for protection against reconstruction attacks.
  arXiv  Detail & Related papers  (2024-05-24T17:49:34Z)
• Security Properties through the Lens of Modal Logic [4.548429316641551]
  We introduce a framework for reasoning about the security of computer systems using modal logic. We show how to use our formalism to represent various variants of confidentiality, integrity, robust declassification and transparent endorsement.
  arXiv  Detail & Related papers  (2023-09-18T07:37:12Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• Quantifying Assurance in Learning-enabled Systems [3.0938904602244355]
  Dependability assurance of systems embedding machine learning components is a key step for their use in safety-critical applications. This paper develops a quantitative notion of assurance that an LES is dependable, as a core component of its assurance case. We illustrate the utility of assurance measures by application to a real world autonomous aviation system.
  arXiv  Detail & Related papers  (2020-06-18T08:11:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.