Source-linked AI summary
A Survey of Security Research for Operating Systems
Masaki Hashimoto, Ruo Ando, Toshiyuki Maeda, Hidehiko Tanaka
TL;DR
Because information systems are social infrastructure and the OS underpins their security functions, strengthening OS security remains an important issue. The paper surveys virtualization, OS verification, and access control in relation to reference-monitor requirements, concluding that these technologies still face challenges.
Problem
Security functions depend on a sound OS foundation, while the security-support functions an OS should provide to upper layers remain an open issue.
Source: §1 · p. 1Method
Results
The survey organizes recent OS security research into three technology areas and presents the challenges associated with each.
Source: §6 · p. 10Takeaways & Limitations
The paper concludes that security support from a robust OS is indispensable, while the technologies for realizing it still have many challenges.
Source: §6 · p. 10Source-code model checking can require substantial CPU time and memory, while safe-language verification covers basic properties and has a high entry barrier for general OS developers.
Source: §4.2 · p. 6, §4.3 · p. 7
Abstract
from arXiv · showhide
In recent years, information systems have become the social infrastructure, so that their security must be improved urgently. In this paper, we introduce the results of the survey of virtualization, operating system verification and access control technologies in association with the design requirements of the reference monitor. Additionally, we show the prospects and challenges for each technology.
1 Introduction
Because information systems underpin social life, security incidents have become more consequential as systems grow more complex and connected. The paper surveys OS virtualization, verification, and access control research and its challenges.
1 Introduction
- Information systems have become social infrastructure, making security incidents more consequential as system configurations diversify and Internet-connected nodes increase.The paper identifies these developments as factors behind year-on-year increases in security incidents.Source: §1 · p. 1
- The OS underlies security functions such as cryptography and intrusion detection, so vulnerabilities in it undermine their foundation.Even a sound OS leaves open which security-support functions it should provide to upper layers.Source: §1 · p. 1
- Existing OS security efforts, including Trusted OS, SELinux, and Trusted Solaris, reduce threats but are not yet sufficient solutions.Research and implementation efforts remain active.Source: §1 · p. 1
- The paper surveys OS virtualization, program verification, and access control in relation to reference-monitor requirements, then outlines research trends and challenges for each.It introduces its classification policy before presenting the technology-specific sections.Source: §1 · p. 2
2 Security Research in Operating Systems
The paper organizes OS security research around the reference monitor and the OS’s role in the Trusted Computing Base. It maps virtualization, verification, and access control to distinct security concerns and reference-monitor requirements.
2 Security Research in Operating Systems
- The OS traditionally forms the main software component of the Trusted Computing Base because its lowest-layer position lets it capture upper-layer behavior.The OS naturally satisfies reference-monitor requirement (ii), while also providing an execution environment for applications.Source: §2 · p. 2
- The paper classifies OS research by threats to the OS itself and to programs running on it, assigning verification mainly to the former and access control mainly to the latter.Virtualization addresses both; encryption, authentication, and digital forensics are outside the paper’s scope.Source: §2 · p. 2
- Virtualization relates to all three reference-monitor requirements, while virtualization and OS verification relate specifically to requirement (iii), integrity of the TCB.Virtualization is also presented as a foundational technology of cloud computing.Source: §2 · p. 2
- Access control uses a reference monitor to protect the information system and assumes the monitor is complete; its main challenge is controlling other programs.It is associated with reference-monitor requirement (ii).Source: §2 · p. 2
3 OS Virtualization Technology
The section surveys OS virtualization through VM observation, memory and I/O virtualization, and integrity verification, explaining their security roles and future challenges. Its examples span software and hardware mechanisms, with trade-offs in observability, overhead, and isolation.
3 OS Virtualization Technology
- Virtualization research is organized around four areas: hypervisor observation, main-memory virtualization, I/O virtualization, and VM integrity verification.The categories reflect the need for defender-side observability, focus on memory and I/O as observation targets, and hardware-supported integrity checks of execution sequences.Source: §3 · pp. 2–3
3.1 Observation of Virtual Machines by the Hypervisor
- VMI enables hypervisor-side observation, defense, and isolation; active methods sample VM state, while passive methods extract information on events, and external observation is harder to detect but sees less.The hypervisor manages and schedules VM resources, and can support centralized management and security analysis.Source: §3.1 · p. 3
3.2 Virtualization of Main Memory
- VM memory virtualization requires staged address translation; Shadow Paging uses a Shadow Page Table, while hardware-assisted paging can reduce translation and hypervisor implementation loads.HUKO uses Intel VT-d’s EPT to isolate tables and reduce guest paging overhead while strengthening access control; hypervisor-side observation also faces the semantic gap.Source: §3.2 · pp. 3–4
3.3 Virtualization of the I/O Mechanism
- I/O virtualization can use software drivers to capture and relay requests or hardware IOMMUs to remap DMA addresses and protect regions.BitVisor selectively intermediates security-related I/O with a small core, while Intel TXT can prohibit DMA to protected regions.Source: §3.3 · p. 4
3.4 Integrity Verification of Virtual Machines
- VM integrity work includes vTPM attestation, TPM-based trusted boot, HIMA’s TOCTTOU consistency checks, and HyperSentry’s isolated verification of the hypervisor.Trusted boot can establish a chain of trust from boot loader through kernel to applications; HyperSentry uses an out-of-channel path to communicate with a remote verifier.Source: §3.4 · pp. 4–5
3.5 Future Challenges
- Future work must strengthen virtualization security functions as general-purpose OSs grow more complex and their use expands, including hypervisor-based construction and isolation of security regions.The implementation of hypervisors for malware detection and analysis remains a challenge, alongside resolving the semantic gap to detect malicious VM operations.Source: §3.5 · p. 5
4 OS Verification Technology
OS verification applies program-verification techniques to protect OS integrity, using theorem-proving assistants, source-code model checking, and safe programming languages. The section surveys examples and identifies practical-scale and multicore verification as challenges.
4.1 Verification Methods Using Theorem-Proving Assistants
- Theorem-proving assistants can verify any property they can handle, but hand-building proofs makes verification costly.Kit, a roughly 300-line machine-language kernel, had task independence verified with the Boyer-Moore theorem prover.Source: §4.1 · pp. 5–6
- seL4’s implementation was verified against a formal specification using Isabelle/HOL, with about 22 person-years of verification work reported.Because seL4 is a microkernel, complex parts such as memory management are outside the verification target.Source: §4.1 · p. 6
4.2 Verification Methods Using Source-Code Model Checking
- Source-code model checking extracts a model from program source and exhaustively checks its states, but can demand substantial CPU time and memory.SDV verifies Windows device drivers against SLIC specifications, not the OS kernel itself; Verve’s Nucleus was verified by a similar, basically automatic method.Source: §4.2 · p. 6
4.3 Verification Methods Using Safe Programming Languages
- Safe-language type checking automatically verifies basic properties, including freedom from type-error-causing memory operations, but its verifiable properties are limited and adoption has a high entry barrier.SPIN allows type-safe extensions at the kernel’s privilege level, but the kernel body is not verified and its compiler remains in the TCB; TOS also type-checks memory and thread management.Source: §4.3 · pp. 6–7
4.4 Future Challenges
- Practical-scale verification is a future challenge; combining methods is considered realistic, and multicore verification must address shared-memory races and memory consistency.Conventional OS-verification research basically assumes a single-CPU environment.Source: §4.4 · p. 7
5 Access Control Technology
The section surveys OS access control through policy models, policy-description languages, policy verification, and enforcement mechanisms. It reviews representative approaches and identifies differing requirements across cloud, virtualized, and embedded environments as a future challenge.
5.1 Security Policy Models
- Policy models reflect confidentiality, integrity, or combined requirements; examples include Bell-LaPadula, Biba, Clark-Wilson, Chinese Wall, and RBAC.RBAC maps access control to roles and organizational responsibilities, while TBAC organizes authorizations into ordered steps within a procedure.Source: §5.1 · p. 8
5.2 Security Policy Description Languages
- Policy-description languages express access-control specifications, with challenges spanning delegation, restriction, negation, readability, semantics, efficient authorization, and extensibility.SecPAL supports delegated rights across administrative domains; Lithium reasons about negation but cannot concisely express delegation.Source: §5.2 · p. 8
5.3 Security Policy Verification
- Policy verification addresses the difficulty of understanding access-control specifications in large, complex systems.RBAC-PAT analyzes ARBAC properties such as role reachability and information flows; PALMS verifies information flows and consistency for MLS policies, but targets MLS alone.Source: §5.3 · p. 9
5.4 Access Control Mechanisms
- Access-control mechanisms enforce policy rules; ACLs are widely used, while capabilities support least-privilege control.seL4 combines capabilities with a take-grant model; Capsicum supports fine-grained sandboxing, while FLSA separates policy decisions from mandatory enforcement.Source: §5.4 · p. 9
5.5 Future Challenges
- Future work must adapt access control to settings with different requirements and assumptions, including cloud and embedded environments.The section identifies distributed policy models, description languages, and enforcement mechanisms as needed areas of research; FLSA extensions beyond standalone OS-layer targets are also being studied.Source: §5.5 · pp. 9–10
6 Conclusion
The paper organizes OS security research around reference-monitor requirements, surveying virtualization, OS verification, and access control alongside their challenges. It concludes that robust OS security remains essential while changing computing environments bring new demands.
Conclusion
- The survey classifies virtualization, OS verification, and access control in relation to reference-monitor requirements, then organizes each field into subtopics, examples, and challenges.The OS-verification topics are theorem-proving assistants, source-code model checking, and safe programming languages; access-control topics include models, languages, verification, and mechanisms.Source: §6 · p. 10
- The paper argues that robust OS security is indispensable, while the surveyed technologies still face challenges and practical OS principles have changed little for nearly half a century.The conclusion expects OS demands to change more rapidly as new computing environments spread.Source: §6 · p. 10
- The authors hope the survey will serve as a foothold for future work addressing the remaining challenges and supporting information-security research.Source: §6 · p. 10