https://arxiv.org/api/wCXSAQeSx0jmdokWPEY0PBrtljA 2026-06-21T18:35:00Z 1379 195 15 http://arxiv.org/abs/2508.16690v2 2025-12-12T16:05:03Z

Specializing systems to specifics of the workload they serve and platform they are running on often significantly improves performance. However, specializing systems is difficult in practice because of compounding challenges: i) complexity for the developers to determine and implement optimal specialization; ii) inherent loss of generality of the resulting implementation, and iii) difficulty in identifying and implementing a single optimal specialized configuration for the messy reality of modern systems. To address this, we introduce Iridescent, a framework for automated online system specialization guided by observed overall system performance. Iridescent lets developers specify a space of possible specialization choices, and then at runtime generates and runs different specialization choices through JIT compilation as the system runs. By using overall system performance metrics to guide this search, developers can use Iridescent to find optimal system specializations for the hardware and workload conditions at a given time. We demonstrate feasibility, effectivity, and ease of use.

2025-08-21T19:48:50Z Vaastav Anand Deepak Garg Antoine Kaufmann http://arxiv.org/abs/2311.07227v3 2025-12-10T07:41:04Z

This paper presents CARTOS, a charging-aware real-time operating system designed to enhance the functionality of intermittently-powered batteryless devices (IPDs) for various Internet of Things (IoT) applications. While IPDs offer significant advantages such as extended lifespan and operability in extreme environments, they pose unique challenges, including the need to ensure forward progress of program execution amidst variable energy availability and maintaining reliable real-time time behavior during power disruptions. To address these challenges, CARTOS introduces a mixed-preemption scheduling model that classifies tasks into computational and peripheral tasks, and ensures their efficient and timely execution by adopting just-in-time checkpointing for divisible computation tasks and uninterrupted execution for indivisible peripheral tasks. CARTOS also supports processing chains of tasks with precedence constraints and adapts its scheduling in response to environmental changes to offer continuous execution under diverse conditions. CARTOS is implemented with new APIs and components added to FreeRTOS but is designed for portability to other embedded RTOSs. Through real hardware experiments and simulations, CARTOS exhibits superior performance over state-of-the-art methods, demonstrating that it can serve as a practical platform for developing resilient, real-time sensing applications on IPDs.

2023-11-13T10:48:36Z To be published in IEEE Transactions on Emerging Topics in Computing Mohsen Karimi Yidi Wang Youngbin Kim Yoojin Lim Hyoseung Kim http://arxiv.org/abs/2512.09300v1 2025-12-10T04:00:40Z

zkVMs promise general-purpose verifiable computation through ISA-level compatibility with modern programs and toolchains. However, compatibility extends further than just the ISA; modern programs often cannot run or even compile without an operating system and libc. zkVMs attempt to address this by maintaining forks of language-specific runtimes and statically linking them into applications to create self-contained unikernels, but this ad-hoc approach leads to version hell and burdens verifiable applications (vApps) with an unnecessarily large trusted computing base. We solve this problem with ZeroOS, a modular library operating system (libOS) for vApp unikernels; vApp developers can use off-the-shelf toolchains to compile and link only the exact subset of the Linux ABI their vApp needs. Any zkVM team can easily leverage the ZeroOS ecosystem by writing a ZeroOS bootloader for their platform, resulting in a reduced maintainence burden and unifying the entire zkVM ecosystem with consolidated development and audit resources. ZeroOS is free and open-sourced at https://github.com/LayerZero-Labs/ZeroOS.

2025-12-10T04:00:40Z Guangxian Zou Isaac Zhang Ryan Zarick Kelvin Wong Thomas Kim Daniel L. -K. Wong Saeid Yazdinejad Dan Boneh http://arxiv.org/abs/2512.08858v1 2025-12-09T17:50:32Z

