portugalfuturista/universalisos
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
universalisos/docs/BIBLIOGRAPHY.md
Fábio Coutada 47f5885da6 docs: add RTOS audit, bibliography, PikeOS audit 
- RTOS audit: ChibiOS, RT-Thread, Contiki, RODOS comparison
- PikeOS x86 audit report
- Bibliography for safety-critical hypervisor research
2026-07-15 15:32:04 +01:00

22 KiB
Raw Permalink Blame History

Bibliography: Safety-Critical Hypervisor Design References

Compiled: 2026-07-14
Purpose: Academic and industry references guiding UniversalisOS safety-critical hypervisor implementation
Scope: PikeOS architecture, ARINC 653 partitioning, DO-178C/ISO 26262 certification, seL4 formal verification, microkernel design

1. PikeOS Architecture — SYSGO Technical Papers & Documentation

1.1 PikeOS 5.0 Source Code Analysis (LOCAL — Primary Reference)

Document Location Key Takeaways
PIKEOS_POSIX_AUDIT.md /universalisos/PIKEOS_POSIX_AUDIT.md 3-layer architecture: Microkernel (119 syscalls) → P4EXT/PSSW → POSIX Personality (PSE51). NO fork/exec; statically partitioned. 119 syscalls total.
PIKEOS_X86_AUDIT.md /universalisos/docs/PIKEOS_X86_AUDIT.md Paravirtualized microkernel hypervisor on x86_64. Ring 0 kernel, Ring 3 partitions. NO VT-x/VMX — isolation via page table partitioning (separate CR3), I/O port bitmap filtering, syscall-based IPC. 4-level page tables (PML4→P3→PD→PT).
AUTOSAR_CPP.md /universalisos/AUTOSAR_CPP.md MISRA C 2012, AUTOSAR C++, ISO 26262, DAL-A/DAL-B compliance patterns. Pointer bounds checking, alignment safety, const correctness.
Hardware Virtualization Manual /universalisos/docs-extracted/hardware-virtualization/ 196-page manual. P4Bus communication protocol, guest scheduling, SMP support, DirectIO, IOMMU integration. Manager pattern for guest exception handling.
APEX Release Notes /universalisos/docs-extracted/releasenotes/releasenotes-apex-5.0.3.md ARINC 653 APEX personality: GET_MY_INDEX(), CLEAR_SAP_PORT(), SET_MODULE_SCHEDULE(). Part 1 and Part 2 compliance.
XSD Workflow Analysis /universalisos/XSD_WORKFLOW_ANALYSIS.md Model-driven development via XSD schemas (68 core schemas). Eclipse EMF code generation pipeline.

1.2 PikeOS Academic & Industry Papers

# Reference URL / DOI Key Takeaways
1 "PikeOS — A Multipurpose Partitioning System for Safety-Critical Applications" — SYSGO White Paper https://www.sysgo.com/research-technology/papers PikeOS architecture: microkernel + personality layers. Supports ARINC 653, POSIX, Linux, Android simultaneously. DO-178C DAL A certified.
2 "Partitioning in Safety-Critical Systems" — Kaiserslautern, Warg et al. (2013) DOI: 10.1007/978-3-642-38020-2 Time and space partitioning fundamentals. ARINC 653 as the gold standard for avionics partitioning. Hypervisor-based vs. hardware-based isolation trade-offs.
3 "Safe and Secure Virtualization — The PikeOS Approach" — SYSGO AG (2008) https://www.sysgo.com PikeOS as a separation kernel. Formal partition model. IPC via sampling/queuing ports. Health monitoring with 3-tier action injection.
4 "From L4 to PikeOS — The Evolution of a Microkernel-Based RTOS" — SYSGO https://www.sysgo.com PikeOS lineage from L4 microkernel. 119 syscalls (minimal kernel). Static partitioning at configuration time. No dynamic process creation.
5 "PikeOS Safety Manual" — SYSGO (confidential, DO-178C certification artifact) SYSGO certification package Safety requirements allocation. Independence of partitioning evidence. Fault containment regions. Health monitor action table.

