Biblio

Middleware for IoT (Internet of Things) helps application developers face challenges, such as device heterogeneity, service interoperability, security and scalability. While extensively adopted nowadays, IoT middleware systems are static because, after deployment, updates are only possible by stopping the thing. Therefore, adaptive capabilities can improve existing solutions by allowing their dynamic adaptation to changes in the environmental conditions, evolve provided functionalities, or fix bugs. This paper presents AMoT, an adaptive publish/subscribe middleware for IoT whose design and implementation adopt software architecture principles and evolutive adaptation mechanisms. The experimental evaluation of AMoT helps to measure the impact of the proposed adaptation mechanisms while also comparing the performance of AMoT with a widely adopted MQTT (Message Queuing Telemetry Transport) based middleware. In the end, adaptation has an acceptable performance cost and the advantage of tunning the middleware functionality at runtime.

This paper describes the architecture and the fundamental methodology of an anomaly detector, which by continuously monitoring Simple Network Management Protocol data and by processing it as complex-events, is able to timely recognize patterns of faults and relevant cyber-attacks. This solution has been applied in the context of smart grids, and in particular as part of a security and resilience component of the Information and Communication Technologies (ICT) Gateway, a middleware-based architecture that correlates and fuses measurement data from different sources (e.g., Inverters, Smart Meters) to provide control coordination and to enable grid observability applications. The detector has been evaluated through experiments, where we selected some representative anomalies that can occur on the ICT side of the energy distribution infrastructure: non-malicious faults (indicated by patterns in the system resources usage), as well as effects of typical cyber-attacks directed to the smart grid infrastructure. The results show that the detection is promisingly fast and efficient.

Modern Intelligent Transport Systems (ITSs) are comprehensive applications that have to cope with a multitude of challenges while meeting strict service and security standards. A novel data-centric middleware that provides the foundation of such systems is presented in this paper. This middleware is designed for high scalability, fast data processing and multimodality. To achieve these goals, an innovative spatial annotation (SpatiaIJSON) is utilised. SpatialJSON allows the representation of geometry, topology and traffic information in one dataset. Data processing is designed in such a manner that any schema or ontology can be used to express information. Further, common concerns of ITSs are addressed, such as authenticity of messages. The core task, however, is to ensure a quick exchange of evaluated information between the individual traffic participants.

In mobile edge computing, edge devices collect data, and an edge server performs computational or data processing tasks that need real-time processing. Depending upon the requested task's complexity, an edge server executes it locally or remotely in the cloud. When an edge server needs to offload its computational tasks, there could be a sudden failure in the cloud or network. In this scenario, we need to provide a flexible execution model to edge devices and servers for the continuous execution of the task. To that end, in this paper, we induced a middleware system that allows an edge server to execute a task on the edge devices instead of offloading it to a cloud server. Edge devices not only send data to an edge server for further processing but also execute edge services by utilizing nearby edge devices' computing resources. We extend the concept of service-oriented architecture and integrate a decentralized peer-to-peer network architecture to achieve reusability, location-specific security, and reliability. By following our methodology, software developers can enhance their application in a collaborative environment without worrying about low-level implementation.

Campus Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation. In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols.We show, in general, how the soundness and completeness of a rule-based model can be ensured by verifying trace properties, linking soundness to safety properties and completeness to liveness properties. We then demonstrate the approach for a recently proposed threat model that quantifies the confidentiality of email communication on the Internet, including DNS, DNSSEC, and SMTP. Using off-the-shelf protocol verification tools, we discover two flaws in their threat model. After fixing them, we show that it provides symbolic soundness.

The advent of 5G, one of the most recent and promising technologies currently under deployment, fulfills the emerging needs of mobile subscribers by introducing several new technological advancements. However, this may lead to numerous attacks in the emerging 5G networks. Thus, to guarantee the secure transmission of user data, 5G Authentication protocols such as Extensible Authentication Protocol - Authenticated Key Agreement Protocol (EAP-AKA) were developed. These protocols play an important role in ensuring security to the users as well as their data. However, there exists no guarantees about the security of the protocols. Thus formal verification is necessary to ensure that the authentication protocols are devoid of vulnerabilities or security loopholes. Towards this goal, we formally verify the security of the 5G EAP-AKA protocol using an automated verification tool called ProVerif. ProVerif identifies traces of attacks and checks for security loopholes that can be accessed by the attackers. In addition, we model the complete architecture of the 5G EAP-AKA protocol using the language called typed pi-calculus and analyze the protocol architecture through symbolic model checking. Our analysis shows that some cryptographic parameters in the architecture can be accessed by the attackers which cause the corresponding security properties to be violated.

