Abstract In automotive engineering, vehicle platooning is a proposed method for improving convoy movements by coordinating them to increase the safety and efficiency of transportation systems. The complexity and stochastic nature of platooning systems provide difficulties for traditional model-checking techniques. However, Statistical Model Checking (SMC) offers a solution by using statistical inference to probabilistically evaluate system features. This paper shows that Uppaal SMC offers a robust framework for assessing platooning systems across various operational scenarios, combining statistical analysis and formal verification methodologies. The behaviour of the platoon is modelled stochastically to cover a wide range of driving scenarios and road surfaces. Using SMC, it has been possible to gauge the safety and functionality of the platoon by estimating the probability of several properties.

In modern day applications, eBPF has emerged as a powerful mechanism for extensible networking, observability, and security. Yet its elevated in-kernel privileges also create new attack avenues, since third-party tooling and supply-chain compromises can introduce malicious BPF loaders. A stealthy attacker may embed trojaned eBPF programs in legitimate tools and application or exploit vulnerable plugins to gain CAP_BPF rights, then probe syscalls, trace kernel events and exfiltrate sensitive data; often without raising traditional alarms. In this paper we propose a threat model to encompass these attack vectors for infrastructure administrator and semi-trusted cloud environment where BPF itself becomes both a tool and a target. We introduce BPF-to-BPF Armor (BBArmor), a prototype solution that enforces stricter controls over BPF syscall usage, isolates BPF programs based on provenance and trust levels and blocks anomalous BPF interactions indicative of compromise. Our evaluation demonstrates that BBArmor mitigates BPF syscall misuse with minimal performance overhead, strengthening security against evolving supply-chain and software-supply threats.

Deepfakes are a type of synthetic media created using artificial intelligence, specifically deep learning algorithms. This technology can for example superimpose faces and voices onto videos, creating hyper-realistic but artificial representations. Deepfakes pose significant risks regarding misinformation and fake news, because they can spread false information by depicting public figures saying or doing things they never did, undermining public trust. In this paper, we propose a method that leverages BLS signatures (Boneh, Lynn, and Shacham 2004) to implement signatures that remain valid after image cropping, but are invalidated in all the other types of manipulation, including deepfake creation. Our approach does not require who crops the image to know the signature private key or to be trusted in general, and it is ${\mathcal{O}}(1)$ in terms of signature size, making it a practical solution for scenarios where images are disseminated through web servers and cropping is the primary transformation. Finally, we adapted the signature scheme for the JPEG standard, and we experimentally tested the size of a signed image.

Virtual switches are one of the most important building blocks in public cloud network stacks as they apply high-level policies to traffic enabling communication between virtual machines (VMs) and the rest of the world. The problem is that virtual switches need CPU cores to process packets and the more cores assigned to them, the less are available to VMs that are rented to customers and hence generate revenue. With this paper, we show that it is potentially possible to find a sweet-spot between performance and costs. The insight is that applications running on VMs are not always using 100% of their CPU processing power: we use this to design switch bypass, a new technique that allow virtual switches to opportunistically offload part of their processing to the virtual NIC drivers associated with guest VMs. Using packet classification as use-case, we show that with switch bypass we obtain a performance boost up to 40% without the need of additional core processing power.

Rust is a multi-paradigm, general-purpose programming language that prioritizes performance, type safety, and fearless concurrency. At compile time, Rust is able to ensure memory and thread safety without relying on automated memory management techniques such as garbage collection. As a result, Rust is gaining significant popularity as a replacement for $\mathrm{C} / \mathrm{C}++$ in various domains where performance and reliability are paramount, such as systems programming, embedded devices, and networking. This paper attempts to critically evaluate the claims of high performance and memory safety associated with Rust, particularly in the context of low-level network programming. The approach involves rewriting Nethuns, a fast C-based network I/O library, using Rust. The Rust-based implementation of Nethuns is described in detail in this work, with a particular emphasis on explaining the design choices, highlighting the primary benefits gained in terms of safety and security, and addressing the challenges encountered throughout the process. The paper concludes with a performance evaluation of the library. The obtained results are promising: the Rust-based library ensures a significantly higher level of safety at compile time, with a modest performance trade-off.