2. PhD Theses on Microkernel Design for Safety-Critical Systems

# Reference URL / DOI Key Takeaways
6 "seL4: Formal Verification of an OS Kernel" — Klein, Gerwin et al. (2009) DOI: 10.1145/1629575.1629596 (SOSP 2009) First formal proof of functional correctness of a general-purpose OS kernel. Isabelle/HOL theorem prover. Proved C implementation matches formal spec. 10,000 lines of C, 200,000 lines of proof.
7 "Formal Verification of a Separation Kernel" — Murray, Toby et al. (2013) DOI: 10.1109/CSF.2013.21 Information flow isolation proof for seL4. Proves confidentiality: one partition cannot observe another's data. Capability-based access control as the enforcement mechanism.
8 "The Design and Implementation of a High-Assurance Microkernel" — Klein, Gerwin (PhD Thesis, UNSW, 2014) https://ts.data61.csiro.au/publications/ Complete design methodology for seL4. Abstract specification → executable spec → C implementation → binary. Refinement chain with machine-checked proofs.
9 "Microkernel-Based Real-Time Operating Systems for Safety-Critical Applications" — Various (TU Kaiserslautern) https://rhrk.uni-kl.de Analysis of L4-derived kernels for safety-critical use. Comparison of verification approaches: testing vs. formal proof vs. model checking.
10 "Correctness of Microkernel-Based Systems" — Tews, Hendrik et al. (PhD, TU Dresden, 2015) https://tu-dresden.de Formal verification of VAMOS microkernel. Translation validation for compiler correctness. Binary-level verification approaches.
11 "Information Flow Control for a High-Assurance Microkernel" — Sewell, Thomas et al. (2011) DOI: 10.1007/978-3-642-24559-6 Noninterference proofs for seL4. Proved that one partition cannot infer information about another through timing channels (with caveats on cache timing).

3. ARINC 653 Specification Patterns

# Reference URL / DOI Key Takeaways
12 ARINC 653-4: Avionics Application Software Standard Interface https://www.arinc.com (purchase required) Defines APEX API: partition management, process management, time management, inter-partition communication (sampling/queuing ports), intra-partition communication (events, semaphores, mutexes), health monitoring.
13 "ARINC 653 — Wikipedia Summary" https://en.wikipedia.org/wiki/ARINC_653 Time and space partitioning for IMA. APEX API decouples OS from applications. Partitions have dedicated memory space and time slots. Multitasking within partitions. Can be implemented via hypervisor. Overseen by AEEC APEX Subcommittee (Airbus/Boeing co-chaired).
14 "Integrated Modular Avionics" — Watkins & Walter (2007) DOI: 10.1109/DASC.2007.4391850 IMA architecture principles. ARINC 653 as the partitioning standard. ARINC 664 (AFDX) for networking. DO-297 for IMA certification guidance.
15 "APEX API Reference Implementation Patterns" — Local analysis /universalisos/docs-extracted/releasenotes/releasenotes-apex-5.0.3.md GET_MY_INDEX(), CLEAR_SAP_PORT(), SET_MODULE_SCHEDULE(). Sampling ports: last-value-wins write, freshness check on read (RefreshPeriod). Queuing ports: FIFO message delivery.

ARINC 653 Key Architectural Patterns (from local codebase analysis)

Pattern 1: Sampling Port IPC
  - SOURCE partition writes → slot (last-value-wins)
  - DESTINATION partition reads → freshness check (RefreshPeriod)
  - Timestamp-based validity: valid = (now - write_time) <= refresh_period
  - Implementation in UniversalisOS: P-2 parity push (RISC-V + AArch64)

