Research / Paper Files

Paper Files

Paper Files are a personal practice of continuous study in cybersecurity that applies the scientific method as a learning tool. Each article is written not for academic publication, but as a deliberate exercise to sharpen the axe — deepening knowledge on specific topics, organizing ideas with rigor, and observing how understanding of certain subjects develops over time. It is the intellectual equivalent of a training journal: each entry records what was studied, how it was analyzed, and what conclusions emerged.

I strongly recommend that security professionals adopt this method. Choose a topic you want to master, research primary sources (RFCs, papers, official documentation), structure your text with introduction, methodology, analysis, and conclusion, and write as if you were explaining to a colleague. The act of writing forces clarity of thought and exposes gaps in understanding that passive reading cannot reveal. Use the articles on this site as examples of format and depth, and build your own collection — over time, you will have a personal repository of refined knowledge that no course or certification can replace.

DAI & ADAI · 2026

AllDetectionDFIRAppSecDevSecOpsAI SecurityIAMCloudContainersIRCryptoResearchPhishingSecrets

226 papers

Containers

A Formal Architecture for Attack Detection and Containment in Container Environments Based on Compositional Attack Surface Modeling

TITLE: A Formal Architecture for Attack Detection and Containment in Container Environments Based on Compositional Attack Surface Modeling ABSTRACT: The massive adoption of containers and orchestrators such as Kubernetes has consolidated the cloud-native paradigm as the predominant infrastructure in corporate environments by 2025. Although the lightweight virtualization model provides operational efficiency and elasticity, kernel sharing and the dynamic nature of clusters significantly expand the attack surface. Recent incidents involving container escape, exploitation of Linux kernel vulnerabilities, and intra-cluster lateral movement demonstrate the need for detection and containment mechanisms with formal grounding and explicit guarantees. In this work, we propose a formal architecture for attack detection and containment in container environments based on compositional attack surface modeling. We formalize the environment as an annotated directed graph that integrates containers, infrastructure nodes, and interaction channels, defining the attack surface as a compositional operator over vertices and edges. We introduce a detection method based on structural deviations in system call graphs, using spectral divergence between observed adjacency matrices and reference models learned during a baseline phase. We demonstrate formal properties under explicit hypotheses, including a conditional completeness theorem. We implemented a prototype integrated with Kubernetes 1.29 with monitoring via eBPF/libbpf and evaluated the system in a 64-node cluster running 1,200 containers. The results indicate an average detection rate above 95% for scenarios aligned with MITRE ATT&CK for Containers, with a false positive rate below 3% and an average CPU overhead of 3.8%. We discuss implications for integration with CNAPP platforms and security governance mechanisms, as well as limitations and evasion vectors. We conclude that formal compositional modeling, combined with efficient kernel-level monitoring, provides a rigorous and scalable basis for protecting large-scale containerized environments.

Read paper →
Containers

A Formal Architecture for Detection and Containment of Attacks in Container Environments Based on Compositional Modeling of the Attack Surface

TITLE: A Formal Architecture for Detection and Containment of Attacks in Container Environments Based on Compositional Modeling of the Attack Surface ABSTRACT: The massive adoption of containers and orchestrators such as Kubernetes has consolidated the cloud-native paradigm as the predominant infrastructure in corporate environments by 2025. Although the lightweight virtualization model provides operational efficiency and elasticity, kernel sharing and the dynamic nature of clusters significantly expand the attack surface. Recent incidents involving container escape, exploitation of vulnerabilities in the Linux kernel, and intra-cluster lateral movement demonstrate the need for detection and containment mechanisms with formal grounding and explicit guarantees. In this work, we propose a formal architecture for the detection and containment of attacks in container environments based on compositional modeling of the attack surface. We formalize the environment as an annotated directed graph that integrates containers, infrastructure nodes, and interaction channels, defining the attack surface as a compositional operator over vertices and edges. We introduce a detection method based on structural deviations in system call graphs, using spectral divergence between observed adjacency matrices and reference models learned during a baseline phase. We demonstrate formal properties under explicit hypotheses, including a conditional completeness theorem. We implemented a prototype integrated with Kubernetes 1.29 with monitoring via eBPF/libbpf and evaluated the system on a 64-node cluster running 1,200 containers. The results indicate an average detection rate above 95% for scenarios aligned with MITRE ATT&CK for Containers, with a false positive rate below 3% and an average CPU overhead of 3.8%. We discuss implications for integration with CNAPP platforms and security governance mechanisms, as well as limitations and evasion vectors. We conclude that formal compositional modeling, combined with efficient kernel-level monitoring, provides a rigorous and scalable foundation for protecting large-scale containerized environments.

