Deploying secure communication protocols remains a challenging task. To ensure that intended security properties hold, formal verification has become increasingly important. In this work, we present a translation from the design-oriented Alice Bob language to the implementation-level language F*, leveraging the DY* library’s verification capabilities. Our approach addresses the expressiveness gap between abstract specifications and concrete implementations by generating verifiable F* code that benefits from its dependent-type system. This integration of model-driven development with dependent types enables the specification and proof of security properties directly at the implementation level. As a result, users, even those without expertise in formal methods, can start from an intuitive Alice Bob notation and obtain a formally backed implementation that can be enriched with features not expressible in Alice Bob, while preserving correctness through re-verification. We demonstrate the effectiveness of this workflow through the generation and verification of several real-world security protocols, showcasing an end-to-end approach to verified protocol implementation.
The expansion of Internet of Things (IoT) applications in sixth-generation (6G) networks creates new security risks that centralized intrusion detection systems cannot adequately address due to scalability limits, communication overhead, and privacy exposure. We propose a federated learning (FL)-based intrusion detection framework augmented with differential privacy (DP) to protect sensitive data while supporting large-scale IoT deployments. The framework trains models collaboratively across distributed nodes with privacy-preserving updates. Evaluation on benchmark IoT traffic datasets under varied attack scenarios shows that FL with DP maintains high detection accuracy, mitigates information leakage, and scales effectively. These results demonstrate the feasibility of combining FL and DP to deliver robust, privacy-preserving intrusion detection for next-generation IoT networks.
Malicious actors can introduce poisoned data by exploiting security vulnerabilities that may be present anywhere in networked systems. Depending on how the data is processed and used, this can have severe and potentially catastrophic effects. Using the data produced in such systems for the generation and evaluation of Artificial Intelligence (AI)/Machine Learning (ML) models, one may identify if malicious data is being introduced, though not necessarily where the intrusions occur. In this work we exploit the availability of metadata that is associated with the security context in which data is collected, transported and processed, as would be available, for example, in a data confidence fabric. We use this metadata in combination with iterative data weighting informed by that context. This facilitates the isolation of potential attack vectors or vulnerabilities by systematically training and evaluating low-impact AI/ML models while adjusting individual context weighting to discover the outlier features. With this approach, we can identify specific security or safety contexts of high significance based on anomalous impacts on model accuracy and loss evaluation computations.
This paper introduces a grammar-driven approach to model and detect sequences of Advanced Persistent Threat (APT) attacks. APTs are characterized by their complexity and multi-step nature, making them challenging to detect with traditional systems. The proposed method employs interpretable rules to capture malicious behaviors and aligns semantically with the MITRE ATT CK framework. This approach enables the detection of plausible attack scenarios even in the presence of incomplete or noisy data. We evaluate it using a public large CTF dataset which provides realistic and diverse attack scenarios. Experiments illustrate the effectiveness of the method in reconstructing plausible attack progressions, even with incomplete data. The main contribution of this study is an open-source implementation in Rust, ensuring reproducibility and extensibility. We also propose future enhancements to better model contextual dependencies between tactics in APT attack sequences. In a nutshell, this grammatical approach offers a robust method for detecting sophisticated threats, bridging the gap between low-level observations and high-level strategic reasoning.
Cyber resilience requirements may be implemented either to comply with regulatory obligations or to align with industry best practices. They enable organizations to demonstrate that they are capable of anticipating, withstanding, recovering from, and adapting to difficult situations and stresses. In this context, metrics can be used in a structured way to demonstrate these capabilities. These are conceptual data repositories that define and standardize information. They must be clearly defined, effectively implemented, and continuously monitored. According to [30] metrics are measures and assessment results intended to track progress, support decision-making, and enhance performance against defined targets. In this paper, we propose an approach for eliciting and selecting cyber resilience metrics that considers the enterprise architecture layers defined by TOGAF. Once selected, we propose a quantitative approach to evaluate the cyber-resilience level of a capability and a Petri net model to represent the interdependencies between cyber-resilience across the enterprise architecture layers.
Self-Sovereign Identity (SSI) platforms expose a new, decentralised trust stack—but they also introduce a novel attack surface spanning edge agents, verifiable credential registries and protocol bridges. However, the question of how to secure these architectural systems remains largely unexplored in the scientific literature, which focuses more on the functionalities they offer. And even when this is the case, current research does not always guarantee the traceability of security measures to the targeted security objectives. We propose an integrated decision framework that aligns business risk appetite with concrete defensive actions. Security attributes derived from the SABSA model anchor an attack graph instantiated with MITRE ATT CK techniques; candidate controls are drawn from the ATT CK and D3FEND corpus. A mixed-integer non-linear programming selects the minimum-cost control portfolio that keeps each attribute’s residual risk below its governance - defined threshold. The optimiser is embedded in a parametric Monte-Carlo simulation that quantifies the probability of exceeding a global loss limit under uncertain attack likelihood and control effectiveness. The model provides an auditable chain from budget spent to the security objective it protects, reconciling divergent scholarly assessments and delivering a reproducible, business-aligned strategy for securing SSI architecture.
The increasing adoption of cloud computing for 3D model sharing and storage necessitates robust protection mechanisms for confidentiality and ownership verification. While encryption ensures data confidentiality, watermarking techniques are required for traceability and ownership protection. This paper presents an enhanced version of an existing homomorphic encryption-based reversible watermarking scheme that employs histogram shifting and the Paillier cryptosystem for 3D models. The original method enables watermark operations in both encrypted and clear domains but suffers from high computational complexity. Our improvement refines homomorphic encryption operations while preserving the core algorithm’s reversible properties. Experimental results demonstrate substantial computational time reductions of up to 99.9 https://github.com/PierreMahieux/Improved_RRDH .
Technical documentation often encodes implicit indicators of device behavior and design choices that can correlate with security weaknesses. This paper introduces a specification-driven framework that automatically extracts such indicators from technical documentation to predict the presence of vulnerabilities in IoT devices. We convert textual specifications into features using TF-IDF and BM25, then evaluate XGBoost and Random Forest classifiers on a corpus of 1,521 documents spanning vulnerable IoT devices, non-vulnerable IoT devices, and non-IoT products. XGBoost achieved the best performance (accuracy 95.1
This paper presents an implementation and evaluation of the Rhapsody algorithm, which mines Attribute-Based Access Control (ABAC) policies from sparse access logs. Rhapsody introduces a novel reliability metric to mitigate over-permissiveness in rule generation. Our work extends the original algorithm by evaluating it on other datasets. We also modify the original confidence evaluation to stabilise rule count and improve alignment with Access Control List (ACL) policies. Furthermore, we introduce specificity as a novel diagnostic metric that evaluates the model’s capacity to reject unauthorised access, a critical aspect often neglected in prior approaches. The experiments are conducted on synthetic and real-world datasets to assess the algorithm’s performance and its resistance to varying levels of noise and data sparsity. The results demonstrate that fine-tuning hyperparameters, namely the support and reliability thresholds, significantly impacts rule quality and robustness against over-permissiveness. These findings further highlight the trade-off between rule simplicity, coverage, and interpretability in policy mining using Rhapsody.
Cooperative Intelligent Transport Systems (C-ITS) bring together vehicles, roadside infrastructure, and service platforms into a continuously interacting environment. The diversity and scale of these systems create persistent challenges for both security and interoperability. This paper introduces a standards-based methodology for designing C-ITS with security built in from the outset. The approach combines a structured decomposition of system assets and message flows with a goal-oriented security workflow, allowing concrete safeguards, such as authenticated communication, protected data exchange, resilient message delivery, and traceable logging, to be derived at an early stage, without depending on past incident data. The result is a solution architecture that is both traceable and interoperable, reducing the need for scarce security expertise and accommodating different communication technologies. The method is illustrated with a vehicle-to-infrastructure (V2I) case study, where roadside units broadcast roadworks warnings and movement data to vehicles. Our contribution is twofold: (i) a standards-aligned method for secure-by-design C-ITS architecture, and (ii) its application to a realistic deployment scenario, offering a practical path toward more resilient and adaptable transport systems.
Hypervisors form the trusted foundation of modern embedded and safety-critical systems, yet few of them come with formal assurance. This paper reports on our ongoing effort to bring rigorous verification to Bao, a lightweight open-source static partitioning hypervisor. We contribute (i) a formal specification and SMT-based validator to automatically detect configuration errors, and (ii) a model checking framework to verify key implementation routines, focusing on Bao’s virtual memory subsystem that enforces isolation. Our compositional, contract-driven approach mitigates scalability issues and has already uncovered subtle flaws in the codebase. These results represent a significant step toward achieving practical industrial-grade assurance for hypervisors in real-time and mixed-criticality environments.
Traditional finance industry suffers from inefficiencies that can be solved by distributed ledger technology. One of the key challenges to the adoption of distributed technology is the privacy concerns surrounding transactions, while still maintaining auditability and meeting regulatory requirements. This paper presents a suite of critical business use cases that are prevalent in the traditional finance industry that are primed for the adoption of distributed ledger technology. For each use case, we determine the respective privacy and auditability requirements. In order to meet these requirements, we present a generic encrypted table-based ledger (ETL) notion that generalizes existing encrypted table-based distributed ledgers. Furthermore, we demonstrate how a bank can be audited for various financial audits without violating privacy.
The digitalization of public and governmental services has enhanced the efficiency, transparency, and collaboration in forensic investigations. However, digital forensics faces critical challenges related to maintaining the integrity, authenticity, and trustworthiness of forensic evidence. This paper addresses how to preserve the integrity of forensic evidence throughout its lifecycle and the balance of trust among stakeholders. We propose a blockchain-based digital forensic system, ForensicChain, that securely records, updates, and verifies case-related data while adhering to legal and technological aspects. Our method leverages Merkle trees to generate cryptographic fingerprints of case files, allowing efficient tamper detection. The system ensures that authorized actions are recorded, maintaining a fully auditable record of modifications. We demonstrate the practicality of our proposed solution through a proof of concept implementation using the Cardano blockchain.
In this paper, we address the challenge of optimizing resilience in IT architectures, where increasing interconnection and complexity make traditional cybersecurity insufficient to ensure service continuity. We propose an ontology-based framework that formalizes resilience across three components robustness, adaptability, and recovery by structuring IT systems into components, features, mitigations, techniques, and tools. This ontology enables a quantifiable assessment of resilience and cost, allowing systematic identification of weaknesses and guided improvements. We introduce a multi-objective optimization model, expressed as a scalarized function balancing resilience and cost through weighting coefficients, and solved with the PuLP library using the CBC solver. Several optimization scenarios are explored: tool selection under cost constraints, resilience maximization with limited budgets, and incremental improvement in partially resilient architectures. Results demonstrate the antagonistic relation between resilience and cost, while highlighting feasible trade-offs that can guide decision-makers in adapting resilience strategies to organizational needs. The proposed approach not only formalizes resilience evaluation but also provides a decision-support mechanism for gradual and cost-effective enhancement of IT architectures. Finally, we discuss limitations and future extensions, notably the integration of uncertainty, dynamic cost models, and differentiated resilience weights.
This study delves into the core obstacles organizations encounter when trying to adopt modern DevSecOps practices. Using a constructivist grounded theory approach, we conducted eighteen in-depth, semi-structured interviews with two distinct groups: nine senior cybersecurity managers and nine hands-on software engineers. Our analysis revealed a profound disconnect between strategic vision and the daily grind. Managers often spoke of governance, resource allocation, and fostering a collaborative culture, while engineers frequently experienced security efforts as disruptive, inefficient, and detrimental to their developer experience (DevEx). Through a comparative analysis of these two perspectives, we pinpointed misaligned priorities, broken communication, and a lack of jointly designed solutions that truly bridge social and technical workflows as key contributors to this divide. From these emergent insights, a core category of Socio-Technical Friction emerged, providing a new theoretical lens that strongly aligns with and extends the principles of Socio-Technical Systems (STS) theory within the DevSecOps context. Specifically, our findings show that DevSecOps initiatives often falter precisely because they treat social and technical systems as separate entities rather than interconnected parts of a whole. This fundamental misalignment creates significant friction where these two systems meet, ultimately slowing down development and weakening security. This study concludes by offering practical recommendations for closing this gap, advocating for a holistic approach to DevSecOps as a truly unified socio-technical system.
Boneh and Franklin introduced one of the earliest constructions of the elegant concept of identity-based encryption (IBE) about two decades ago. Despite significant research advancements and numerous potential applications, IBE has yet to see widespread real-world adoption. A primary challenge is the excessive trust placed in the key derivation server, which inherently possesses the ability to decrypt all ciphertexts. Recent work proposed approaches to reduce server trust in IBE schemes by using a server, called a key curator, that only helps update the public parameters and holds no secret key. In this paper, we present, in the key-curator model, the first IBE scheme that, via a black-box reduction, preserves sender efficiency of a class of IBE schemes (for which we show that there are already well-known and efficient instantiations in the literature), works in the public-random string model (and in particular not requiring extra secret information kept by the key curator) and satisfies ‘sender-efficiency’ performance requirements demanded by many applications (e.g., Internet of Things). All previously proposed IBE schemes with reduced server trust either did not preserve IBE functionality or were subject to server-collusion attacks or only focused on ‘receiver-efficiency’ performance requirements.
As Artificial Intelligence systems become more integrated into everyday applications, concerns about data privacy and compliance with the “Right to Be Forgotten” laws have grown. Machine Learning models are increasingly vulnerable to privacy attacks such as membership inference attacks and model inversion attacks, which can reveal sensitive training data. Traditional approaches often require retraining the model from scratch, a costly and time-consuming process. This has led to an increased focus on Machine Unlearning, a process that selectively removes the influences of specific data points from an already-trained model without retraining. However, a reliable and explainable verification method to ensure that unlearning occurred remains to be explored. This research introduces a novel verification method leveraging local explainability to ensure the effectiveness and transparency of unlearning operations. By analyzing feature importance before and after unlearning, the framework provides interpretable evidence of behavioral change. Experiments on the Breast Cancer dataset show that Data Obfuscation and Data Pruning achieve up to 89
Enterprises and public administrations rely on complex, distributed information systems (IS) that integrate heterogeneous technologies and infrastructures. Managing these systems requires accurate cartography and robust modelling to ensure alignment with business objectives, regulatory compliance, and resilience to cybersecurity threats. Cartography -dynamically eliciting app, tools, components- serves as a decision-support tool that builds stakeholder trust and acceptance through transparency and explainability, enabling stakeholders to visualize processes, data flows, and system dependencies. As such, cartography is becoming a cornerstone for cybersecurity, regulatory compliance, and enterprise governance. This paper presents CARTOGRAPHIT, a framework bridging academic research and industrial deployment through the CyberCampus ANR INRIA PTCC program( https://ptcc.fr/ ). Our multilayer data model separates business, application, data, and infrastructure concerns, offering clarity and adaptability. We implement 6 layers, at various levels of granularity (ecosystem, business, application, container, logical, physical) enabling an intelligent auto-discovery engine. CARTOGRAPHIT combines contributions in trust, traceability, and (meta)data modelling with compliance requirements (ANSSI, GDPR, ISO 27001, NIS2).
Secure Neural Network Inference (SNNI) protocols, vital for privacy-preserving AI, face substantial computational and communication overhead. Dynamic Early-Exit (EE) networks could help decrease the overhead, but existing SNNI protocols do not support such networks. We introduce QUOKKA, the first system to enable SNNI for confidence-based EE neural networks using secure Multi-Party Computation. QUOKKA addresses the challenges of dynamic decision-making and sensitive intermediary result handling in SNNI. Implemented with EENet and CrypTen, QUOKKA achieves 2–5 × acceleration over traditional SNNI without a decrease in accuracy. Our findings demonstrate practical, highly efficient, and privacy-preserving SNNI for dynamic AI, paving the way for broader Machine-Learning-as-a-Service deployment.
In a model inversion attack, an adversary tries to reconstruct private training data through iterative inference of a neural network model. To ensure confidentiality of the training data, protection against model inversion attacks is crucial. However, existing defense techniques primarily require modifications to the trained model architecture or even retraining, which limits their applicability to deployed models. In addition, most of them become ineffective against label-only attacks, which require minimal information to succeed. This paper proposes an improved defense mechanism that filters out inference requests from malicious attackers. It does not alter existing model architectures and works against various types of attacks. Our experimental results show that our approach is highly effective with mean defense accuracy scores of 90.00
