Formal verification offers strong guarantees of correctness, robustness, and security. However, these guarantees depend on specification correctness, and even minor flaws can invalidate proofs and introduce critical vulnerabilities. We present Scope, an automated system that identifies specification inconsistencies by combining formal modeling with rule-based consistency checking. Unlike traditional approaches that rely on implementations, Scope treats the specification as the sole ground truth. It translates the specification into a machine-verifiable model using Verus and SMT solvers, then detects inconsistencies in success/failure conditions, dependency rules, and state transitions. We apply Scope to the Realm Management Monitor (RMM) specifications for Arm's Confidential Compute Architecture (CCA), uncovering 35 previously unknown bugs—including security-critical flaws in ABI semantics and missing state transitions—all confirmed by Arm. Compared to modern LLM-based tools, Scope improves inconsistency-detection precision by 7x over GPT-o1 and up to 40× over leading chat models (LLaMA 3.1, GPT-4o, Claude 3.7).

Fuzzing is arguably the most practical approach for detecting security bugs in software, but a non-trivial extent of efforts is required for its adoption. To be effective, high-quality fuzz drivers should be first formulated with a proper sequence of APIs that can exhaustively explore the program states. To alleviate this burden, existing solutions attempt to generate fuzz drivers either by inferring the valid sequences of APIs from the consumer code (i.e., actual uses of APIs) or by directly extracting them from sample executions. Unfortunately, all existing approaches suffer from a common problem: the observed API sequences, either statically inferred or dynamically monitored, are intermingled with custom application logics. However, we observed that the unit tests are carefully crafted by the actual designer of the APIs to validate their proper usages, and importantly, it is a common practice to write the unit tests during their development (e.g., over 70% of popular GitHub projects).In this paper, we propose, UTopia, an open-source tool and analysis algorithm that can automatically synthesize effective fuzz drivers from existing unit tests with near-zero human involvement. To demonstrate its effectiveness, we applied UTopia to 55 open-source project libraries, including Tizen and Node.js, and automatically generated 5K fuzz drivers from 8K eligible unit tests. In addition, we executed the generated fuzzers for approximately 5 million per-core hours and discovered 123 bugs. More importantly, 2.4K of the generated fuzz drivers were adopted to the continuous integration process of the Tizen project, indicating the quality of the synthesized fuzz driver. The proposed tool and results are publicly available and maintained for a broader adoption among both researchers and practitioners.

Owing to the benefits of system virtualization, even CE devices have come to take advantage of the technology. However, due to the lack of windowing system which fits virtualization-based CE devices, it is not only inefficient but also difficult for end users to utilize the CE devices running multiple domains. In this paper we present an effective virtual window system for CE devices based on system virtualization. Our approach has three major advantages: (1) by modifying X window system, it provides shared windowing services between domains without dependency of a specific network protocol; (2) by providing a unified graphical user interface which integrates icons of all the applications from every domain, it frees users from remembering which applications are located in which domain and from doing tedious operations for application launching and installation; (3) it provides efficiency in terms of size (storage and memory) and performance to CE devices. We have implemented a prototype of the virtual window system on the basis of Secure Xen on ARM. Our evaluation shows that our approach is usable and efficient enough to be practically adopted for CE devices based on system virtualization.

System virtualization is now available for mobile devices allowing for many advantages. Two of the major benefits from virtualization are system fault isolation and security. The isolated driver domain (IDD) model, a widely adopted architecture, enables strong system fault isolation by limiting the impact of driver faults to the driver domain itself. However, excessive I/O requests from a malicious domain to an IDD can cause CPU overuse of the IDD and performance degradation of applications in the IDD and other domains that share the same I/O device with the malicious do-main. If the IDD model is applied to mobile devices, this failure of performance isolation could also lead to battery drain, and thus it introduces a new severe threat to mobile devices. In order to solve this problem, we propose a fine-grained I/O access control mechanism in an IDD. Requests from guest domains are managed by an accounting module in terms of CPU usage, with the calcula-tion of estimated CPU consumption using regression equations. The requests are scheduled by an I/O access control enforcer ac-cording to security policies. As a result, our mechanism provides precise control on the CPU usage of a guest domain due to I/O device access, and prevents malicious guest domains from CPU overuse, performance degradation, and battery drain. We have implemented a prototype of our approach considering both network and storage devices with a real smart phone (SGH-i780) that runs two para-virtualized Linux kernels on top of Secure Xen on ARM. The evaluation shows our approach effectively protects a smart phone against excessive I/O attacks and guarantees availability.

In this paper we present a multi-layer mandatory access control mechanism (ACM) for mobile devices based on system virtualization technology. We discuss a detailed threat model to mobile devices in the real world to develop an ACM fitted to mobile devices. Then, we propose a novel multi-layer access control mechanism for mobile devices, which provides strong protection against the identified mobile threats as well as performance efficiency. Our Virtual Machine Monitor (VMM) and secure domain have independent access control modules to effectively control mobile device's resources. Access control module at VMM controls access requests from a domain to physical/virtual resources in order to confine sharing resources among domains for confidentiality. It also protects a mobile device against DoS attacks draining limited system resources such as battery and memory to guarantee availability. In addition, access control at secure domain enforces fine-grained control of resources (e.g., file system access control) in upper layer without degrading performance of a mobile device due to additional hypercall invocations. Furthermore, there is no bypass of our access control since our ACM is placed inside VMM which is simple and small enough to verify its safety and we eliminated the chance of VMM corruption by checking integrity of VMM including ACM during bootstrap time.

We will demonstrate a prototype of the beyond 3G mobile terminal based on system virtualization technology, which meets both security and flexibility requirements. In the proposed architecture, two domains, secure domain and normal domain, run on top of secure virtual machine monitor (VMM) which includes mandatory access control and domain integrity check mechanisms. Only security critical applications and services (e.g., banking, trading, and DRM) can run on the secure domain, and malware is prohibited from accessing the secure domain. Both flexibility and rich user experiences are provided by allowing users to install and execute application software, which might be potentially vulnerable, on the normal domain. Even in the case of malware attack, it cannot cause security threats to the secure domain because of the isolation and our access control features. This demonstration will show how secure our mobile terminal is against malware attacks compared to conventional single OS based mobile terminal.