Read paper →
Containers

A Formal Architecture for Detection and Mitigation of Container Escapes Based on Probabilistic Behavioral Profiles and Kernel-Level Policy Verification

TITLE: A Formal Architecture for Detection and Mitigation of Container Escapes Based on Probabilistic Behavioral Profiles and Kernel-Level Policy Verification ABSTRACT: Container-based virtualization has become a cornerstone of cloud-native infrastructure, but its reliance on a shared kernel imposes structural security challenges. Container escapes remain critical compromise vectors, especially in large-scale Kubernetes environments, where vulnerabilities in the runtime, the cgroups subsystem, or the kernel itself may result in isolation breaches. In this work, we propose a formal architecture for detecting and mitigating container escapes based on probabilistic modeling of system call sequences and automatic synthesis of kernel-level security policies. We model the legitimate behavior of applications as a probabilistic language over the syscall alphabet, instantiated by variable-order Markov chains with Bayesian smoothing. We derive formal bounds of correctness and completeness under $(\epsilon, \delta)$ parameters and introduce a decision criterion based on accumulated log-likelihood. From the observed empirical support, we automatically synthesize minimal seccomp profiles and policies compatible with modern LSMs (AppArmor or SELinux), quantifiably reducing the attack surface. We implement the architecture using eBPF coupled to Linux 6.x kernel tracepoints, integrating it into a Kubernetes 1.28 cluster with containerd 1.7. In an experimental evaluation involving 120 nodes and 1,800 containers, we obtained an average reduction of 72.4% in the set of permitted syscalls, a detection rate of 96.1%, and an average CPU overhead of 3.7%. We further demonstrate that the approach outperforms mechanisms based exclusively on heuristic rules while maintaining scalability and low latency. We conclude that the combination of formal probabilistic modeling, efficient kernel-level verification, and automatic policy synthesis constitutes a robust strategy for the dynamic hardening of containerized environments in 2025.

Read paper →
Containers

A Formal Architecture for Detecting and Mitigating Container Escapes Based on Probabilistic Behavioral Profiles and Kernel Policy Verification

TITLE: A Formal Architecture for Detecting and Mitigating Container Escapes Based on Probabilistic Behavioral Profiles and Kernel Policy Verification ABSTRACT: Container-based virtualization has become a foundation of cloud-native infrastructure, but its reliance on a shared kernel imposes structural security challenges. Container escapes remain critical compromise vectors, especially in large-scale Kubernetes environments, where vulnerabilities in the runtime, the cgroups subsystem, or the kernel itself can result in isolation breaches. In this work, we propose a formal architecture for detecting and mitigating container escapes based on probabilistic modeling of system call sequences and automatic synthesis of security policies at the kernel level. We model legitimate application behavior as a probabilistic language over the syscall alphabet, instantiated by variable-order Markov chains with Bayesian smoothing. We derive formal bounds for correctness and completeness under $(\epsilon, \delta)$ parameters and introduce a decision criterion based on cumulative log-likelihood. From the empirical support observed, we automatically synthesize minimal seccomp profiles and policies compatible with modern LSMs (AppArmor or SELinux), quantitatively reducing the attack surface. We implemented the architecture with eBPF coupled to Linux 6.x kernel tracepoints, integrating it into a Kubernetes 1.28 cluster with containerd 1.7. In an experimental evaluation involving 120 nodes and 1,800 containers, we achieved an average reduction of 72.4% in the set of permitted syscalls, a detection rate of 96.1%, and an average CPU overhead of 3.7%. We further demonstrate that the approach outperforms mechanisms based exclusively on heuristic rules, while maintaining scalability and low latency. We conclude that the combination of formal probabilistic modeling, efficient kernel-level verification, and automatic policy synthesis constitutes a robust strategy for dynamic hardening of containerized environments in 2025.

Read paper →
Cloud

Operational Threat Modeling and Telemetry-Based Detection for Multi-Cloud Environments: Practical Defense Strategies in IaaS, PaaS, and Kubernetes Infrastructures (2025)

