ASELSANMicrokernel
S37 · SOURCE-BOUND GATE EVIDENCE

RPi5 G7c tek EL0/SVC paketi hazırlandı; fiziksel BOOT7C bekliyor

Operations komutu/kapı ailesi → gerçek repository yürütme sözleşmesi Bu sayfa yalnız S37 kapısına aittir; komşu kapıların kaynakları bu kabulün içine katılmaz.

S37Komut / fiziksel sözleşmeOperations id exactsource SHA exact

operation: rpi5-g7c-el0-svc-package-staged

script/Makefile/config · Operations · 2 exact excerpt

sequence-bound=true · implementation-bound=false
01 · Yürütme sözleşmesi

Gerçek script / Makefile / config kaynağı

tam dosyaL1–L232
scripts/verify-rpi5-g7c-layout.sh::verify-rpi5-g7c-layout.sh
#!/bin/sh
set -eu

if [ "$#" -ne 4 ]; then
    echo "usage: $0 <llvm-readobj> <llvm-objdump> <hello-elf> <rpi5-kernel-elf>" >&2
    exit 2
fi

readobj=$1
objdump=$2
hello=$3
kernel=$4

for path in "$readobj" "$objdump" "$hello" "$kernel"; do
    if [ ! -f "$path" ] || [ ! -r "$path" ]; then
        echo "HATA: G7c gate okuyamıyor: $path" >&2
        exit 1
    fi
done

headers=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g7c-headers.XXXXXX")
hello_dis=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g7c-hello.XXXXXX")
kernel_dis=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g7c-kernel.XXXXXX")
first_eret=$(mktemp "${TMPDIR:-/tmp}/aselsanos-g7c-eret.XXXXXX")
trap 'rm -f "$headers" "$hello_dis" "$kernel_dis" "$first_eret"' EXIT HUP INT TERM

"$readobj" --file-headers --program-headers "$hello" > "$headers"
"$objdump" -d --no-show-raw-insn "$hello" > "$hello_dis"
"$objdump" -d --demangle --no-show-raw-insn "$kernel" > "$kernel_dis"

need_header() {
    if ! grep -Fq "$1" "$headers"; then
        echo "HATA: trusted hello ELF alanı eksik: $1" >&2
        exit 1
    fi
}

need_header "Format: elf64-littleaarch64"
need_header "Arch: aarch64"
need_header "Type: Executable (0x2)"
need_header "Machine: EM_AARCH64 (0xB7)"
need_header "Entry: 0x44000000"
need_header "ProgramHeaderOffset: 0x40"
need_header "HeaderSize: 64"
need_header "ProgramHeaderEntrySize: 56"
need_header "ProgramHeaderCount: 3"
need_header "Offset: 0x10000"
need_header "VirtualAddress: 0x44000000"
need_header "PhysicalAddress: 0x44000000"
need_header "FileSize: 40"
need_header "MemSize: 40"
need_header "Flags [ (0x5)"
need_header "Offset: 0x11000"
need_header "VirtualAddress: 0x44001000"
need_header "PhysicalAddress: 0x44001000"
need_header "FileSize: 37"
need_header "MemSize: 37"
need_header "Flags [ (0x4)"
need_header "Type: PT_GNU_STACK (0x6474E551)"

load_count=$(grep -Fc "Type: PT_LOAD (0x1)" "$headers")
stack_count=$(grep -Fc "Type: PT_GNU_STACK (0x6474E551)" "$headers")
if [ "$load_count" -ne 2 ] || [ "$stack_count" -ne 1 ]; then
    echo "HATA: hello ELF yalnız 2 PT_LOAD + 1 PT_GNU_STACK taşımalı" >&2
    exit 1
fi

text_sha=$(dd if="$hello" bs=1 skip=65536 count=40 2>/dev/null | shasum -a 256 | awk '{print $1}')
rodata_sha=$(dd if="$hello" bs=1 skip=69632 count=37 2>/dev/null | shasum -a 256 | awk '{print $1}')
expected_text_sha=7f068bdf9276e17a57bc714520a54ab147c9429ec01d327b36922cf44b81a270
expected_rodata_sha=10aec301f6f286c07bef81baa92c5aadf43ae44c1b84351f42b71f595aa5d4b1
if [ "$text_sha" != "$expected_text_sha" ]; then
    echo "HATA: trusted hello .text SHA256 değişti: $text_sha" >&2
    exit 1
fi
if [ "$rodata_sha" != "$expected_rodata_sha" ]; then
    echo "HATA: trusted hello .rodata SHA256 değişti: $rodata_sha" >&2
    exit 1
fi