Nested virtualization is now widely supported by major cloud vendors, allowing users to leverage virtualization-based technologies in the cloud. However, supporting nested virtualization significantly increases host hypervisor complexity and introduces a new attack surface in cloud platforms. While many prior studies have explored hypervisor fuzzing, none has explicitly addressed nested virtualization due to the challenge of generating effective virtual machine (VM) instances with a vast state space as fuzzing inputs. We present NecoFuzz, the first fuzzing framework that systematically targets nested virtualization-specific logic in hypervisors. NecoFuzz synthesizes executable fuzz-harness VMs with internal states near the boundary between valid and invalid, guided by an approximate model of hardware-assisted virtualization specifications. Since vulnerabilities in nested virtualization often stem from incorrect handling of unexpected VM states, this specification-guided, boundary-oriented generation significantly improves coverage of security-critical code across different hypervisors. We implemented NecoFuzz on Intel VT-x and AMD-V by extending AFL++ to support fuzz-harness VMs. NecoFuzz achieved 84.7% and 74.2% code coverage for nested virtualization-specific code on Intel VT-x and AMD-V, respectively, and uncovered six previously unknown vulnerabilities across three hypervisors, including two assigned CVEs.

2025-12-09T17:50:32Z To appear in EuroSys 2026 Reima Ishii Takaaki Fukai Takahiro Shinagawa 10.1145/3767295.3769347 http://arxiv.org/abs/2512.00400v2 2025-12-09T15:06:30Z

The growing complexity of embedded systems creates tension between rich functionality and strict resource and real-time constraints. Traditional monolithic operating system and hypervisor designs suffer from resource bloat and unpredictable scheduling, making them unsuitable for time-critical workloads where low latency and low jitter are essential. We propose TenonOS, a demand-driven, self-generating, lightweight operating system framework for time-critical embedded systems that rethinks both hypervisor and operating system architectures. TenonOS introduces a LibOS-on-LibOS model that decomposes hypervisor and operating system functionality into fine-grained, reusable micro-libraries. A generative orchestration engine dynamically composes these libraries to synthesize a customized runtime tailored to each application's criticality, timing requirements, and resource profile. TenonOS consists of two core components: Mortise, a minimalist micro-hypervisor, and Tenon, a real-time library operating system. Mortise provides lightweight isolation and removes the usual double-scheduler overhead in virtualized setups, while Tenon provides precise and deterministic task management. By generating only the necessary software stack per workload, TenonOS removes redundant layers, minimizes the trusted computing base, and maximizes responsiveness. Experiments show a 40.28 percent reduction in scheduling latency, an ultra-compact 361 KiB memory footprint, and strong adaptability.

2025-11-29T09:06:40Z Xinkui Zhao Yifan Zhang Haidan Zhao Hao Zhang Qingyu Ma Lufei Zhang Guanjie Cheng Shuiguang Deng Jianwei Yin Zuoning Chen http://arxiv.org/abs/2504.20964v2 2025-12-07T08:44:10Z

We introduce OSVBench, a new benchmark for evaluating Large Language Models (LLMs) on the task of generating complete formal specifications for verifying the functional correctness of operating system kernels. This benchmark is built upon a real-world operating system kernel, Hyperkernel, and consists of 245 complex specification generation tasks in total, each of which is a long-context task of about 20k-30k tokens. The benchmark formulates the specification generation task as a program synthesis problem confined to a domain for specifying states and transitions. This formulation is provided to LLMs through a programming model. The LLMs must be able to understand the programming model and verification assumptions before delineating the correct search space for syntax and semantics and generating formal specifications. Guided by the operating system's high-level functional description, the LLMs are asked to generate a specification that fully describes all correct states and transitions for a potentially buggy code implementation of the operating system. Experimental results with 12 state-of-the-art LLMs indicate limited performance of existing LLMs on the specification generation task for operating system verification. Significant disparities in their performance highlight differences in their ability to handle long-context code generation tasks. The code are available at https://github.com/lishangyu-hkust/OSVBench

2025-04-29T17:34:49Z Shangyu Li Juyong Jiang Tiancheng Zhao Jiasi Shen http://arxiv.org/abs/2411.12893v2 2025-12-06T17:55:14Z