Today's Internet is built on decades-old networking protocols that lack scalability, reliability, and security. In response, the networking community has developed path-aware Internet architectures that solve these issues while simultaneously empowering end hosts. In these architectures, autonomous systems construct authenticated forwarding paths based on their routing policies. Each end host then selects one of these authorized paths and includes it in the packet header, thus allowing routers to efficiently determine how to forward the packet. A central security property of these architectures is path authorization, requiring that packets can only travel along authorized paths. This property protects the routing policies of autonomous systems from malicious senders.The fundamental role of packet forwarding in the Internet and the complexity of the authentication mechanisms employed call for a formal analysis. In this vein, we develop in Isabelle/HOL a parameterized verification framework for path-aware data plane protocols. We first formulate an abstract model without an attacker for which we prove path authorization. We then refine this model by introducing an attacker and by protecting authorized paths using (generic) cryptographic validation fields. This model is parameterized by the protocol's authentication mechanism and assumes five simple verification conditions that are sufficient to prove the refinement of the abstract model. We validate our framework by instantiating it with several concrete protocols from the literature and proving that they each satisfy the verification conditions and hence path authorization. No invariants must be proven for the instantiation. Our framework thus supports low-effort security proofs for data plane protocols. The results hold for arbitrary network topologies and sets of authorized paths, a guarantee that state-of-the-art automated security protocol verifiers cannot currently provide.

Controller area network is the serial communication protocol, which broadcasts the message on the CAN bus. The transmitted message is read by all the nodes which shares the CAN bus. The message can be eavesdropped and can be re-used by some other node by changing the information or send it by duplicate times. The message reused after some delay is replay attack. In this paper, the CAN network with three CAN nodes is implemented using the universal verification components and the replay attack is demonstrated by creating the faulty node. Two types of replay attack are implemented in this paper, one is to replay the entire message and the other one is to replay only the part of the frame. The faulty node uses the first replay attack method where it behaves like the other node in the network by duplicating the identifier. CAN frame except the identifier is reused in the second method which is hard to detect the attack as the faulty node uses its own identifier and duplicates only the data in the CAN frame.

Mobile payment protocols have attracted widespread attention over the past decade, due to advancements in digital technology. The use of these protocols in online industries can dramatically improve the quality of online services. However, the central issue of concern when utilizing these types of systems is their accountability, which ensures trust between the parties involved in payment transactions. It is, therefore, vital for researchers to investigate how to handle the accountability of mobile payment protocols. In this research, we introduce a secure mobile payment protocol to overcome this problem. Our payment protocol combines all the necessary security features, such as confidentiality, integrity, authentication, and authorization that are required to build trust among parties. In other words, is the properties of mutual authentication and non-repudiation are ensured, thus providing accountability. Our approach can resolve any conflicts that may arise in payment transactions between parties. To prove that the proposed protocol is correct and complete, we use the Scyther and AVISPA tools to verify our approach formally.

UPI (Unified Payments Interface) is a framework in India wherein customers can send payments to merchants from their smartphones. The framework consists of UPI servers that are connected to the banks at the sender and receiver ends. To send and receive payments, customers and merchants would have to first register themselves with UPI servers by executing a registration protocol using payment apps such as BHIM, PayTm, Google Pay, and PhonePe. Weaknesses were recently reported on these protocols that allow attackers to make money transfers on behalf of innocent customers and even empty their bank accounts. But the reported weaknesses were found after informal and manual analysis. However, as history has shown, formal analysis of cryptographic protocols often reveals flaws that could not be discovered with manual inspection. In this paper, we model UPI protocols in the pattern of traditional cryptographic protocols such that they can be rigorously studied and analyzed using formal methods. The modeling simplifies many of the complexities in the protocols, making it suitable to analyze and verify UPI protocols with popular analysis and verification tools such as the Constraint Solver, ProVerif and Tamarin. Our modeling could also be used as a general framework to analyze and verify many other financial payment protocols than just UPI protocols, giving it a broader applicability.