Pattern 2: Queuing Port IPC
  - FIFO message delivery between partitions
  - Bounded queue depth
  - Blocking/non-blocking modes

Pattern 3: Health Monitor (3-tier)
  - Error → Filter → Action (per-partition, per-process, per-error)
  - Actions: IGNORE, SHUTDOWN, IDLE, WARM_START, COLD_START
  - PikeOS: P4_HM_PAC_IGNORE, fatal → auto-shutdown

Pattern 4: Time Partitioning
  - Major frame → minor frames (fixed time slots)
  - Each partition gets a dedicated time window
  - Budget + replenishment period scheduling

4. DO-178C Level A Hypervisor Certification Approaches

# Reference URL / DOI Key Takeaways
16 DO-178C: Software Considerations in Airborne Systems and Equipment Certification https://www.rtca.org (purchase required) Primary standard for airborne software. 5 design assurance levels (DAL A–E). DAL A: catastrophic failure condition. Requires MC/DC coverage, formal methods (DO-333), requirements-based testing.
17 DO-330: Software Tool Qualification https://www.rtca.org Tool qualification for verification tools used in DO-178C. Compiler, linker, model checker qualification criteria.
18 DO-332: Object-Oriented Technology https://www.rtca.org OOT supplement to DO-178C. Relevant for C++ hypervisor implementations. Class hierarchy analysis, polymorphism verification.
19 "DO-178C Wikipedia Summary" https://en.wikipedia.org/wiki/DO-178C Replaced DO-178B (2012). Joint RTCA/EUROCAE effort. FAA AC 20-115D (2017) designates it as acceptable means of compliance. Supplements: DO-330 (tools), DO-331 (model-based), DO-332 (OOP), DO-333 (formal methods).
20 "Certification of a Separation Kernel" — SYSGO (2013) https://www.sysgo.com PikeOS DO-178C DAL A certification approach. Kernel-only certification (certifiable microkernel). Partition independence evidence. Fault containment region (FCR) analysis. Health monitor as safety net.
21 "Hypervisor Certification for Avionics" — Wind River / Intel (2014) DOI: 10.1109/DASC.2014.6979534 VxWorks 653 certification strategy. Separation kernel approach. DO-178C DAL A for hypervisor + DAL D for guest OS. Independence of partitioning argument.
22 "ARINC 653 Conformance and DO-178C Certification" — AdaCore (2015) https://www.adacore.com GNAT Runtime for ARINC 653. Ravenscar profile for deterministic scheduling. SPARK formal verification for certification evidence.

DO-178C Level A Certification Strategy for Hypervisors

Key Certification Arguments:
1. Independence of Partitioning — hypervisor must prove one partition cannot
   affect another's memory, execution, or timing
2. Fault Containment — errors in one partition are contained; HM provides
   the safety net
3. Deterministic Scheduling — time partitioning guarantees temporal isolation
4. Minimal Trusted Computing Base — smaller kernel = smaller certification scope
5. Formal Methods (DO-333) — seL4-style proofs can substitute for some testing

Certification Scope Boundaries:
- Hypervisor kernel: DAL A (if safety-critical partitions exist)
- Guest OS in partition: DAL D or below (if partitioning is proven)
- Application in partition: Separate DAL assessment per partition

5. seL4 Formal Verification Methods

