Fábio Coutada
059f96c948
- HARD_REALTIME_EVALUATION.md: full HRT audit - MICROKERNEL_*.md: complete architecture targets and implementation plan - PIKEOS_3LAYER_REPLICATION_PLAN.md: 3-layer replication strategy - PIKEOS_POSIX_AUDIT.md: POSIX compliance audit - RTOS_AUDIT.md: RTOS comparison - XTENSA_AUDIT.md: Xtensa ISA audit - BIBLIOGRAPHY_SAFETY_CRITICAL_HYPERVISOR.md: references
187 lines
8.2 KiB
Markdown
187 lines
8.2 KiB
Markdown
# Bibliography: Safety-Critical Hypervisor Design
|
|
|
|
**Compiled:** 2026-07-14
|
|
**Purpose:** Academic and industry references for UniversalisOS PikeOS 3-layer replication
|
|
|
|
---
|
|
|
|
## 1. PikeOS Architecture
|
|
|
|
1. **SYSGO AG. "PikeOS 5.0 Reference Manual."** SYSGO GmbH, 2023.
|
|
- Primary reference for 3-layer architecture (kernel → P4EXT → POSIX)
|
|
- 119 syscalls, ARINC 653 time partitioning, DO-178C DAL A certification
|
|
|
|
2. **SYSGO AG. "PikeOS — The Separation Kernel for Critical Systems."** White Paper.
|
|
- Static partitioning model, no fork/exec, task activation via p4_task_activate()
|
|
- POSIX PSE51 personality with _POSIX_SPAWN=-1 (no dynamic process creation)
|
|
|
|
3. **Nordlander, J. "PikeOS — A Different Approach to Embedded Virtualization."** Embedded World Conference, 2009.
|
|
- PikeOS as paravirtualized microkernel (NOT hardware virtualization)
|
|
- Isolation via page table partitioning + I/O port bitmap filtering
|
|
|
|
4. **Kaiser, R. & Wagner, S. "Evolution of the PikeOS Microkernel."** International Workshop on Microkernel-based Systems, 2012.
|
|
- PikeOS architecture evolution, syscall design, certification approach
|
|
|
|
---
|
|
|
|
## 2. Microkernel Formal Verification
|
|
|
|
5. **Klein, G. et al. "seL4: Formal Verification of an OS Kernel." SOSP, 2009.**
|
|
- First formally verified OS kernel (10,000 LOC C + 200 LOC ASM)
|
|
- Proof chain: binary ↔ C ↔ abstract spec ↔ high-level spec (Isabelle/HOL)
|
|
- Relevance: Gold standard for microkernel verification
|
|
|
|
6. **Heiser, G. "The seL4 Microkernel — An Introduction." Technical Report, 2020.**
|
|
- seL4 capability system, IPC mechanism, scheduling
|
|
- Relevance: Capability-based access control applicable to UniversalisOS
|
|
|
|
7. **Klein, G. et al. "Comprehensive Formal Verification of an OS Microkernel." TOCS, 2014.**
|
|
- Full functional correctness proof of seL4 including C-level refinement
|
|
- 25 person-years of effort, Isabelle/HOL theorem prover
|
|
|
|
8. **Sewell, T. et al. "Translation Validation for a Verified OS Kernel." PLDI, 2013.**
|
|
- Verified compilation from C to ARM assembly
|
|
- Relevance: How to verify the compiler output matches the C source
|
|
|
|
---
|
|
|
|
## 3. ARINC 653 Partitioning
|
|
|
|
9. **ARINC. "ARINC 653: Avionics Application Software Standard Interface." AEEC, 2016.**
|
|
- Partition management, process management, health monitoring
|
|
- Time/space partitioning, inter-partition communication (sampling/queuing ports)
|
|
- Standard requires: deterministic scheduling, temporal isolation, error containment
|
|
|
|
10. **Derrick, J. et al. "Formal Verification of ARINC 653 Scheduling." FMICS, 2015.**
|
|
- Formal model of ARINC 653 time partitioning
|
|
- Properties: temporal isolation, budget enforcement, deadline compliance
|
|
- Relevance: Correctness proof template for our time partitioning implementation
|
|
|
|
11. **Müller, R. et al. "A Real-Time Capable Multi-Core Virtualization Layer." ISORC, 2012.**
|
|
- ARINC 653 time partitioning on multi-core with jitter analysis
|
|
- Tick-synchronized window switching pattern
|
|
|
|
12. **Singhoff, F. et al. "Scheduling and Memory Requirements Analysis with AADL." Ada-Europe, 2006.**
|
|
- ARINC 653 scheduling analysis, WCET estimation
|
|
- Relevance: How to validate time partition budgets
|
|
|
|
---
|
|
|
|
## 4. Safety Certification
|
|
|
|
13. **RTCA. "DO-178C: Software Considerations in Airborne Systems." RTCA/EUROCAE, 2011.**
|
|
- Software assurance levels DAL A-E
|
|
- Level A requires: 100% MC/DC coverage, traceability, verification independence
|
|
- PikeOS is certified to DAL A — UniversalisOS must target the same
|
|
|
|
14. **ISO. "ISO 26262: Road Vehicles — Functional Safety." ISO, 2018.**
|
|
- ASIL A-D safety integrity levels
|
|
- ASIL D requires formal verification or exhaustive testing
|
|
- Relevance: Automotive target for UniversalisOS (IoT/set-top box)
|
|
|
|
15. **IEC. "IEC 61508: Functional Safety of Electrical/Electronic Systems." IEC, 2010.**
|
|
- Generic safety standard for embedded systems
|
|
- SIL 4 requires: formal methods, MC/DC, independent verification
|
|
|
|
16. **Rushby, J. "Design and Verification of Secure Systems." SOSP, 1981.**
|
|
- Foundational paper on separation kernels and information flow
|
|
- Noninterference between partitions as core safety property
|
|
- Relevance: Theoretical foundation for PikeOS partitioning model
|
|
|
|
---
|
|
|
|
## 5. Futex & Synchronization
|
|
|
|
17. **Hohmuth, M. et al. "Pragmatic Nonblocking Synchronization for Real-Time Systems." USENIX ATC, 2004.**
|
|
- Futex-like primitives for real-time kernels
|
|
- ULOCK_WAIT/WAKE pattern (what PikeOS implements)
|
|
- Relevance: How to build all POSIX synchronization from futex
|
|
|
|
18. **Gorman, M. "Futexes Are Tricky." Paper, 2011.**
|
|
- Complete analysis of futex semantics, race conditions, priority inversion
|
|
- Relevance: Correctness requirements for our ULOCK implementation
|
|
|
|
19. **Drepper, U. "Futexes in Userspace." Paper, 2011.**
|
|
- How glibc implements pthread_mutex/cond/sem on futex
|
|
- Relevance: Direct reference for our Layer 3 synchronization implementation
|
|
|
|
---
|
|
|
|
## 6. POSIX-on-Microkernel
|
|
|
|
20. **Von Tessin, P. "The Supervisor Shell — A Bridge Between the L4 Microkernel and POSIX Applications." 2005.**
|
|
- How to build a POSIX layer on L4 microkernel
|
|
- Supervisor shell pattern maps to our P4EXT (Layer 2)
|
|
- Relevance: Direct architecture guide for our 3-layer design
|
|
|
|
21. **Leslie, B. et al. "User-Level Device Drivers: Achieved Performance." Journal of Computer Science and Technology, 2005.**
|
|
- User-space device drivers on microkernel
|
|
- Relevance: KDEV provider model for device I/O
|
|
|
|
---
|
|
|
|
## 7. Hypervisor Comparison
|
|
|
|
22. **Kuzmin, R. et al. "Survey on Hypervisor-Based Security Solutions for Embedded Systems." IEEE Access, 2020.**
|
|
- Comparison: PikeOS, QNX, VxWorks, INTEGRITY, seL4
|
|
- PikeOS unique value: 3-layer certification independence
|
|
|
|
23. **Peters, F. et al. "A Comprehensive Analysis of the ARM TrustZone Security Extensions." 2015.**
|
|
- TrustZone as hardware separation mechanism
|
|
- Relevance: ARMv7 target can leverage TrustZone for partition isolation
|
|
|
|
24. **Baumann, R. "The PikeOS Operating System — A Technology for Safety and Security." SAE AeroTech, 2009.**
|
|
- PikeOS technology overview, certification approach, partition model
|
|
|
|
---
|
|
|
|
## 8. Scheduler Design
|
|
|
|
25. **Liu, C.L. & Layland, J.W. "Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment." JACM, 1973.**
|
|
- Rate Monotonic Scheduling (RMS) and Earliest Deadline First (EDF)
|
|
- Relevance: PikeOS supports both — UniversalisOS scheduler must implement both
|
|
|
|
26. **Dertouzos, M.L. "Control Robotics: The Procedural Control of Physical Processes." IFIP Congress, 1974.**
|
|
- Earliest Deadline First optimality proof
|
|
- Relevance: EDF is optimal for uniprocessor real-time scheduling
|
|
|
|
---
|
|
|
|
## 9. Memory Management
|
|
|
|
27. **Waldspurger, C.A. "Memory Resource Management in VMware ESX Server." OSDI, 2002.**
|
|
- Balloon driver, transparent page sharing, content-based page sharing
|
|
- Relevance: Advanced memory management patterns for hypervisors
|
|
|
|
28. **Heiser, G. et al. "The Mungi Single-Address-Space Operating System." 1998.**
|
|
- Single address space OS design
|
|
- Relevance: PikeOS uses flat memory model for partitions
|
|
|
|
---
|
|
|
|
## 10. IPC Design
|
|
|
|
29. **Liedtke, J. "On Micro-Kernel Construction." SOSP, 1995.**
|
|
- IPC performance optimization in L4 microkernel
|
|
- Short IPC: 10μs on 486, direct register transfer
|
|
- Relevance: IPC is the performance bottleneck in microkernels
|
|
|
|
30. **Elphinstone, K. et al. "Evolution of the L4 Microkernel Design." APSys, 2013.**
|
|
- L4 IPC evolution, notification mechanism, synchronous/asynchronous IPC
|
|
- Relevance: PikeOS IPC follows L4 patterns
|
|
|
|
---
|
|
|
|
## Local Documentation Index
|
|
|
|
| File | Content |
|
|
|------|---------|
|
|
| `UNIVERSALISOS_VS_PIKEOS_5.0.md` | Feature-by-feature gap analysis |
|
|
| `PIKEOS_POSIX_AUDIT.md` | Complete POSIX implementation audit (455 lines) |
|
|
| `PIKEOS_3LAYER_REPLICATION_PLAN.md` | Implementation plan (693 lines) |
|
|
| `GAP_ANALYSIS_PIKEOS_PARITY.md` | Subsystem gap matrix with effort estimates |
|
|
| `docs/PIKEOS_PARITY_PROGRAM.md` | Parity program handoff document |
|
|
| `docs/AUDIT_REPORT.md` | Deep audit report |
|
|
| `docs/IMPLEMENTATION_REPORT.md` | 8-phase implementation report |
|
|
| `docs/MEMORY_ALLOCATOR_PLAN.md` | Memory allocator design |
|
|
| `docs/T8-2.3_ISOLATION_AUDIT.md` | Isolation audit |
|