Resource elasticity is one of the key defining characteristics of the Function-as-a-Service (FaaS) serverless computing paradigm. While compute resources assigned to VM-sandboxed functions can be seamlessly adjusted on the fly, memory elasticity remains challenging. Hot(un)plugging memory resources suffers from long reclamation latencies and occupies valuable CPU resources. We identify the obliviousness of the OS memory manager to the hotplugged memory as the key issue hindering hot-unplug performance, and design Squeezy, a novel approach for fast and efficient VM memory hot(un)plug, targeting VM-sandboxed serverless functions. Our key insight is that by segregating hotplugged memory regions from regular VM memory, we are able to bound the lifetime of allocations within these regions thus enabling their fast and efficient reclamation. We implement Squeezy in Linux v6.6 as an extension to the OS memory manager. Our evaluation reveals that Squeezy is an order-of-magnitude faster than state-of-the-art, keeping tail latency bounded, when reclaiming VM memory, achieving sub-second reclamation of multiple GiBs of memory while serving realistic FaaS load.

2024-11-19T22:18:31Z Orestis Lagkas Nikolos National Technical University Of Athens Chloe Alverti University of Illinois Urbana-Champaign Stratos Psomadakis National Technical University Of Athens Georgios Goumas National Technical University Of Athens Nectarios Koziris National Technical University Of Athens http://arxiv.org/abs/2512.06331v1 2025-12-06T07:32:00Z

The design of real-time systems is based on assumptions about environmental conditions in which they will operate. We call this their safe operational envelope. Violation of these assumptions, i.e., out-of-envelope environments, can jeopardize timeliness and safety of real-time systems, e.g., by overwhelming them with interrupt storms. A long-lasting debate has been going on over which design paradigm, the time- or event-triggered, is more robust against such behavior. In this work, we investigate the claim that time-triggered systems are immune against out-of-envelope behavior and how event-triggered systems can be constructed to defend against being overwhelmed by interrupt showers. We introduce importance (independently of priority and criticality) as a means to express which tasks should still be scheduled in case environmental design assumptions cease to hold, draw parallels to mixed-criticality scheduling, and demonstrate how event-triggered systems can defend against out-of-envelope behavior.

2025-12-06T07:32:00Z Published at the RTAutoSec Workshop, which was co-located to ECRTS 2025 Marcus Völp Mohammad Ibrahim Alkoudsi Azin Bayrami Asl Kristin Krüger Julio Rodrigues Mendonca da Neto Gerhard Fohler http://arxiv.org/abs/2512.05555v1 2025-12-05T09:26:08Z

Dynamic data race detectors are indispensable for flagging concurrency errors in software, but their high runtime overhead limits their adoption. This overhead stems primarily from pervasive instrumentation of memory accesses - a significant fraction of which is redundant. We addresses this inefficiency through a static, compiler-integrated approach that identifies and eliminates redundant instrumentation, drastically reducing the runtime cost of dynamic data race detectors. We introduce a suite of interprocedural static analyses reasoning about memory access patterns, synchronization, and thread creation to eliminate instrumentation for provably race-free accesses and show that the completeness properties of the data race detector are preserved. We further observe that many inserted checks flag a race if and only if a preceding check has already flagged an equivalent race for the same memory location - albeit potentially at a different access. We characterize this notion of equivalence and show that, when limiting reporting to at least one representative for each equivalence class, a further class of redundant checks can be eliminated. We identify such accesses using a novel dominance-based elimination analysis. Based on these two insights, we have implemented five static analyses within the LLVM, integrated with the instrumentation pass of the race detector ThreadSanitizer. Our experimental evaluation on a diverse suite of real-world applications demonstrates that our approach significantly reduces race detection overhead, achieving a geomean speedup of 1.34x, with peak speedups reaching 2.5x under high thread contention. This performance is achieved with a negligible increase in compilation time and, being fully automatic, places no additional burden on developers. Our optimizations have been accepted by the ThreadSanitizer maintainers and are in the process of being upstreamed.