TITLE: Operational Threat Modeling and Telemetry-Based Detection for Multi-Cloud Environments: Practical Defense Strategies in IaaS, PaaS, and Kubernetes Infrastructures (2025) ABSTRACT: Cloud computing has become the dominant operational substrate for corporate infrastructure, digital services, and artificial intelligence platforms. In 2025, multi-cloud and hybrid environments combining AWS, Microsoft Azure, and Google Cloud Platform (GCP) are common, while cloud-native architectures based on containers, Kubernetes, and serverless functions significantly expand the attack surface. This paper presents an operational cloud security analysis focused on threat modeling, risk formalization, and the practical implementation of telemetry-based detection and response mechanisms. The research examines recurring attack vectors observed in red teaming and incident response operations between 2021 and 2025, including abuse of IAM identities, exfiltration via cloud APIs, compromise of Kubernetes workloads, and exploitation of misconfigurations in storage and virtual networks. We propose a formal risk assessment model adapted for cloud environments that combines exposure, privilege, and observability metrics, expressed mathematically to enable automated mitigation prioritization. The methodology includes collection of native telemetry (CloudTrail, Azure Activity Logs, GCP Audit Logs), runtime instrumentation with eBPF, and behavioral detection based on rules aligned with the MITRE ATT&CK for Cloud framework. The study describes a practical implementation using widely adopted tools up to 2025, including Falco, ScoutSuite, kube-bench, and SIEM analysis pipelines. We experimentally evaluate the approach in a simulated multi-cloud environment containing Kubernetes workloads and serverless services, demonstrating a significant reduction in mean time to detect (MTTD) and improved risk prioritization. We also present a realistic case study based on patterns observed in public incidents involving exposed credentials and abuse of cloud APIs. The results indicate that the combination of formal risk modeling with granular telemetry and Zero Trust controls provides substantial gains in the operational resilience of cloud environments. The work contributes a practical framework for offensive and defensive security teams operating in complex cloud infrastructures, aligned with the state of the art in the security ecosystem up to 2025.

Read paper →
Cloud

Operational Threat Modeling and Telemetry‑Based Detection for Multi‑Cloud Environments: Practical Defense Strategies in IaaS, PaaS, and Kubernetes Infrastructures (2025)

TITLE: Operational Threat Modeling and Telemetry‑Based Detection for Multi‑Cloud Environments: Practical Defense Strategies in IaaS, PaaS, and Kubernetes Infrastructures (2025) ABSTRACT Cloud computing has become the dominant operational substrate for corporate infrastructure, digital services, and artificial intelligence platforms. In 2025, multi‑cloud and hybrid environments combining AWS, Microsoft Azure, and Google Cloud Platform (GCP) are common, while cloud‑native architectures based on containers, Kubernetes, and serverless functions significantly expand the attack surface. This paper presents an operational analysis of cloud security focused on threat modeling, risk formalization, and the practical implementation of telemetry‑based detection and response mechanisms. The research examines recurring attack vectors observed in red teaming and incident response operations between 2021 and 2025, including abuse of IAM identities, exfiltration via cloud APIs, compromise of Kubernetes workloads, and exploitation of misconfigurations in storage and virtual networks. We propose a formal risk assessment model adapted for cloud environments that combines metrics of exposure, privilege, and observability, mathematically expressed to enable automated mitigation prioritization. The methodology includes the collection of native telemetry (CloudTrail, Azure Activity Logs, GCP Audit Logs), runtime instrumentation with eBPF, and behavioral detection based on rules aligned with the MITRE ATT&CK for Cloud framework. The study describes a practical implementation using tools widely adopted up to 2025, including Falco, ScoutSuite, kube‑bench, and analysis pipelines in SIEM. We experimentally evaluate the approach in a simulated multi‑cloud environment containing Kubernetes workloads and serverless services, demonstrating a significant reduction in mean time to detection (MTTD) and improved risk prioritization. We also present a realistic case study based on patterns observed in public incidents involving exposed credentials and abuse of cloud APIs. The results indicate that the combination of formal risk modeling with granular telemetry and Zero Trust controls provides substantial gains in the operational resilience of cloud environments. This work contributes a practical framework for offensive and defensive security teams operating in complex cloud infrastructures, aligned with the state of the art of the security ecosystem through 2025.