Virtual Machines are the key technology in cloud computing. In order to upgrade, repair or service the physical machine where a Virtual Machine is hosted, a common practice is to live-migrate the Virtual Machine to a different server. This involves copying all the guest memory over the network, which may take a non-negligible amount of time. In this work, we propose a technique to speed up the migration time by reducing the amount of guest memory to be transferred with the help of the guest OS. In particular, during live-migration, an eBPF program is injected in the guest kernel to obtain, and send to the Virtual Machine Monitor, the list of guest page frames that are currently unused. The VMM can then safely skip these pages during the copy. We have integrated this technique in the live-migration implementation of QEMU (Bellard, 2005), and we show the effects of our work in some experiments comparing the results against the QEMU default implementation.

Modern multi-core servers are powerful enough to process multi-gigabit live packet streams on the network data plane. However, in most cases network programmers must build their applications from scratch, by implementing both the interfaces towards the lower hardware level and the proper mechanisms for parallel programming. Data Stream Processing (DaSP) frameworks have recently emerged as promising approaches to overcome the above issues and to let programmers simply focus on the logic of the application to develop. However, DaSP platforms are generally not designed for the networking domain, in terms of both performance and functions. In this paper, we selected the WindFlow DaSP framework and built suitable extensions to attach multiple (accelerated) packet sources of data to it. We then implemented a simple monitoring application on top of WindFlow and carried out stress tests with synthetic and real traffic. The results prove that performance scale linearly with the processing cores so that the application was able to process the whole amount of live data up to nearly 20 Gbps rate.

Cloud providers are continuously evolving their virtual networking infrastructure to improve performance and functionality. This evolution, however, typically stops at the virtual NIC interface, since any change in that domain would require impractical upgrades in the running VMs with the collaboration of the customers who own them. This could hinder many important evolutions, like the transition to newer revisions of the VirtIO standard. To overcome this problem we propose BPFHV, a new paravirtualized network meta-device that is able to dynamically change its internal operation under the hypervisor control. BPFHV comes with a set of hypervisor-provided callbacks that the guest must call to complete datapath operations, such as posting a new packet for transmission. By injecting new callbacks, the hypervisor can dynamically change the behaviour of the device and of its guest driver even after the initial deployment of a VM. We describe our prototype implementation on the QEMU hypervisor with Linux guests, reusing the eBPF infrastructure for code injection. We show some preliminary experimental results and discuss some possible further applications.

Summary Data processing pipelines normally use lockless Single‐Producer–Single‐Consumer (SPSC) queues to efficiently decouple their processing threads and achieve high throughput, minimizing the cost of synchronization. SPSC queues have been widely studied, mostly for applications such as streaming data or network monitoring, where the main goal is maximizing throughput. There are now many applications, such as virtual‐machine–virtual‐machine communication, software‐defined networking, and message‐based kernels, where low latency is also important, and the tradeoffs between high‐throughput and low‐latency algorithms have not been studied equally well. Furthermore, at high or variable transaction rates, the effect of memory hierarchies and cache coherence subsystems may be dominant and yield surprising results. In this paper, we make two contributions. First, we provide a comprehensive study of the two main families of SPSC queues, namely, “Lamport” and “FastForward” queues, with a detailed analytical and experimental characterization of their behavior in terms of operating regimes, throughput, latency, and cache misses. Second, we propose two new queue variants, namely, improved FastForward and batched improved FastForward, which have better worst‐case behavior than other variants in terms of cache misses, which is an important feature for a number of applications. Together, these two contributions provide practical guidelines to choose the best solution depending on the application requirements.