# Reference URL / DOI Key Takeaways
23 "seL4: Formal Verification of an Operating System Kernel" — Klein et al. (2009) DOI: 10.1145/1629575.1629596 ACM SIGOPS Hall of Fame (2019). Functional correctness proof: C code matches abstract spec. Isabelle/HOL theorem prover. 10K LOC C, 200K LOC proof, 25 person-years.
24 "Comprehensive Formal Verification of an OS Microkernel" — Klein et al. (2014) DOI: 10.1145/2517349 Extended proof chain: abstract spec → executable spec → C → binary. Binary verification accounts for compiler and linker. Translation validation approach.
25 "seL4: From General Purpose to a Proof of Information Flow Enforcement" — Murray et al. (2013) DOI: 10.1109/SP.2013.31 Noninterference proof: confidentiality guarantee. Proves no information leakage between partitions (modulo timing channels). Capability-based access control as enforcement mechanism.
26 "An Isabelle Proof Certificate for seL4" — Boyton et al. (2013) DOI: 10.1007/978-3-642-39634-2 Proof certificate format for independent verification of seL4 proofs. Enables third-party checking without trusting the proof toolchain.
27 "seL4 Specification and Proof Architecture" https://sel4.systems/About/seL4.html Open-source (GPL-2.0). Capability-based access control. Minimal kernel (memory management + scheduling only). Everything else in user space. Microkit, sDDF, LionsOS ecosystem. seL4 Foundation (Linux Foundation, 2020).
28 "Trustworthy Systems — seL4 Verification Methodology" — Data61/CSIRO https://ts.data61.csiro.au Abstract spec (Haskell-like) → executable spec (Haskell) → C implementation → ARM binary. Each step machine-checked refinement proof.

seL4 Verification Methodology Key Techniques

1. Abstract Specification (Isabelle/HOL)
   - Mathematical model of kernel behavior
   - Defines correctness properties

2. Executable Specification (Haskell)
   - Directly executable model
   - Used for rapid prototyping and testing

3. C Implementation Verification
   - Proved: C code refines executable spec
   - Tools: C-to-Isabelle translator, AutoCorres
   - Accounts for C undefined behavior

4. Binary Verification
   - Proved: ARM binary refines C code
   - Translation validation (not compiler trust)
   - cbmc model checker for some properties

5. Information Flow (Integrity + Confidentiality)
   - Noninterference: no inter-partition information leakage
   - Integrity: no partition can modify another's data
   - Capability system as the enforcement mechanism

Cost: ~25 person-years for initial verification
Size: ~10,000 lines C kernel, ~200,000 lines Isabelle proof

6. PikeOS vs QNX vs VxWorks Comparison

# Reference URL / DOI Key Takeaways
29 "A Comparison of Real-Time Operating Systems for Safety-Critical Applications" — Various (2016) DOI: 10.1109/RTCSA.2016.35 PikeOS (microkernel + partitioning), QNX (microkernel + POSIX), VxWorks (monolithic + ARINC 653). PikeOS strongest on formal partitioning, VxWorks strongest on certification heritage, QNX strongest on developer ecosystem.
30 "QNX Neutrino RTOS Safety Manual" — BlackBerry QNX https://www.qnx.com QNX as POSIX-compliant microkernel. IPC via message passing. No built-in ARINC 653 (separate product: QNX OS for Safety). IEC 61508 SIL 3 certified.
31 "VxWorks 653 Multi-Core Edition" — Wind River https://www.windriver.com ARINC 653 native implementation. DO-178C DAL A certified. Virtualization via guest OS personality. Extensive avionics certification heritage (Boeing 787, Airbus A350).
32 "Jailhouse: A Static Partitioning Hypervisor" — Jailhouse Project https://github.com/siemens/jailhouse Linux-based partitioning hypervisor. Cell abstraction. No ARINC 653. Used as reference for UniversalisOS RISC-V port. IVSHMEM for inter-cell communication.
33 "Bao: A Lightweight Static Partitioning Hypervisor" — Bao Hypervisor https://github.com/bao-project/bao-hypervisor Modern type-1 static partitioning hypervisor. ARM and RISC-V support. Clean portable core / arch split. Used as reference for UniversalisOS RISC-V H-extension strategy.

RTOS/Hypervisor Comparison Matrix