In the era of big data and artificial intelligence, computer networks have become an important infrastructure, and the Internet has become ubiquitous. The most basic property of computer networks is reachability. The needs of the modern Internet mainly include cost, performance, reliability, and security. However, even for experienced network engineers, it is very difficult to manually conFigure the network to meet the needs of the modern large-scale Internet. The engineers often make mistakes, which can cause network paralysis, resulting in incalculable losses. Due to the development of automatic reasoning technology, automatic verification of network configuration is used to avoid mistakes. Network verification is at least an NP-C problem, so it is necessary to compress the network to reduce the network scale, thereby reducing the network verification time. This paper proposes a new model of network modeling, which is more suitable for the verification of network configuration on common protocols (such as RIP, BGP). On the basis of the existing compression method, two compression rules are added to compress the modeled network, reducing network verification time and conducting network reachability verification experiments on common networks. The experimental results are slightly better than the current compression methods.

This paper deals with a problem that arises in vertical composition of protocols, i.e., when a channel protocol is used to encrypt and transport arbitrary data from an application protocol that uses the channel. Our work proves that we can verify that the channel protocol ensures its security goals independent of a particular application. More in detail, we build a general paradigm to express vertical composition of an application protocol and a channel protocol, and we give a transformation of the channel protocol where the application payload messages are replaced by abstract constants in a particular way that is feasible for standard automated verification tools. We prove that this transformation is sound for a large class of channel and application protocols. The requirements that channel and application have to satisfy for the vertical composition are all of an easy-to-check syntactic nature.

Given the central importance of designing secure protocols, providing solid mathematical foundations and computer-assisted methods to attest for their correctness is becoming crucial. Here, we elaborate on the formal approach introduced by Bana and Comon in [10], [11], which was originally designed to analyze protocols for a fixed number of sessions, and lacks support for proof mechanization.In this paper, we present a framework and an interactive prover allowing to mechanize proofs of security protocols for an arbitrary number of sessions in the computational model. More specifically, we develop a meta-logic as well as a proof system for deriving security properties. Proofs in our system only deal with high-level, symbolic representations of protocol executions, similar to proofs in the symbolic model, but providing security guarantees at the computational level. We have implemented our approach within a new interactive prover, the Squirrel prover, taking as input protocols specified in the applied pi-calculus, and we have performed a number of case studies covering a variety of primitives (hashes, encryption, signatures, Diffie-Hellman exponentiation) and security properties (authentication, strong secrecy, unlinkability).

In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step towards achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results such as soundness of a typed model

The popular federated edge learning (FEEL) framework allows privacy-preserving collaborative model training via frequent learning-updates exchange between edge devices and server. Due to the constrained bandwidth, only a subset of devices can upload their updates at each communication round. This has led to an active research area in FEEL studying the optimal device scheduling policy for minimizing communication time. However, owing to the difficulty in quantifying the exact communication time, prior work in this area can only tackle the problem partially by considering either the communication rounds or per-round latency, while the total communication time is determined by both metrics. To close this gap, we make the first attempt in this paper to formulate and solve the communication time minimization problem. We first derive a tight bound to approximate the communication time through cross-disciplinary effort involving both learning theory for convergence analysis and communication theory for per-round latency analysis. Building on the analytical result, an optimized probabilistic scheduling policy is derived in closed-form by solving the approximate communication time minimization problem. It is found that the optimized policy gradually turns its priority from suppressing the remaining communication rounds to reducing per-round latency as the training process evolves. The effectiveness of the proposed scheme is demonstrated via a use case on collaborative 3D objective detection in autonomous driving.

Since the personal data protection law is on the way of many countries, how to use data mining method to secure sensitive information has become a challenge for enterprises. To make sure every employee follows company's data protection strategy, it may take lots of time and cost to seek and scan thousands of folders and files in user equipment, ensuring that the file contents meet IT security policies. Hence, this paper proposed a lightweight, pattern-based detection system, PIDS, which is expecting to enable an affordable data leakage prevention with essential cost and high efficiency in small business enterprise. For verification and evaluation, PIDS has been deployed on more than 100,000 PCs of collaboration enterprises, and the feedback shows that the system is able to approach its original design functionality for finding violated or sensitive contents efficiently.