In this study, we investigate some counterintuitive but frequent performance issues that arise when doing high-speed networking (or I/O in general) with Virtual Machines (VMs). VMs use one or more single-producer/single-consumer systems to exchange I/O data (e.g. network packets) with their hypervisor. We show that when the producer and the consumer process packets at different rates, the high cost required for synchronization (interrupts and ‘kicks’) may reduce throughput of the system well below the slowest of the two parties; moreover, accelerating the faster party may cause the throughput to decrease. Our work provides a model for throughput, efficiency and latency of producer/consumer systems when notifications or sleeping are used as a synchronization mechanism; identifies different operating regimes depending on the operating parameters; validates the accuracy of our model against a VirtIO-based prototype, taking into account most of the details of real-world deployments; provides practical and robust strategies to maximize throughput and minimize energy while keeping the latency under control, without depending on precise timing measurements nor unreasonable assumptions on the system’s behavior. The study is particularly interesting for Network Function Virtualization deployments, where high-rate producer/consumer systems in virtualized environments are the core components.

Tenants in a cloud environment run services, such as Virtual Network Function instantiations, that may legitimately generate millions of packets per second. The hosting platform, hence, needs robust packet scheduling mechanisms that support these rates and, at the same time, provide isolation and dependable service guarantees under all load conditions. Current hardware or software packet scheduling solutions fail to meet all these requirements, most commonly lacking on either performance or guarantees. In this paper we propose an architecture, called PSPAT to build efficient and robust software packet schedulers suitable to high speed, highly concurrent environments. PSPAT decouples clients, scheduler and device driver through lock-free mailboxes, thus removing lock contention, providing opportunities to parallelize operation, and achieving high and dependable performance even under overload. We describe the operation of our system, discuss implementation and system issues, provide analytical bounds on the service guarantees of PSPAT, and validate the behavior of its Linux implementation even at high link utilization, comparing it with current hardware and software solutions. Our prototype can make over 28 million scheduling decisions per second, and keep latency low, even with tens of concurrent clients running on a multi-core, multi-socket system.

Network Function Virtualization has been touted as the silver bullet for tackling a number of operator problems, including vendor lock-in, fast deployment of new functionality, converged management, and lower expenditure since packet processing runs on inexpensive commodity servers. The reality, however, is that, in practice, it has proved hard to achieve the stable, predictable performance provided by hardware middleboxes, and so operators have essentially resorted to throwing money at the problem, deploying highly underutilized servers (e.g., one NF per CPU core) in order to guarantee high performance during peak periods and meet SLAs.

This work addresses an apparently simple but elusive problem that arises when doing high speed networking on Virtual Machines. When a VM and its peer (usually the hypervisor) process packets at different rates, the work required for synchronization (interrupts and "kicks") may reduce throughput well below the slowest of the two parties.

The rising interest in Network Function Virtualization (NFV) requires Virtual Machines (VMs) to operate with diversified networking workloads, from traditional, bulk TCP transfers to novel ones featuring extremely high packet rates. In response, researchers have explored and proposed new solutions for high performance VM networking, including optimizations to virtual network adapters (such as VirtIO) to support high speed bulk traffic, and alternative frameworks for userspace networking and physical or virtual passthrough. To date, we are still missing a comprehensive solution that supports such extreme workloads across multiple operating systems and hypervisors, while at the same time addressing other requirements such as ease of configuration, operating system independence, scalability and isolation. In this paper we present ptnet, an approach to network I/O virtualization that provides high performance for both traditional TCP/IP and high packet rate applications. ptnet leverages the features of the netmap framework (including virtualization and passthrough support), and defines a simple yet performant network device model that can be easily supported in different operating systems and hypervisors. We prove the effectiveness of our approach by comparing ptnet's performance with one of the state of the art I/O virtualization solutions, namely VirtIO on Linux and QEMU/KVM. ptnet is available under a BSD license as part of the netmap distributions on github.

In this work we discuss the limitations of link emulators based on conventional network stacks, and present our alternative architecture called TLEM, which is designed to address current high speed links and be open to future speed improvements. TLEM is structured as a pipeline of stages, implemented with separate threads and with limited interactions with each other, so that high performance can be achieved. Our emulator can handle bidirectional traffic at speeds of over 18 Mpps (64 byte packets) and 40 Gbit/s (1500 byte packets) per direction even with large emulation delays. Even higher performance can be achieved with shorter delays, as the workload fits better into the L3 cache of the system. TLEM is distributed as BSD-licensed opensource as part of the netmap distributions, and runs on any system that supports netmap (this includes FreeBSD, Linux and now even Windows).

