portugalfuturista/universalisos
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
universalisos/BIBLIOGRAPHY_SAFETY_CRITICAL_HYPERVISOR.md
Fábio Coutada 059f96c948 docs: add safety-critical evaluation and implementation plans 
- 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
2026-07-15 15:32:05 +01:00

8.2 KiB
Raw Blame History

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

  1. 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

  2. Heiser, G. "The seL4 Microkernel — An Introduction." Technical Report, 2020.

    • seL4 capability system, IPC mechanism, scheduling
    • Relevance: Capability-based access control applicable to UniversalisOS

  3. 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

  4. 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

  1. 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

  2. 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

  3. 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

  4. 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

  1. 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

  2. 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)

  3. 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

  4. 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

  1. 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

  2. Gorman, M. "Futexes Are Tricky." Paper, 2011.

    • Complete analysis of futex semantics, race conditions, priority inversion
    • Relevance: Correctness requirements for our ULOCK implementation

  3. 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

  1. 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

  2. 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

  1. 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

  2. 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

  3. 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

  1. 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

  2. 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

  1. 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

  2. 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

  1. 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

  2. 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