for contract in \
    '44000014:.*svc[[:space:]]+#0' \
    '44000020:.*svc[[:space:]]+#0' \
    '44000024:.*brk[[:space:]]+#0'; do
    if ! grep -Eq "$contract" "$hello_dis"; then
        echo "HATA: trusted hello disassembly sözleşmesi eksik: $contract" >&2
        exit 1
    fi
done
svc_count=$(grep -Ec '[[:space:]]svc[[:space:]]+#0([[:space:]]|$)' "$hello_dis")
if [ "$svc_count" -ne 2 ]; then
    echo "HATA: trusted hello tam iki SVC #0 taşımalı: $svc_count" >&2
    exit 1
fi

awk '
    /<rpi5_g7c_first_eret>:/ { capture = 1; next }
    capture && /^[[:space:]]*$/ { exit }
    capture { print }
' "$kernel_dis" > "$first_eret"

instruction_count=$(awk '/^[[:space:]]*[[:xdigit:]]+:/ { count++ } END { print count + 0 }' "$first_eret")
if [ "$instruction_count" -ne 44 ]; then
    echo "HATA: first ERET trampoline exact 44 instruction olmalı: $instruction_count" >&2
    cat "$first_eret" >&2
    exit 1
fi

# Presence checks alone cannot prove that ELR/SPSR are programmed only after
# interrupts are masked or that every privileged register is scrubbed before
# entering EL0.  Normalize llvm-objdump's whitespace, then compare the whole
# trampoline instruction-for-instruction and in order.
first_eret_sequence=$(awk '
    /^[[:space:]]*[[:xdigit:]]+:/ {
        line = $2
        for (i = 3; i <= NF; i++) line = line " " $i
        print line
    }
' "$first_eret")
expected_first_eret_sequence='msr DAIFSet, #0xf
mrs x2, CPACR_EL1
and x2, x2, #0xffffffffffcfffff
orr x2, x2, #0x100000
msr CPACR_EL1, x2
isb
msr SP_EL0, x1
msr ELR_EL1, x0
mov x2, xzr
msr SPSR_EL1, x2
msr TPIDR_EL0, x2
msr TPIDRRO_EL0, x2
mov x0, xzr
mov x1, xzr
mov x3, xzr
mov x4, xzr
mov x5, xzr
mov x6, xzr
mov x7, xzr
mov x8, xzr
mov x9, xzr
mov x10, xzr
mov x11, xzr
mov x12, xzr
mov x13, xzr
mov x14, xzr
mov x15, xzr
mov x16, xzr
mov x17, xzr
mov x18, xzr
mov x19, xzr
mov x20, xzr
mov x21, xzr
mov x22, xzr
mov x23, xzr
mov x24, xzr
mov x25, xzr
mov x26, xzr
mov x27, xzr
mov x28, xzr
mov x29, xzr
mov x30, xzr
isb
eret'
if [ "$first_eret_sequence" != "$expected_first_eret_sequence" ]; then
    echo "HATA: first ERET sanitization sırası/değeri exact sözleşmeye uymuyor" >&2
    printf '%s\n' "$first_eret_sequence" >&2
    exit 1
fi

for contract in \
    'msr[[:space:]]+DAIFSet, #0xf' \
    'mrs[[:space:]]+x2, CPACR_EL1' \
    'and[[:space:]]+x2, x2, #0xffffffffffcfffff' \
    'orr[[:space:]]+x2, x2, #0x100000' \
    'msr[[:space:]]+CPACR_EL1, x2' \
    'msr[[:space:]]+SP_EL0, x1' \
    'msr[[:space:]]+ELR_EL1, x0' \
    'msr[[:space:]]+SPSR_EL1, x2' \
    'msr[[:space:]]+TPIDR_EL0, x2' \
    'msr[[:space:]]+TPIDRRO_EL0, x2'; do
    if ! grep -Eq "$contract" "$first_eret"; then
        echo "HATA: first ERET sanitization eksik: $contract" >&2
        exit 1
    fi
done

for register in 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30; do
    count=$(grep -Ec "mov[[:space:]]+x${register}, xzr([[:space:]]|$)" "$first_eret")
    if [ "$count" -ne 1 ]; then
        echo "HATA: first ERET x${register} tam bir kez temizlemiyor: $count" >&2
        exit 1
    fi
done

if [ "$(grep -Ec '[[:space:]]eret([[:space:]]|$)' "$first_eret")" -ne 1 ]; then
    echo "HATA: first ERET trampoline tek eret ile bitmeli" >&2
    exit 1
fi
if grep -Eq '[[:space:]](bl|blr|ret|str|stp|ldr|ldp)[[:space:]]' "$first_eret"; then
    echo "HATA: first ERET trampoline çağrı/stack/bellek talimatı içeriyor" >&2
    cat "$first_eret" >&2
    exit 1
fi

for barrier in \
    'dc[[:space:]]+civac' \
    'tlbi[[:space:]]+vmalle1is' \
    'dsb[[:space:]]+ishst' \
    'dsb[[:space:]]+ish' \
    '[[:space:]]isb([[:space:]]|$)'; do
    if ! grep -Eq "$barrier" "$kernel_dis"; then
        echo "HATA: G7c cache/TLB publish talimatı ELF içinde yok: $barrier" >&2
        exit 1
    fi
done

for marker in \
    'ASELSAN/G7C0 CPU=0 MODE=EL0 ROOT=SHARED ASID=0 ELF=TRUSTED PMM_ALLOC=3' \
    'ASELSAN/G7C1 SVC=WRITE ELR=0x' \
    'ASELSAN/G7C2 SVC=EXIT ELR=0x' \
    'ASELSAN/BOOT7C EL0=OK SVC_WRITE=OK SVC_EXIT=OK SWITCH=EL1H TIMER=OK MAPS=OK' \
    'ASELSAN/G7CERR'; do
    if ! strings "$kernel" | grep -Fq "$marker"; then
        echo "HATA: G7c marker ELF içinde yok: $marker" >&2
        exit 1
    fi
done

echo "PASS: G7c trusted ELF, exact SVC ABI, cache/TLB publish ve sanitized first-ERET doğrulandı"
echo "      text_sha256=$text_sha"
echo "      rodata_sha256=$rodata_sha"
snippet sha256: 9e202f289469file sha256: 9e202f289469
02 · Kapı kimlik kaydı

Operations sıra, kimlik ve başlık bağı

tam Operations kaydıL33965–L34079
website/src/lib/operations.ts::rpi5-g7c-el0-svc-package-staged
  {
    id: "rpi5-g7c-el0-svc-package-staged",
    date: "2026-08-20",
    sequence: 37,
    status: "partial",
    title: "RPi5 G7c tek EL0/SVC paketi hazırlandı; fiziksel BOOT7C bekliyor",
    summary:
      "G7b fiziksel BOOT7B sınırı korunarak yalnız board-rpi5 için çalışan dar bir G7c yolu hazırlandı. Exact iki sayfalık trusted hello ELF'i üç yeni PMM frame'ine W^X alias geçişiyle yükleniyor; kernel EL0'dan kapalı kalıyor, first-ERET bütün GPR/TLS durumunu temizliyor, bounded WRITE normal exception dönüşünden geçiyor ve EXIT bütün user/copy eşlemelerini kaldırıp EL1h monitörüne dönüyor. G7c host testleri 16/16, workspace 68/68, üç kart build'i, QEMU runtime smoke, RPi5 makine-kodu/layout kapısı ve paket manifesti geçti. 226448 baytlık 276d568b…a99d0 imaj yalnız build/rpi5 içinde hazırdır; microSD yazımı ve gerçek UART10 G7C0/G7C1/G7C2/BOOT7C kanıtı yapılmadığı için kayıt staged/partial tutulur.",
    evidence: [
      "Trusted hello doğrulayıcısı yalnız exact ELF64/AArch64 executable header'ını, iki PT_LOAD + bir PT_GNU_STACK program header'ını, entry 0x44000000'ı, 40 bayt text'i ve 37 bayt rodata'yı kabul ediyor; text ve rodata mutation/truncation negatif testleri fail-closed geçiyor.",
      "Yükleme sırasında text/rodata/stack frame'leri yalnız EL1 RW/NX alias'lardan yazılıyor ve üçünün de tamamı PoC'ye clean+invalidate ediliyor. Bu alias'lar kaldırılıp DSB/TLBI/DSB/ISB tamamlanmadan final U-RX, U-R/NX ve U-RW/NX eşlemeleri kurulmuyor.",
      "RPi5 kernel text'i KERNEL_TEXT_EL1, rodata'sı KERNEL_RODATA_EL1, data/bss/stack'i KERNEL_DATA exact descriptor'larıyla EL0'a kapalı. Alt ve üst user stack guard VA'ları unmapped; bounded copy-in aperture yalnız EL1 R/NX'tir.",
      "First-ERET makine-kodu kapısı tam 44 talimatı sırayla doğruladı: ELR/SPSR öncesi DAIF maskesi, CPACR_EL1.FPEN=01, SP_EL0/ELR_EL1, EL0t SPSR, TPIDR_EL0/TPIDRRO_EL0 ve x0–x30 temizliği, ardından tek eret.",
      "Exact syscall sözleşmesi WRITE için SVC #0, x8=2, fd=1, ptr=0x44001000, len=37 ve ELR=0x44000018; EXIT için x8=3, status=0 ve ELR=0x44000024'tür. EXIT user text/rodata/stack ve copy aperture'ı kaldırıp normal trap-frame eret ile EL1h monitörüne yönelir.",
      "make verify-rpi5-g7c-host exit 0 verdi: trusted ELF 4/4, exact page flag 4/4 ve strict UART/negatif transcript 8/8; toplam G7c hedef testi 16/16 PASS.",
      "cargo test --workspace toplam 68/68 PASS verdi. make verify-core exit 0 ile QEMU, RPi4 ve RPi5 build'lerini, QEMU runtime smoke'u ve RPi5 image/layout paketini birlikte tamamladı; artefaktsız geçici repo kopyasında aynı hedef sıcak cache olmadan da geçti.",
      "QEMU smoke exact ‘hello ELF + IPC ELF + scheduler SEC 5; fault marker yok’ sonucunu verdi. G7c marker'ları QEMU ve RPi4 ELF'lerinde yok; G7C0/G7C1/G7C2/BOOT7C/G7CERR yalnız RPi5 ELF'inde birer kez bulundu.",
      "scripts/verify-rpi5-g7c-layout.sh trusted hello layout'unu, exact iki SVC konumunu, first-ERET sanitization dizisini ve cache/TLB publish talimatlarını dondurulmuş RPi5 makine kodunda PASS kabul etti.",
      "Yeni aselsanos-rpi5.img 226448 bayt / 276d568b793dc580577f3e3c89e06f428dc56c5d5ec208e10d905043f0ba99d0; hello ELF 70344 bayt / f60b9d4322962780f0eac218f3ffef7221785b54621dcfc11d3fb3590921d230 olarak sabitlendi.",
      "Sabit DTB 78703 bayt / 40a2fbe9c29e8b9a4912cf726a943068defb779fc052ec38e457a79c58abca00 ve config.txt 501 bayt / 1248275cdc6f6ce951ce0ff2183471d194c5b9bb58c3dc3f66efa9156f91d76b kaldı; SHA256SUMS üç payload için 3/3 OK verdi.",
      "Teknik sınır ve fiziksel kabul prosedürü docs/M8.1-RPi5-G7c-EL0-SVC-Staged-Proof.md içinde donduruldu.",
    ],
    commands: [
      "make verify-rpi5-g7c-host",
      "cargo test --workspace",
      "make verify-core",
      "make verify-qemu",
      "make image-rpi5",
      "cd build/rpi5 && shasum -a 256 -c SHA256SUMS",
      "shasum -a 256 hello ELF + RPi5 ELF + image + DTB + config + manifest",
      "RPi5/QEMU/RPi4 ELF G7c marker isolation audit",
    ],
    terminalSessionsNote:
      "Bu kayıttaki oturumlar 20 Ağustos 2026'da dondurulmuş G7c kaynağı üzerinde yeniden çalıştırıldı. Uzun, tekrarlayan mevcut compiler warning'leri seçili çıktıda kısaltılmıştır; bütün gösterilen komutlar exit 0 verdi.",
    terminalSessions: [
      {
        id: "g7c-host-tests",
        title: "G7c trusted ELF · page flags · strict UART",
        commandLines: ["make verify-rpi5-g7c-host"],
        outputLines: [
          "Running tests/rpi5_g7c_elf.rs",
          "test result: ok. 4 passed; 0 failed",
          "Running tests/rpi5_g7c_page_flags.rs",
          "test result: ok. 4 passed; 0 failed",
          "Running tests/rpi5_g7c_uart.rs",
          "test result: ok. 8 passed; 0 failed",
        ],
        exitCode: 0,
        outputMode: "selected",
        outputNote: "Üç G7c hedef test binary'sinin sonuç satırları seçildi.",
      },
      {
        id: "g7c-core-matrix",
        title: "Workspace · üç board · QEMU runtime",
        commandLines: ["make verify-core"],
        outputLines: [
          "cargo test --workspace: 68 passed; 0 failed",
          "QEMU kernel build: PASS",
          "QEMU smoke PASS: hello ELF + IPC ELF + scheduler SEC 5; fault marker yok",
          "Raspberry Pi 4 kernel build: PASS",
          "Raspberry Pi 5 kernel build: PASS",
          "RPi5 image/layout package: PASS",
        ],
        exitCode: 0,
        outputMode: "selected",
        outputNote:
          "Uzun build warning dökümü yerine matrisin sonuçları seçildi; warning'ler hata olarak saklanmadı veya gizlenmedi.",
      },
      {
        id: "g7c-machine-code-package",
        title: "RPi5 machine-code kapısı ve paket",
        commandLines: ["make image-rpi5"],
        outputLines: [
          "PASS: RPi5 PMM publish SCTLR_EL1 + ISB sonrasında; _start_rust pre-MMU gövdesinde exclusive atomik yok",
          "PASS: G7c trusted ELF, exact SVC ABI, cache/TLB publish ve sanitized first-ERET doğrulandı",
          "text_sha256=7f068bdf9276e17a57bc714520a54ab147c9429ec01d327b36922cf44b81a270",
          "rodata_sha256=10aec301f6f286c07bef81baa92c5aadf43ae44c1b84351f42b71f595aa5d4b1",
          "aselsanos-rpi5.img: OK",
          "bcm2712-rpi-5-b.dtb: OK",
          "config.txt: OK",
          "276d568b793dc580577f3e3c89e06f428dc56c5d5ec208e10d905043f0ba99d0  aselsanos-rpi5.img",
        ],
        exitCode: 0,
        outputMode: "selected",
        outputNote:
          "Makine-kodu/layout ve 3/3 manifest kabul satırları seçildi.",
      },
      {
        id: "g7c-artifact-hashes",
        title: "G7c dondurulmuş artefakt hash'leri",
        commandLines: [
          "shasum -a 256 userspace/hello/.../hello target/rpi5/.../aselsan_kernel build/rpi5/*",
        ],
        outputLines: [
          "f60b9d4322962780f0eac218f3ffef7221785b54621dcfc11d3fb3590921d230  hello",
          "a7fa1257cfc94c0fd1b4106665bb0d065767a1aa8f9d933aba023eb65d88a8b8  aselsan_kernel",
          "276d568b793dc580577f3e3c89e06f428dc56c5d5ec208e10d905043f0ba99d0  aselsanos-rpi5.img",
          "40a2fbe9c29e8b9a4912cf726a943068defb779fc052ec38e457a79c58abca00  bcm2712-rpi-5-b.dtb",
          "1248275cdc6f6ce951ce0ff2183471d194c5b9bb58c3dc3f66efa9156f91d76b  config.txt",
          "eb267fc450a8b14105867935d2b2a07a78af7b78170a4bf9dcf5a4d4c2184acc  SHA256SUMS",
        ],
        exitCode: 0,
        outputMode: "complete",
      },
    ],
    limitations: [
      "276d568b…a99d0 G7c paketi yalnız build/rpi5 içinde hazırdır; fiziksel microSD'ye yazılmadı. Kartta gerçek BOOT7B PASS veren c065bbd7…db5f G7b paketi bulunur.",
      "G7C0, payload, G7C1, G7C2 ve BOOT7C henüz gerçek Raspberry Pi 5 UART10 kaydında gözlenmedi; G7c fiziksel PASS değildir. Fixture'daki frame ve tick değerleri yalnız sentetik validator girdisidir.",
      "Bu yol yalnız CPU0, shared root/ASID0, sabit iki sayfalık trusted ELF ve exact WRITE/EXIT ABI smoke'udur; genel ELF yükleme, ayrı address-space/ASID izolasyonu, çoklu user task veya scheduler userspace entegrasyonu değildir.",
      "Üç G7c PMM frame'i monotonic smoke sonunda free/reuse edilmez. Stack kullanımı/overflow, demand paging, COW, allocator lifecycle, preemption, SMP, uzun soak ve farklı güç/sıcaklık koşulları kanıtlanmaz.",
      "Host validator UART'taki DTB page-cover, heap ve guard aralıklarını bağımsız dışlar; ayrıntıları loglanmayan kernel, reserved-memory ve CMA aralıkları kernel-side PMM self-check sınırındadır.",
      "QEMU yalnız regression ve cfg izolasyonudur. ELF string presence ve sentetik fixture gerçek RPi5 execution/UART kanıtının yerini tutmaz.",
      "G7d timer-preemptive scheduling ve G8 PSCI/SMP ayrı kapılardır.",
    ],
  },
snippet sha256: 95003a2b066efile sha256: 9726dbf00f84
Kayıtlı yürütme/kanıt komutu
make verify-rpi5-g7c-host
Registry schema v5 · generator website/scripts/generate-code-gates.mjs · Tam SHA-256: 91d38c7b6222f0b4c117be786454853543da55a160e543d9b951057cc20dcc06