Supporting network I/O at high packet rates in virtual machines is fundamental for the deployment of Cloud data centers and Network Function Virtualization. Historically, SR-IOV and hardware passthrough were thought as the only viable solution to reduce the high cost of virtualization. In previous work [15] we showed how even plain device emulation can achieve VM-to-VM speeds of millions of packets per second (Mpps), though still at least 3 times slower than bare metal. In this paper, to fill this gap, we present ptnetmap, a virtual passthrough network device (based on the netmap framework). ptnetmap allows VMs to connect to any netmap port (physical devices, software switches, netmap pipes), conserving the speed and isolation of the native netmap system, and removing the constraints of hardware passthrough. Our work includes two key features not present in previous proposals: we provide a high speed path also to untrusted VMs, and do not require dedicated polling cores/threads, which is fundamental to achieve an efficient use of resources. Besides these features, our speed is also beyond previously published values. Running on top of ptnetmap, VMs can saturate a 10 Gbit link at 14.88 Mpps, talk at over 20 Mpps to untrusted VMs, and over 70 Mpps to trusted VMs. ptnetmap extends the netmap framework, and currently supports Linux and FreeBSD guests, and QEMU/KVM host. Support for bhyve/FreeBSD host is under development.

Equivalence checking plays a crucial role in formal verification to ensure the correctness of concurrent systems. However, this method cannot be scaled as easily with the increasing complexity of systems due to the state explosion problem. This article presents an efficient procedure, based on heuristic search, for checking Milner's strong and weak equivalence; to achieve higher efficiency, we actually search for a difference between two processes to be discovered as soon as possible, thus the heuristics aims to find a counterexample, even if not the minimum one, to prove nonequivalence. The presented algorithm builds the system state graph on-the-fly, during the checking, and the heuristics promotes the construction of the more promising subgraph. The heuristic function is syntax based, but the approach can be applied to different specification languages such as CCS, LOTOS, and CSP, provided that the language semantics is based on the concept of transition. The algorithm to explore the search space of the problem is based on a greedy technique; GreASE (Greedy Algorithm for System Equivalence), the tool supporting the approach, is used to evaluate the achieved reduction of both state-space size and time with respect to other verification environments.

Most of the work on VM network performance has focused so far on bulk TCP traffic, which covers classical applications of virtualization. Completely new “paravirtualized devices” (Xenfront, VIRTIO, vmxnet) have been designed and implemented to improve network throughput. We expect virtualization to become widely used also for different workloads: packet switching devices and middleboxes, Software Defined Networks, etc.. These applications involve very high packet rates that are problematic not only for the hypervisor (which emulates network interfaces) but also for the host itself (which switches packets between guests and physical NICs). In this paper we provide three main results. First, we demonstrate how rates of millions of packets per second can be achieved even within VMs, with limited but targeted modifications on device drivers, hypervisors and the host's virtual switch. Secondly, we show that emulation of conventional NICs (e.g., Intel e1000) is perfectly capable of achieving such packet rates, without requiring completely different device models. Finally, we provide sets of modifications suitable for different use cases (acting only on the guest, or only on the host, or on both) which can improve the network throughput of a VM by 20 times or more. These results are important because they enable a new set of applications within virtual machines. In particular, we achieve guest-to-guest UDP speeds of over 1 Mpps with short frames (and 6 Gbit/s with 1500-byte frames) using a conventional e1000 device, and socket-based sender/receivers. This matches the speed of the OS on bare metal. Furthermore, we reach over 5 Mpps when guests use the netmap API. Our work requires only small changes to device drivers (about 100 lines, both for FreeBSD and Linux version of e1000), similarly small modifications to the hypervisor (we have a QEMU prototype available) and the use of the VALE switch as a network backend. Relevant changes are being incorporated and/or distributed as external patches for FreeBSD, QEMU and Linux.

The growing popularity of virtual machines is pushing the demand for high performance communication between them. Past solutions have seen the use of hardware assistance, in the form of "PCI passthrough" (dedicating parts of physical NICs to each virtual machine) and even bouncing traffic through physical switches to handle data forwarding and replication.