2025-12-05T09:26:08Z 35 pages Alexey Paznikov Andrey Kogutenko Yaroslav Osipov Michael Schwarz Umang Mathur http://arxiv.org/abs/2501.16165v3 2025-12-04T09:44:25Z

The Operating System (OS) kernel is foundational in modern computing, especially with the proliferation of diverse computing devices. However, its development also comes with vulnerabilities that can lead to severe security breaches. Kernel fuzzing, a technique used to uncover these vulnerabilities, poses distinct challenges when compared to user-space fuzzing. These include the complexity of configuring the testing environment and addressing the statefulness inherent to both the kernel and the fuzzing process. Despite the significant interest from the community, a comprehensive understanding of kernel fuzzing remains lacking, hindering further progress in the field. In this paper, we present the first systematic study focused specifically on OS kernel fuzzing. We begin by outlining the unique challenges of kernel fuzzing, which distinguish it from those in user space. Following this, we summarize the progress of 107 academic studies from top-tier venues between 2017 and 2025. To structure this analysis, we introduce a stage-based fuzzing model and a novel fuzzing taxonomy that highlights nine core functionalities unique to kernel fuzzing. Each of these functionalities is examined in conjunction with the methodological approaches employed to address them. Finally, we identify remaining gaps in addressing challenges and outline promising directions to guide forthcoming research in kernel security.

2025-01-27T16:03:14Z This work has been accepted by ACM Transactions on Software Engineering and Methodology (TOSEM) Jiacheng Xu He Sun Shihao Jiang Qinying Wang Mingming Zhang Xiang Li Kaiwen Shen Peng Cheng Jiming Chen Charles Zhang Shouling Ji http://arxiv.org/abs/2511.13239v2 2025-12-03T10:47:46Z

Cryptocurrency trading has attracted tremendous attention from both retail and institutional investors. However, most traders fail to scale their assets under management due to fragile strategies that collapse during adverse markets. The primary causes are oversized leverage, speculative position sizing, and the absence of robust risk management or hedging mechanisms. This paper introduces Talyxion, an end to end framework for crypto portfolio allocation that shifts the paradigm from speculation to optimization. The proposed pipeline consists of four stages: universe selection, alpha backtesting, volatility aware portfolio optimization, and dynamic drawdown based risk management. By combining operations research techniques with practical risk controls, Talyxion enables scalable crypto portfolios that can withstand market downturns. In live 30 day trading on Binance Futures, the framework achieved a return on investment (ROI) of +16.68%, with the Sharpe ratio reaching 5.72 and the maximum drawdown contained at just 4.56%, demonstrating strong downside risk control. The system executed 227 trades, of which 131 were profitable, resulting in a win rate of 57.71% and a PnL of +1,137.49 USDT. Importantly, these results outperformed the buy and hold baseline (Sharpe 1.79, ROI 4.36%, MDD 4.96%) as well as several top leader copy trading bots on Binance, highlighting both the competitiveness and scalability of Talyxion in real world trading environments.

2025-11-17T11:03:42Z Thanh Nguyen http://arxiv.org/abs/2512.03279v1 2025-12-02T22:38:44Z

We present Mirror-Optimized Storage Tiering (MOST), a novel tiering-based approach optimized for modern storage hierarchies. The key idea of MOST is to combine the load balancing advantages of mirroring with the space-efficiency advantages of tiering. Specifically, MOST dynamically mirrors a small amount of hot data across storage tiers to efficiently balance load, avoiding costly migrations. As a result, MOST is as space-efficient as classic tiering while achieving better bandwidth utilization under I/O-intensive workloads. We implement MOST in Cerberus, a user-level storage management layer based on CacheLib. We show the efficacy of Cerberus through a comprehensive empirical study: across a range of static and dynamic workloads, Cerberus achieves better throughput than competing approaches on modern storage hierarchies especially under I/O-intensive and dynamic workloads.

