This paper presents a study of update-related vulnerabilities based on a curated dataset of disclosures from the past decade. We analyze the exploitability, impact, and severity of these vulnerabilities, comparing them with the broader population of disclosed vulnerabilities. Our findings reveal that update-related vulnerabilities tend to be more severe and impactful, with a higher concentration of high-severity scores and a greater compromise of confidentiality, integrity, and availability. In contrast to general vulnerabilities, which are often network-exploitable, most update-related attacks require local access. We identify and categorize the most common weakness types in update mechanisms. We find that the most frequent weaknesses include authentication and authorization-related weaknesses, input-related weaknesses, path-related weaknesses, and certificate-related weaknesses. Furthermore, we introduce a rule-based approach with predefined keywords that assign vulnerabilities to six target-system classes. The classification relies on textual vulnerability descriptions together with vendor and product metadata. Finally, based on our analysis, we derive a set of clear mitigation recommendations to help secure update processes and reduce associated risks.

In this study, we introduce MoMEP, a message transmission protocol relying on chameleon signatures. These signatures allow modification of signed messages while keeping the original signature valid. Despite their useful features, chameleon signatures have received limited use in real-world applications, such as internet protocols. Our work bridges this the gap by presenting a protocol based on chameleon signatures, and formally proving its trustworthiness using symbolic formal verification. In particular, providing accountability guarantees presents unique challenges, as message modifications can erase evidence of misbehavior, breaking traditional assumptions about trace-based accountability. To address this, we define three protocol-level accountability properties (i.e., unforgeability, non-repudiation, and non-frameability) for MoMEP, complementing earlier definitions applicable for cryptographic primitives. These properties are essential to allow symbolic protocol verification and ensure accountability for all relevant entities involved in the message exchange. We also introduce an entity accountability notion that does not rely on storing protocol traces and is based on an evidence-driven verdict function. We model MoMEP in the Tamarin theorem prover and formally verify that it satisfies our accountability properties. Finally, we prove the soundness and completeness of MoMEP’s evidence-based verdict function, reinforcing its correctness and applicability for deciding accountability in real-world scenarios.

We present a PQ Noise Explorer, a Rust repository for designing, formally verifying, and implementing arbitrary PQ Noise patterns. PQ Noise Explorer can validate any PQ Noise pattern and translate it into a model for automated verification and also a software implementation written in Rust.

Digital infrastructure is vital for the economy, democracy, and everyday life, yet it is becoming increasingly vulnerable to strategic cyber-attacks. These attacks can lead to significant disruptions, resulting in widespread service outages, financial losses, and a decline in public trust. Ensuring resilience is difficult due to the infrastructure's complexity, the large volume of data involved, and the growing need for quick, coordinated responses. In the EU Horizon project CyberSecDome, we propose a multi-layered framework that provides AI-driven solutions for incident prediction and detection, automated testing, risk assessment, and rapid incident response, supporting continuity amid complex, large-scale cyber threats. Additionally, Cyber-SecDome introduces a virtual reality interface to enhance AI model explainability and provide real-time contextual awareness of ongoing attacks and defense mechanisms. It also enables privacy-aware model sharing across AI systems, fostering secure collaboration among different domes.

With the recent dramatic increase in performance of artificial intelligence and related computing systems, together with advanced sensing, connectivity, and technological platforms, autonomous systems are poised to enter many application domains such as transportation and manufacturing. As autonomy increases, the risks of cybersecurity threats are equally rising, requiring the development of sophisticated methods on all layers of autonomous systems architectures. Therefore, this paper systematically introduces cybersecurity challenges ranging from the physical layer to the system of systems layer defining the collaboration of autonomous systems. Without loss of generality, autonomous vehicles are used to highlight current developments, illustrating which efforts are necessary to achieve secure and safe autonomous systems. Our discussions are comprehensively highlighting which research domains require further investigation and offer promising opportunities to contribute to mitigating cybersecurity challenges of autonomous systems.

Recent changes in standards and regulations, driven by the increasing importance of software systems in meeting societal needs, mandate increased security testing of software systems. Penetration testing has been shown to be a reliable method to asses software system security. However, manual penetration testing is labor-intensive and requires highly skilled practitioners. Given the shortage of cybersecurity experts and current societal needs, increasing the degree of automation involved in penetration testing can aid in fulfilling the demands for increased security testing. In this work, we formally express the penetration testing problem at the architectural level and suggest a general self-organizing architecture that can be instantiated to automate penetration testing of real systems. We further describe and implement a specialization of the architecture in ADAPT, an architecture-driven automated penetration testing tool, targeting systems composed of hosts and services. We evaluate and demonstrate the feasibility of ADAPT by automatically performing penetration tests with success against: Metasploitable2, Metasploitable3, and a realistic virtual network used as a lab environment for penetration tester training.