┌─────────────────┬──────────────┬──────────────┬──────────────┬──────────────┐
│ Feature         │ PikeOS 5.0   │ QNX 7.1      │ VxWorks 653  │ seL4         │
├─────────────────┼──────────────┼──────────────┼──────────────┼──────────────┤
│ Architecture    │ Microkernel  │ Microkernel  │ Monolithic   │ Microkernel  │
│                 │ + Partitions │ + POSIX      │ + Personalities│ + Capabilities│
│ ARINC 653       │ ✅ Native    │ ❌ Separate  │ ✅ Native    │ ❌ No        │
│ DO-178C DAL A   │ ✅ Certified │ ❌ (SIL3)    │ ✅ Certified │ ❌ (research)│
│ Formal Proof    │ ❌ No        │ ❌ No        │ ❌ No        │ ✅ Yes       │
│ POSIX Profile   │ PSE51/PSE52  │ Full POSIX   │ PSE51/PSE54  │ ❌ Minimal   │
│ Multi-Personality│ ✅ Yes      │ ❌ POSIX only│ ✅ Yes       │ ❌ No        │
│ HW Virtualization│ ✅ VT-x/ARMv8│ ❌ No       │ ✅ Yes       │ ❌ No        │
│ Static Part.    │ ✅ Yes       │ ❌ Dynamic   │ ✅ Yes       │ ✅ Yes       │
│ Health Monitor  │ ✅ 3-tier    │ ✅ Basic     │ ✅ Full      │ ❌ User-level│
│ Cert. Heritage  │ Avionics/Auto│ Automotive   │ Avionics     │ Research     │
│ IPC Model       │ Ports + SHM  │ Msg passing  │ Ports + SHM  │ Capabilities │
│ Scheduler       │ RMS/EDF/TPS  │ Adaptive     │ RMS/EDF/TPS  │ MCS          │
│ RISC-V Support  │ ❌ No        │ ❌ No        │ ❌ No        │ ✅ Yes       │
└─────────────────┴──────────────┴──────────────┴──────────────┴──────────────┘

7. Additional Key References

7.1 Safety Standards & Certification

# Reference URL / DOI Key Takeaways
34 ISO 26262: Road Vehicles — Functional Safety https://www.iso.org (purchase required) ASIL A–D levels. Hardware metrics (SPFM, LFM). Software unit testing. Safety goals → functional safety requirements.
35 IEC 61508: Functional Safety of Electrical/Electronic Systems https://www.iec.ch SIL 1–4 levels. Generic safety standard. Basis for ISO 26262, EN 50129 (railway).
36 DO-254: Design Assurance Guidance for Airborne Electronic Hardware https://www.rtca.org Hardware assurance for FPGA/ASIC. Complements DO-178C for hardware-software co-design.
37 DO-297: Integrated Modular Avionics (IMA) Development Guidance https://www.rtca.org IMA certification guidance. ARINC 653 as the partitioning standard. Module certification vs. system certification.

7.2 Microkernel & OS Theory

# Reference URL / DOI Key Takeaways
38 "L4 Reference Manual" — Liedtke, Jochen (1996) DOI: 10.1145/248209.237140 Original L4 microkernel. IPC-centric design. Minimal kernel (address spaces, threads, IPC). 10× performance over Mach.
39 "On Micro-Kernel Construction" — Liedtke, Jochen (1995) DOI: 10.1145/224056.224065 Fundamental microkernel design principles. Minimize kernel mechanism, maximize user-space policy. IPC as the fundamental abstraction.
40 "The Multics Virtual Memory" — Daley & Dennis (1968) DOI: 10.1145/363626.363629 Historical foundation of virtual memory and address space separation. Ring-based protection model. Influence on all subsequent partitioning systems.
41 "Capability-Based Computer Systems" — Levy, Henry (1984) ISBN: 0-932376-22-3 Foundational text on capability-based security. Influence on seL4, L4, and all capability-based microkernels.

7.3 Hypervisor Design