Read paper →
Cloud

A Formal Architecture for Adaptive Threat Detection and Containment in Multi-Cloud Environments Based on Temporal Graphs and Verifiable Policies

TITLE: A Formal Architecture for Adaptive Threat Detection and Containment in Multi-Cloud Environments Based on Temporal Graphs and Verifiable Policies ABSTRACT: The adoption of multi-cloud and hybrid strategies has become a dominant practice in critical sectors, increasing the semantic and operational complexity of access control and security monitoring mechanisms. The heterogeneity among AWS IAM, Microsoft Entra ID/Azure RBAC, Google Cloud IAM, and RBAC/ABAC models in Kubernetes, combined with identity federation, CI/CD pipelines, and API-driven integrations, introduces temporal and cross-cutting dependencies that are not captured by local policy analyses. Recent reports indicate that the misuse of valid credentials remains the predominant attack vector in incidents, often exploiting legitimate compositions of permissions. We propose a formal architecture for adaptive threat detection and containment based on temporal privilege graphs and automated policy verification via SMT. We formalize the multi-cloud environment as a dynamic system G_t = (V_t, E_t, τ_t, w_t, ℓ_t), defining compromise paths, accumulated temporal risk, and the dual problem of detection and containment as instances of reachability and minimum cut under functional constraints. We demonstrate partial correctness properties and a reduction to maximum flow for minimum containment. We present an incremental algorithm with sublinear amortized complexity analysis under sparsity and temporal locality assumptions. Containment is validated by encoding organizational invariants in decidable first-order logic, solved by SMT. We implemented a prototype in Kubernetes 1.29 with a graph backend and integration with OPA and MITRE ATT&CK taxonomies. Empirical evaluations with anonymized real logs and synthetic scenarios show a statistically significant reduction in detection time compared to approaches based exclusively on correlation. Case studies in the financial and healthcare sectors illustrate the ability to block attack chains while preserving functional requirements. The proposal contributes to the convergence of identity-based security, formal verification, and automated response in contemporary multi-cloud ecosystems.

Read paper →
Cloud

Formally Verifiable Detection of Configuration Drift and Attack Chains in Multi‑Cloud Environments Based on Dependency Graphs and Probabilistic Inference

1. Introduction

Read paper →
Cloud

A Formally Verifiable Architecture for Detection and Mitigation of Lateral Movement in Multi-Cloud Environments Based on Distributed Telemetry, Temporal Verification, and Compositional Analysis

1. Introduction

Read paper →
IAM

Adaptive Identity and Access Management Architecture with Continuous Graph-Based Risk Assessment and Formal Policies for Multicloud Environments

1. Introduction

Read paper →
IAM

A Formally Verifiable Architecture for Adaptive Identity and Access Management with Quantitative Security Guarantees in Multi-Cloud Environments

1. Introduction

Read paper →
IAM

Adaptive and Formally Verifiable Architecture for Identity and Access Management with Risk-Oriented Privilege Minimization

1. Introduction

Read paper →
IAM

IAM-GraphSec: A Formal, Verifiable, and Scalable Architecture for Adaptive Identity Governance and Attack Surface Minimization in Multi-Cloud Environments

1. Introduction

Read paper →
AI Security

Formal Architecture for Security of Artificial Intelligence Systems: A Quantitative Framework for Mitigation of Adversarial Attacks, Data Poisoning, Exploitation, and Threats to Foundation Models in Critical Environments

1. Introduction

Read paper →
AI Security

Formal Architecture for Security of Artificial Intelligence Systems: Threat Modeling, Adversarial Robustness, and Integrated Cryptographic Guarantees

1. Introduction

Read paper →
AI Security

FORMALLY GROUNDED ARCHITECTURE FOR MACHINE LEARNING MODEL SECURITY: UNIFIED DETECTION AND MITIGATION OF ADVERSARIAL, POISONING, AND MODEL EXTRACTION ATTACKS

1. Introduction

Read paper →
AI Security

A Formally Grounded Architecture for Security of Artificial Intelligence Systems: Integrated Mitigation of Data Poisoning and Adversarial Attacks with Quantitative Guarantees

1. Introduction

Read paper →
AI Security