Remote Attestation is emerging as a promising technique to ensure that some remote device is in a trustworthy state. This can for example be an IoT device that is attested by a cloud service before allowing the device to connect. However, flaws in the communication protocols associated with the remote attestation mechanism can introduce vulnerabilities into the system design and potentially nullify the added security. Formal verification of protocol security can help to prevent such flaws. In this work we provide a detailed analysis of the necessary security properties for remote attestation focusing on the authenticity of the involved agents. We extend beyond existing work by considering the possibility of an attestation server (making the attestation process involve three parties) as well as requiring verifier authentication. We demonstrate that some security properties are not met by a state-of-the-art commercial protocol for remote attestation for our strong adversary model. Moreover, we design two new communication protocols for remote attestation that we formally prove fulfil all of the considered authentication properties.

Providing authenticated interactions is a key responsibility of most cryptographic protocols. When designing new protocols with strict security requirements it is therefore essential to formally verify that they fulfil appropriate authentication properties. We identify a gap in the case of protocols with unilateral (one-way) authentication, where existing properties are poorly adapted. In existing work, there is a preference for defining strong authentication properties, which is good in many cases but not universally applicable. In this work we make the case for weaker authentication properties. In particular, we investigate one-way authentication and extend Lowe's authentication hierarchy with two such properties. We formally prove the relationship between the added and existing properties. Moreover, we demonstrate the usefulness of the added properties in a case study on remote attestation protocols. This work complements earlier work with additional generic properties that support formal verification of a wider set of protocol types.

Mobile networks have grown in size and relevance, with novel applications in areas including transportation, finance, and health. The wide use of mobile networks generates rich data about users, raising interest in using such data for law enforcement and antiterrorism through Lawful Interception (LI). Countries worldwide have established legal frameworks to conduct LI, and technical standards have been created for its implementation and deployment, but without sufficient (and rigorous) security controls. While LI originated for benign purposes, we show in this paper that malicious entities could exploit it to frame users into suspicion of criminal activity. Further, we propose a solution for non-frameability, which we formally prove uphold desired properties even in scenarios where attackers completely infiltrate the operator networks. To perform the formal verification, we extend prior work with a more complete model of the fifth generation (5G) of mobile networks in the Tamarin prover.

Vehicular networks will enable a range of novel applications to enhance road traffic efficiency, safety, and reduce fuel consumption. As for other cyber-physical systems, security is essential to the deployment of these applications and standardisation efforts are ongoing. In this paper, we perform a systematic security evaluation of a vehicular platooning protocol through a thorough analysis of the protocol and security standards. We tackle the complexity of the resulting model with a proof strategy based on a relation on keys. The key relation forms a partial order, which encapsulates both secrecy and authenticity dependencies. We show that our order-aware approach makes the verification feasible and proves authenticity properties along with secrecy of all keys used throughout the protocol.

Microservice architectures decompose applications into individual components for enhanced maintainability and horizontal scaling, but also comes with an increased cost for orchestrating the services. Software-Defined Networks (SDNs) enables the dynamic configuration of network switches using controllers. In this paper we propose a microservice architecture that leverages SDN to orchestrate the microservices with the goal of reducing the orchestration latency cost. We perform a set of experiments using Mininet in which we implement a tailor-made microservice application that uses SDN for orchestration in combination with a set of different controllers and load balancers. Our results show that our proposed architecture performs in the same order of magnitude as a corresponding monolithic system.

The expansion of mobile network capabilities throughout the decades has increased people's exposure to the digital world, and the next generations of communication networks are expected to achieve ubiquitous connectivity and immersive use cases. Security and privacy concerns have arisen and are continuously taken into account in the design of mobile networks. However, a relevant limitation currently lies in the use of shared secrets for providing security and privacy to users. Ideally, we believe that users' identities should be immune to impersonation as long as their own devices remain secure, notwithstanding the network operators and other entities potentially being compromised. In this paper, we develop this idea with the objective of providing the non-repudiation property, which represents a mitigation to its dual, impersonation.