2025-12-02T22:38:44Z 18 pages, to be published in 24th USENIX Conference on File and Storage Technologies (FAST '26) Kaiwei Tu Kan Wu Andrea C. Arpaci-Dusseau Remzi H. Arpaci-Dusseau http://arxiv.org/abs/2511.09956v2 2025-12-02T01:24:46Z

This paper shows that cache-based optimizations are often ineffective in cloud virtual machines (VMs) due to limited visibility into and control over provisioned caches. In public clouds, CPU caches can be partitioned or shared among VMs, but a VM is unaware of cache provisioning details. Moreover, a VM cannot influence cache usage via page placement policies, as memory-to-cache mappings are hidden. The paper proposes a novel solution, CacheX, which probes accurate and fine-grained cache abstraction within VMs using eviction sets without requiring hardware or hypervisor support, and showcases the utility of the probed information with two new techniques: LLC contention-aware task scheduling and virtual color-aware page cache management. Our evaluation of CacheX's implementation in x86 Linux kernel demonstrates that it can effectively improve cache utilization for various workloads in public cloud VMs.

2025-11-13T04:37:52Z Mani Tofigh Edward Guo Weiwei Jia Xiaoning Ding Zirui Neil Zhao Jianchen Shan http://arxiv.org/abs/2512.01381v1 2025-12-01T07:54:48Z

Accurate estimation of the Worst-Case Deadline Failure Probability (WCDFP) has attracted growing attention as a means to provide safety assurances in complex systems such as robotic platforms and autonomous vehicles. WCDFP quantifies the likelihood of deadline misses under the most pessimistic operating conditions, and safe estimation is essential for dependable real-time applications. However, achieving high accuracy in WCDFP estimation often incurs significant computational cost. Recent studies have revealed that the classical assumption of the critical instant, the activation pattern traditionally considered to trigger the worst-case behavior, can lead to underestimation of WCDFP in probabilistic settings. This observation motivates the use of a revised critical instant formulation that more faithfully captures the true worst-case scenario. This paper investigates convolution-based methods for WCDFP estimation under this revised setting and proposes an optimization technique that accelerates convolution by improving the merge order. Extensive experiments with diverse execution-time distributions demonstrate that the proposed optimized Aggregate Convolution reduces computation time by up to an order of magnitude compared to Sequential Convolution, while retaining accurate and safe-sided WCDFP estimates. These results highlight the potential of the approach to provide both efficiency and reliability in probabilistic timing analysis for safety-critical real-time applications.

2025-12-01T07:54:48Z 8 pages, 5 figures. Proceedings of APRIS2025 Proceedings of 8th Asia Pacific Conference on Robot IoT System Development and Platform (APRIS2025), 2025, pp. 1-8 Hiroto Takahashi Atsushi Yano Takuya Azumi http://arxiv.org/abs/2512.16926v1 2025-11-28T15:17:18Z

This paper addresses limitations of current scheduling methods in the Robot Operating System (ROS)2, focusing on scheduling tasks beyond simple chains and analyzing arbitrary Directed Acyclic Graphs (DAGs). While previous research has focused mostly on chain-based scheduling with ad-hoc response time analyses, we propose a novel approach using the events executor to implement fixed-job-level-priority schedulers for arbitrary ROS2 graphs on uniprocessor systems. We demonstrate that ROS 2 applications can be abstracted as forests of trees, enabling the mapping of ROS 2 applications to traditional real-time DAG task models. Our usage of the events executor requires a special implementation of the events queue and a communication middleware that supports LIFO-ordered message delivery, features not yet standard in ROS2. We show that our implementation generates the same schedules as a conventional fixed-priority DAG task scheduler, in spite of lacking access to the precedence information that usually is required. This further closes the gap between established real-time systems theory and ROS2 scheduling analyses.

2025-11-28T15:17:18Z 18 pages, 5 figure Oren Bell Harun Teper Mario Günzel Chris Gill Jian-Jia Chen