We present a novel approach for the collaborative training of neural network models in decentralized federated environments. In the iterative process a group of autonomous peers run multiple training rounds to train a common model. Thereby, participants perform all model training steps locally, such as stochastic gradient descent optimization, using their private, e.g. mission-critical, training datasets. Based on locally updated models, participants can jointly determine a common model by averaging all associated model weights without sharing the actual weight values. For this purpose we introduce a simple n-out-of-n secret sharing schema and an algorithm to calculate average values in a peer-to-peer manner. Our experimental results with deep neural networks on well-known sample datasets prove the generic applicability of the approach, with regard to model quality parameters. Since there is no need to involve a central service provider in model training, the approach can help establish trustworthy collaboration platforms for businesses with high security and data protection requirements.

In the recent years, mobile ad hoc wireless networks (MANETs) have experienced a tremendous rise in popularity and usage due to their flexibility and ability to provide connectivity from anywhere at any time. In general, MANETs provide mobile communication to participating nodes in situation where nodes do not need access to an existing network infrastructure. MANETs have a network topology that changes over time due to lack of infrastructure and mobility of nodes. Detection of a malicious node in MANETs is hard to achieve due to the dynamic nature of the relationships between moving node and the nature of the wireless channel. Most traditional Intrusion Detection System (IDS) are designed to operate in a centralized manner; and do not operate properly in MANET because data in MANETs is distributed in different network devices. In this paper, we present an Hierarchical Cooperative Intrusion Detection Method (HCIDM) to secure packets routing in MANETs. HCIDM is a distributed intrusion detection mechanism that uses collaboration between nodes to detect active attacks against the routing table of a mobile ad hoc network. HCIDM reduces the effectiveness of the attack by informing other nodes about the existence of a malicious node to keep the performance of the network within an acceptable level. The novelty of the mechanism lies in the way the responsibility to protect the networks is distributed among nodes, the trust level is computed and the information about the presence of a malicious is communicated to potential victim. HCIDM is coded using the Network Simulator (NS-2) in an ad hoc on demand distance vector enable MANET during a black hole attack. It is found that the HCIDM works efficiently in comparison with an existing Collaborative Clustering Intrusion Detection Mechanism (CCIDM), in terms of delivery ratio, delay and throughput.

Trust is vital to promoting human and robot collaboration, but like human teammates, robots make mistakes that undermine trust. As a result, a human’s perception of his or her robot teammate’s trustworthiness can dramatically decrease [1], [2], [3], [4]. Trustworthiness consists of three distinct dimensions: ability (i.e. competency), benevolence (i.e. concern for the trustor) and integrity (i.e. honesty) [5], [6]. Taken together, decreases in trustworthiness decreases trust in the robot [7]. To address this, we conducted a 2 (high vs. low anthropomorphism) x 4 (trust repair strategies) between-subjects experiment. Preliminary results of the first 164 participants (between 19 and 24 per cell) highlight which repair strategies are effective relative to ability, integrity and benevolence and the robot’s anthropomorphism. Overall, this paper contributes to the HRI trust repair literature.

This paper presents a management system for a fleet of autonomous mobile robots performing logistics in security-heterogeneous factories. Loading and unloading goods and parts between workstations in these dynamic environments often demands from the mobile robots to share space and resources such as corridors, interlocked security doors and elevators among themselves. This model explores a dynamic task scheduling and assignment to the robots taking into account their location, tasks previously assigned and battery levels, all the while being aware of the physical constraints of the installation. The benefits of the proposed architecture were validated through a set of experiments in a mockup of INCM's shop-floor environment. During these tests 3 robots operated continuously for several hours, self-charging without any human intervention.

In-Network Computing is a promising field that can be explored to leverage programmable network devices to offload computing towards the edge of the network. This has created great interest in supporting a wide range of network functionality in the data plane. Considering a networked robotics domain, this brings new opportunities to tackle the communication latency challenges. However, this approach opens a room for hardware-level exploits, with the possibility to add a malicious code to the network device in a hidden fashion, compromising the entire communication in the robotic facilities. In this work, we expose vulnerabilities that are exploitable in the most widely used flexible framework for writing robot software, Robot Operating System (ROS). We focus on ROS protocol crossing a programmable SmartNIC as a use case for In-Network Hijacking and In-Network Replay attacks, that can be easily implemented using the P4 language, exposing security vulnerabilities for hackers to take control of the robots or simply breaking the entire system.