Today’s vehicles are examples of Cyber-Physical Systems (CPS) controlled by a large number of electronic control units (ECUs), which manage everything from heating to steering and braking. Due to the increasing complexity and inter-dependency of these units, it has become essential for an ECU to be able to ensure the integrity of the firmware running on other ECU’s to guarantee its own correct operation. Existing solutions for firmware attestation use a centralized approach, which means a single point of failure. In this article, we propose and investigate a decentralized firmware attestation scheme for the automotive domain. The basic idea of this scheme is that each ECU can attest to the state of those ECU’s on which it depends. Two flavors of ECU attestation, i.e., parallel and serial solution, were designed, implemented, and evaluated. The two variants were compared in terms of both detection performance (i.e., the ability to identify unauthorized firmware modifications) and timing performance. Our results show that the proposed scheme is feasible to implement and that the parallel solution showed a significant improvement in timing performance over the serial solution.

Summary Blockchains are increasingly studied in the context of new applications. Permissioned blockchains promise to deal with the issue of complete removal of trust, a notion that is currently the hallmark of the developed society. Before the idea is adopted in contexts where resource efficiency and fast operation is a requirement, one could legitimately ask the question: can permissioned blockchains match the performance of traditional large‐scale databases? This paper compares two popular frameworks, Hyperledger Fabric and Apache Cassandra, as representatives of permissioned blockchains and distributed databases, respectively. We compare their latency for varying workloads and network sizes. The results show that, for small systems, blockchains can start to compete with traditional databases, but also that the difference in consistency models and differences in setup can have a large impact on the resulting performance.

Coordinated vehicles for intelligent traffic management are instances of cyber-physical systems with strict correctness requirements. A key building block for these systems is the ability to establish a group membership view that accurately captures the locations of all vehicles in a particular area of interest. In this article, we formally define view correctness in terms of soundness and completeness and establish theoretical bounds for the ability to verify view correctness. Moreover, we present an architecture for an online view detection and verification process that uses the information available locally to a vehicle. This architecture uses an SMT solver to automatically prove view correctness (if possible). We evaluate this architecture using both synthetic and trace-based scenarios and demonstrate that the ability to verify view correctness is on par with the ability to detect view violations.

This paper investigates common misconceptions held by students regarding concurrency in order to better understand how concurrency education can be improved in the future. As a part of the exam in two courses on concurrency and operating systems, students were asked to identify and eliminate any concurrency issues in a piece of code as a part of their final exam. Different types of mistakes were identified and the 216 answers were sorted into categories accordingly. The results presented in this paper show that while most students were able to identify the cause of an issue given its symptoms, only approximately half manage to successfully eliminate the concurrency issues. Many of the incorrect solutions fail to associate shared data with a synchronization primitive, e.g. using one lock to protect multiple instances of a data structure, or multiple locks to protect the same instance in different situations. This suggests that students may not only have trouble dealing with concepts related to concurrency, but also more fundamental concepts related to the underlying computational model. Finally, this paper proposes possible explanations for the students' mistakes in terms of improper mental models, and suggests types of problems that highlight the issues with these mental models to improve students' understanding of the subject.

The Internet-of-Things (IoT) is a large and complex domain. These systems are often constructed using a very diverse set of hardware, software and protocols. This, combined with the ever increasing number of IoT solutions/services that are rushed to market means that most such systems are rife with security holes. Recent incidents (e.g., the Mirai botnet) further highlight such security issues. With emerging technologies such as blockchain and software-defined networks (SDNs), new security solutions are possible in the IoT domain. In this paper we will explore future trends in IoT security: (a) the use of blockchains in IoT security, (b) data provenance for sensor information, (c) reliable and secure transport mechanisms using SDNs (d) scalable authentication and remote attestation mechanisms for IoT devices and (e) threat modeling and risk/maturity assessment frameworks for the domain.

In Vehicular Ad Hoc Networks (VANETs), nodes periodically share beacons in order to convey information about identity, velocity, acceleration, and position. Truthful positioning of nodes is essential for the proper behavior of applications, including the formation of vehicular platoons. Incorrect position information can cause problems such as increased fuel consumption, reduced passenger comfort, and in some cases even accidents. In this paper, we design and evaluate Vouch: a secure proof-of-location scheme tailored for VANETs. The scheme leverages the node positioning capability of fifth generation (5G) wireless network roadside units. The key idea of Vouch is to disseminate periodic proofs of location, combined with plausibility checking of movement between proofs. We show that Vouch can detect position falsification attacks in high-speed scenarios without incurring a large overhead.

New advanced traffic management solutions with fully or semi-autonomous vehicles that communicate over a wireless interface to coordinate their driving decisions create new challenges in distributed computing. In this paper we address the problem of dynamic group membership in three stages. First, we propose three criteria to specify correctness and performance of the group views created by such algorithms in terms of soundness, completeness and freshness. Second, we develop a group membership protocol tailored for vehicular coordination. Finally, we show through simulation and model-based verification that the protocol does indeed meet the criteria and provide at least 95% perfect group membership views under as adverse conditions as 70% packet loss or very high churn rate.