Operational Security of Large Language Models: Threat Modeling, Adversarial Exploitation, and Defensive Architectures for AI Systems in Enterprise Cyber Environments

1. Introduction

Read paper →
DevSecOps

A Formally Verifiable Architecture for DevSecOps Orchestration with Quantitative Risk Prioritization and Threat-Oriented Continuous Integration

1. Introduction Digital transformation has accelerated the adoption of distributed architectures, microservices, containerization, and infrastructure as code (IaC), resulting in increasingly shorter and highly automated development cycles. The DevOps paradigm has consolidated itself as a response to the need to reduce time-to-market, promoting continuous integration (CI) and continuous delivery (CD) (GITLAB, 2024). However, the late insertion of security controls into these pipelines has substantially expanded the attack surface, especially in cloud-native and API-oriented environments. Wi

Read paper →
DevSecOps

Formal Orchestration of Security Controls in DevSecOps Pipelines: A Framework Based on Threat Modeling, Multi-Objective Optimization, and Continuous Verification

maximize_detection_probability: true ``` This abstraction enables the orchestration engine to map policies onto platform-specific controls. For example: • artifact signing may use Sigstore in Kubernetes clusters • binary authorization in Google Cloud • custom signing services in on-premise environments The mapping function can be represented as $$ f : P \rightarrow C_{platform} $$ where $P$ represents abstract policy requirements and $C_{platform}$ represents concrete security control implementations supported by a given environment. Finally, cross-platform orchestration becomes part

Read paper →
DevSecOps

Risk-Oriented DevSecOps with Continuous Formal Verification: A Quantitative Model for Adaptive Security Orchestration in CI/CD Pipelines

1. Introduction The consolidation of DevOps practices, combined with the widespread adoption of architectures based on microservices, containers, and infrastructure as code (IaC), has structurally transformed the software development lifecycle. By 2026, organizations operate highly automated CI/CD pipelines, frequently integrated with CNAPP (Cloud-Native Application Protection Platforms) and observability mechanisms based on eBPF. However, the compression of time between commit and deploy amplifies the attack surface and increases the probability of exposure to known and misconfiguration vuln

Read paper →
DevSecOps

Evidence-Oriented DevSecOps: A Formal Architecture with Contextual Risk-Based Prioritization and Continuous Verification for Large-Scale Software Delivery Pipelines (2026)

DeploymentVerification DeploymentVerification --> RuntimeMonitoring RuntimeMonitoring --> IncidentResponse RuntimeMonitoring --> ContinuousVerification ContinuousVerification --> StaticAnalysis IncidentResponse --> [] ``` Within this model, the ContinuousVerification state performs consistency checks on previously generated evidence artifacts. If verification fails, the system transitions to IncidentResponse. We define the pipeline correctness invariant as follows: $$ \forall s_i \in S,\ Integrity(E_i) \land PolicyCompliance(E_i) $$ Where: - $Integrity(E_i)$ verifie

Read paper →
Research

Operational Cybersecurity Research in the Era of AI-Augmented Threats: A Practical Framework for Empirical Threat Hunting, Detection Engineering, and Adversarial Simulation (2026)

1. Introduction Cybersecurity research has evolved dramatically over the past two decades, transitioning from a discipline primarily focused on cryptography and protocol analysis into a complex operational science encompassing adversarial modeling, telemetry analytics, large-scale distributed systems, and cyber-physical risk management. The emergence of cloud-native architectures, containerized workloads, software supply-chain dependencies, and identity-centric infrastructures has significantly expanded the attack surface available to adversaries. Simultaneously, attackers have adopted increa

Read paper →
AppSec

Operationalizing Application Security in the AI‑Augmented Software Supply Chain: Practical AppSec Architecture, Threat Modeling, and Empirical Evaluation (2026)

DeploymentVerification DeploymentVerification --> RuntimeMonitoring RuntimeMonitoring --> [] ``` Each transition includes verification predicates ensuring integrity and compliance. Correctness Proof Sketch Theorem 1: Pipeline Integrity Preservation Given cryptographically signed artifacts and verified stage transitions, the pipeline preserves artifact integrity. Proof Assume: 1. Initial artifact $A_0$ is trusted. 2. Each stage verifies artifact signature before transformation. 3. New artifacts are signed after transformation. Then for stage $i$: $$ Verify(Sign(A_i)) = True $$ and af

Read paper →