We propose the technique of Adaptive Allele Consolidation, that greatly improves the performance of the Lange-Goradia algorithm for genotype elimination in pedigrees, while still producing equivalent output. Genotype elimination consists in removing from a pedigree those genotypes that are impossible according to the Mendelian law of inheritance. This is used to find errors in genetic data and is useful as a preprocessing step in other analyses (such as linkage analysis or haplotype imputation). The problem of genotype elimination is intrinsically combinatorial, and Allele Consolidation is an existing technique where several alleles are replaced by a single “lumped” allele in order to reduce the number of combinations of genotypes that have to be considered, possibly at the expense of precision. In existing Allele Consolidation techniques, alleles are lumped once and for all before performing genotype elimination. The idea of Adaptive Allele Consolidation is to dynamically change the set of alleles that are lumped together during the execution of the Lange-Goradia algorithm, so that both high performance and precision are achieved. We have implemented the technique in a tool called Celer and evaluated it on a large set of scenarios, with good results.

Bytecode verification is a key point in the security chain of the Java platform. This feature is only optional in many embedded devices since the memory requirements of the verification process are too high. In this article we propose an approach that significantly reduces the use of memory by a serial/parallel decomposition of the verification into multiple specialized passes. The algorithm reduces the type encoding space by operating on different abstractions of the domain of types. The results of our evaluation show that this bytecode verification can be performed directly on small memory systems. The method is formalized in the framework of abstract interpretation.

Java applets run on a Virtual Machine that checks code integrity and correctness before execution using a module called the Bytecode Verifier. Java Card technology allows Java applets to run on smart cards. The large memory requirements of the verification process do not allow the implementation of an embedded Bytecode Verifier in the Java Card Virtual Machine. To address this problem, we propose a verification algorithm that optimizes the use of system memory by imposing an ordering on the verification of the instructions. This algorithm is based on control flow dependencies and immediate postdominators in control flow graphs.

We present a thorough analysis of the memory behaviour of page caching and prefetching algorithms. The analysis is restricted to programs whose execution consists of iteration of a sequence of page accesses. Program activity is characterized in terms of utilization of system resources. A graphical model of program execution is used to describe both page placement in the primary memory and the actions of page fetch and replacement. The algorithms are compared from the point of view of a number of performance indexes that include program response time and utilization of the secondary memory system. Special attention is paid to transient program behaviour and the effects of the time necessary for the processor to control the disk activities of page fetch. The results of a large set of measurement experiments are used to validate the analytical model and acquire significant indications concerning the extent of the simplifying assumptions made in the theoretical analysis. The discussion of the relation to previous work makes special reference to two classes of algorithms that received much attention in the past, aggressive prefetching and informed prefetching.

Abstract A method is presented for checking secure information flow in Java bytecode, assuming a multilevel security policy that assigns security levels to the objects. The method exploits the type‐level abstract interpretation of standard bytecode verification to detect illegal information flows. We define an algorithm transforming the original code into another code in such a way that a typing error detected by the Verifier on the transformed code corresponds to a possible illicit information flow in the original code. We present a prototype tool that implements the method and we show an example of application. Copyright © 2004 John Wiley & Sons, Ltd.

Abstract A method is proposed for checking security properties in programs written in high‐level languages. The method is based on the model checking technique. The SMV tool is used. The representation of the program is a Kripke structure modelling the control flow graph enriched with security information. The properties considered are secure information flow and the absence of covert channels caused by program termination. The formulae expressing these security properties are given using the logic CTL. Copyright © 2003 John Wiley & Sons, Ltd.

When an applet is sent over the internet, Java Virtual Machine code is transmitted and remotely executed. Because untrusted code can be executed on the local computer running the web browser security problems may arise. We present a method to check illicit flows in Java bytecode, that exploits the type-level abstract interpretation of bytecode verification. We present an algorithm transforming a bytecode into another one that, when abstractly executed by the standard bytecode verifier, reveals illicit information flows. We show an example of application of the method.