This work studies the energy and quality of service (QoS) trade-off in the context of mobile devices with two communication interfaces (a high energy and a low energy interface). We propose an optimisation scheme during underload scenarios where proxy groups are dynamically formed exploiting both interfaces. The scheme integrates a reward mechanism that compensates a proxy while carrying other group members’ traffic, and deals with churn (joining and leaving of nodes) in a cell area. For traffic flows that approximate knowledge about current services we show that the scheme can achieve energy savings of 60% for all mobile nodes as whole. We also demonstrate the impact on disruption-sensitive flows as a function of the traffic mix, and that the use of rewards for selection of proxies is a fair mechanism in the long term.

For most safety-related applications that are envisaged in VANETs, the provisioning of a real-time medium access control is of great importance. However, the ability to access the wireless medium in a collision-free and time-bounded manner is particularly challenging in networks with unreliable wireless channel and dynamic topologies. Existing CSMA protocols such as 802.11p are prone to high rates of transmission collision, whereas TDMA-based protocols are not able to cope with the highly dynamic nature of vehicular networks. In this paper, we propose a novel MAC protocol: Real-time Reservation Protocol (RRP) which supports reliable and timely broadcast in VANETs. We believe that the vision of context awareness and farsightedness which constitute the core of most safety applications in VANETs should be brought to the design of the MAC layer as well. In the proposed protocol, broadcast messages are transmitted with high success rates, and the maximum time to access the medium is bounded. In a simulation-based study we compare the performance of RRP with 802.11p and RR-ALOHA in terms of packet delivery rate and staleness - a novel application-level QoS metric. Results indicate that RRP achieved satisfactory performance, which demonstrates the feasibility and effectiveness of real-time medium access control in VANETs.

In the event of a disaster, telecommunication infrastructures can be severely damaged or overloaded. Hastily formed networks can provide communication services in an ad hoc manner. These networks are challenging due to the chaotic context where intermittent connection is the norm and the identity and number of participants cannot be assumed. In such environments malicious actors may try to disrupt the communications to create more chaos for their own benefit. This paper proposes a general security framework for monitoring and reacting to disruptive attacks. It includes a collection of functions to detect anomalies, diagnose them, and perform mitigation. The measures are deployed in each node in a fully distributed fashion, but their collective impact is a significant resilience to attacks, so that the actors can disseminate information under adverse conditions. The approach has been evaluated in the context of a simulated disaster area network with a manycast dissemination protocol, Random Walk Gossip, with a store-and-forward mechanism. A challenging threat model where adversaries may attempt to reduce message dissemination or drain network resources without spending much of their own energy has been adopted.

Information dissemination in disaster scenarios requires timely and energy-efficient communication in intermittently connected networks. When the existing infrastructure is damaged or overloaded, we suggest the use of a manycast algorithm that runs over a wireless mobile ad hoc network, and overcomes partitions using a store-and-forward mechanism. This paper presents a random walk gossip protocol that uses an efficient data structure to keep track of already informed nodes with minimal signaling. Avoiding unnecessary transmissions also makes it less prone to overloads. Experimental evaluation shows higher delivery ratio, lower latency, and lower overhead compared to a recently published algorithm.

Abstract Replicated distributed object systems are deployed to provide timely and reliable services to actors at distributed locations. This paper treats applications in which data updates are dependent on satisfaction of integrity constraints over multiple objects. Network partitions, caused by occasional link failures, overload or attacks create problems in keeping both consistency and availability in such networks. We propose a means of achieving higher availability by providing partition‐awareness in middleware. The general approach has been illustrated by implementing a number of CORBA extensions that trade consistency for availability during network partitions. This paper contains a thorough experimental evaluation that presents the gains and costs of our approach. The experiments clearly illustrate the benefit of our protocols in terms of significantly higher availability and the number of performed operations. Copyright © 2009 John Wiley & Sons, Ltd.

Replicated systems that run over partitionable environments, can exhibit increased availability if isolated partitions are allowed to optimistically continue their execution independently. This availability gain is traded against consistency, since several replicas of the same objects could be updated separately. Once partitioning terminates, divergences in the replicated state needs to be reconciled. One way to reconcile the state consists of letting the application manually solve inconsistencies. However, there are several situations where automatic reconciliation of the replicated state is meaningful. We have implemented replication and automatic reconciliation protocols that can be used as building blocks in a partition-tolerant middleware. The novelty of the protocols is the continuous service of the application even during the reconciliation process. A prototype system is experimentally evaluated to illustrate the increased availability despite network partitions.