As multi-robot systems (MRS) are widely used in various tasks such as natural disaster response and social security, people enthusiastically expect an MRS to be ubiquitous that a general user without heavy training can easily operate. However, humans have various preferences on balancing between task performance and safety, imposing different requirements onto MRS control. Failing to comply with preferences makes people feel difficult in operation and decreases human willingness of using an MRS. Therefore, to improve social acceptance as well as performance, there is an urgent need to adjust MRS behaviors according to human preferences before triggering human corrections, which increases cognitive load. In this paper, a novel Meta Preference Learning (MPL) method was developed to enable an MRS to fast adapt to user preferences. MPL based on meta learning mechanism can quickly assess human preferences from limited instructions; then, a neural network based preference model adjusts MRS behaviors for preference adaption. To validate method effectiveness, a task scenario "An MRS searches victims in an earthquake disaster site" was designed; 20 human users were involved to identify preferences as "aggressive", "medium", "reserved"; based on user guidance and domain knowledge, about 20,000 preferences were simulated to cover different operations related to "task quality", "task progress", "robot safety". The effectiveness of MPL in preference adaption was validated by the reduced duration and frequency of human interventions.

Autonomous navigation of a robot is more challenging in an uncontrolled environment owing to the necessity of coordination among several activities. This includes, creating a map of the surrounding, localizing the robot inside the map, generating a motion plan consistent with the map, executing the plan with control and all other tasks involved concurrently. Moreover, autonomous navigation problems are significant for future robotics applications such as package delivery, security, cleaning, agriculture, surveillance, search and rescue, construction, and transportation which take place in uncontrolled environments. Therefore, an attempt has been made in this research to develop a robot which could function as a security agent for a house to address the aforesaid particulars. This robot has the capability to navigate autonomously in the prescribed map of the operating zone by the user. The desired map can be generated using a Light Detection and Ranging (LiDAR) sensor. For robot navigation, it requires to pick out the robot location accurately itself, otherwise robot will not move autonomously to a particular target. Therefore, Adaptive Monte Carlo Localization (AMCL) method was used to validate the accuracy of robot localization process. Moreover, additional sensors were placed around the building to sense the prevailing security threats from intruders with the aid of the robot.

Surveillance systems involve a camera module (at a fixed location) connected/streaming video via Internet Protocol to a (video) server. In our IMPRINT consortium project, by mounting miniaturised camera module/s on mobile quadruped-lizard like robots, we developed a stealth surveillance system, which could be very useful as a monitoring system in hostage situations. In this paper, we report about the communication system that enables secure transmission of: Live-video from robots to a server, GPS-coordinates of robots to the server and Navigation-commands from server to robots. Since the end application is for stealth surveillance, often can involve sensitive data, data security is a crucial concern, especially when data is transmitted through the internet. We use the RC4 algorithm for video transmission; while the AES algorithm is used for GPS data and other commands’ data transmission. Advantages of the developed system is easy to use for its web interface which is provided on the control station. This communication system, because of its internet-based communication, it is compatible with any operating system environment. The lightweight program runs on the control station (on the server side) and robot body that leads to less memory consumption and faster processing. An important requirement in such hostage surveillance systems is fast data processing and data-transmission rate. We have implemented this communication systems with a single-board computer having GPU that performs better in terms of speed of transmission and processing of data.

The Robot Operation System (ROS) is widely used in academia as well as the industry to build custom robot applications. Successful cyberattacks on robots can result in a loss of control for the legitimate operator and thus have a severe impact on safety if the robot is moving uncontrollably. A high level of security thus needs to be mandatory. Neither ROS 1 nor 2 in their default configuration provide protection against network based attackers. Multiple protection mechanisms have been proposed that can be used to overcome this. Unfortunately, it is unclear how effective and usable each of them are. We provide a structured analysis of the requirements these protection mechanisms need to fulfill by identifying realistic, network based attacker models and using those to derive relevant security requirements and other evaluation criteria. Based on these criteria, we analyze the protection mechanisms available and compare them to each other. We find that none of the existing protection mechanisms fulfill all of the security requirements. For both ROS 1 and 2, we discuss which protection mechanism are most relevant and give hints on how to decide on one. We hope that the requirements we identify simplify the development or enhancement of protection mechanisms that cover all aspects of ROS and that our comparison helps robot operators to choose an adequate protection mechanism for their use case.