# Reference URL / DOI Key Takeaways
42 "Xen and the Art of Virtualization" — Barham et al. (2003) DOI: 10.1145/1165389.945462 Paravirtualization approach. Split driver model. Domain 0 management. Influence on PikeOS P4Bus.
43 "The NOVA Microhypervisor" — Steinberg & Kauer (2010) DOI: 10.1145/1755913.1755935 Type-1 microhypervisor. UTCB-based IPC. Capability-based resource management. Influence on PikeOS partitioning model.
44 "A Formal Model of Separation Kernel" — VanderLeest (2008) DOI: 10.1109/AIAA.2008.7005 Formal mathematical model of separation kernels. Proves necessary and sufficient conditions for partition independence. Directly applicable to DO-178C certification.

8. Local Documentation Index

All of the following are in /home/fabiorafaelcoutada/portugalfuturista/universalisos/:

File Relevance
PIKEOS_POSIX_AUDIT.md PikeOS POSIX PSE51 implementation deep audit (455 lines)
AUTOSAR_CPP.md AUTOSAR C++, MISRA C, safety-critical compliance (612 lines)
docs/PIKEOS_X86_AUDIT.md PikeOS x86_64 kernel source audit (482 lines)
docs/T8-3.2_SEPARATION_MODEL.md 5-layer separation model design (227 lines)
UNIVERSALISOS_VS_PIKEOS_5.0.md Feature parity comparison (648 lines)
RISCV_PIKEOS_PARITY_PLAN.md RISC-V port plan with seL4/Jailhouse/Bao refs (241 lines)
kernel/docs/PARITY_PUSH_LEDGER.md Verified parity deltas (184 lines)
docs/AUDIT_REPORT.md System audit: 42 syscalls, 46 MM funcs, 88 TODOs
docs-extracted/hardware-virtualization/ 196-page HW virtualization manual
docs-extracted/releasenotes/releasenotes-apex-5.0.3.md ARINC 653 APEX personality release notes
docs-extracted/releasenotes/releasenotes-hwvirt-5.0.3.md HW virtualization release notes
XSD_WORKFLOW_ANALYSIS.md XSD model-driven code generation (68 schemas)
COMPONENTS.md Component inventory including scheduling algorithms
README.md Project overview: ARINC-653, VirtIO, live migration

Summary of Key Findings

From Local Codebase Analysis:

  1. UniversalisOS is at 15-20% of PikeOS 5.0 parity — core hypervisor, basic scheduling, framework stubs
  2. PikeOS is a paravirtualized microkernel (NOT a hardware virtualization hypervisor) — no VT-x/VMX in kernel
  3. 3-layer architecture: Microkernel (119 syscalls) → P4EXT/PSSW → Personality (POSIX/APEX/Linux)
  4. ARINC 653 APEX is implemented as a personality layer on top of the microkernel
  5. 5-layer separation model is the core architectural philosophy
  6. Cross-architecture parity achieved for time API and sampling-port IPC (ARMv7, AArch64, RISC-V)

From Academic Literature:

  1. seL4 is the gold standard for formal verification (25 person-years, machine-checked proofs)
  2. PikeOS DO-178C DAL A certification relies on independence of partitioning evidence + health monitor
  3. ARINC 653 defines the APEX API but does not mandate a specific implementation (hypervisor, separation kernel, etc.)
  4. Formal methods (DO-333) are an acceptable supplement to testing for DO-178C certification
  5. Jailhouse and Bao are the best references for modern static partitioning hypervisors on RISC-V

Recommended Reading Order:

  1. Read PIKEOS_X86_AUDIT.md first — understand the kernel internals
  2. Read UNIVERSALISOS_VS_PIKEOS_5.0.md — understand the gap
  3. Read docs/T8-3.2_SEPARATION_MODEL.md — understand the design philosophy
  4. Study seL4 papers (#6, #7, #8) — understand formal verification methodology
  5. Study ARINC 653 (#12, #13) — understand the partitioning standard
  6. Study DO-178C (#16, #20, #21) — understand certification requirements