S564 · R1 güncelleme: paket manifesti ve hash zinciri modeli
S564 kaynak/host model kapısı PASS'tir: güncelleme paketi manifesti (path ≤ 64 bayt, bayt sayısı, 32 baytlık SHA-256 özeti, Kernel/Dtb/Config/App rolleri), manifest başlığı (monoton sürüm, öncül manifest hash'i, ≤ 16 giriş), deterministik kanonik kodlama, öncül→ardıl hash zinciri doğrulaması ve gözlenen paketin head manifeste bayt-bayt exact eşleşmesi saf Rust modeli olarak eklendi; SHA-256 modülün içinde saf ve streaming olarak implemente edildi ve "" ile "abc" bilinen vektörlerine sabitlendi. S545 candidate paket kimlikleri (aselsanos-rpi5.img 945760 B / ed1901a9…, dtb 78703 B / 40a2fbe9…, config.txt 420 B / aef848bf…) fixture olarak taşınır ve SHA256SUMS ile dondurulmuş dosyalardan yeniden hesaplanan özetlerle bayt-bayt eşleşmek zorundadır; her sapma fail-closed reddedilir. İmza doğrulaması S564 kapsamı dışıdır ve açıkça fail-closed reddedilir (S566/R2). Focused 24/24 PASS'tir. S540 ve S543 fiziksel RED immutable kalır; hiçbir SD, UART, board veya güncelleme işlemi yoktur; physical observation=0, RUNBOOK_EXECUTED_IN_S564=NO, Boot-to-UI=false ve R1 acceptance=false'dur. S565 aşamalı güncelleme apply/rollback modelidir ve bu modülün SHA-256 ve zincir makbuzlarını tüketecektir.
Doğrulanan kanıt
- S564, S563'ten ayrı kaynak modülü, 24-test focused binary, proof, status bloğu ve Operations kaydına sahiptir; kernel ve simulation crate'lerinde kayıtlıdır ancak hiçbir boot, IRQ, scheduler veya driver yoluna bağlanmamıştır.
- Dar S564 source/host model status=PASS; R1 umbrella=PARTIAL ve S540/S543 physical gate status=RED olarak ayrı tutulur.
- SHA-256 modülün içinde FIPS 180-4'e göre saf, no_std ve streaming (64 baytlık blok tamponu, checked 2^61 bayt mesaj sınırı) olarak implemente edilmiştir; "" → e3b0c442…52b855, "abc" → ba7816bf…f20015ad, 448-bit iki-blok vektörü ve bir milyon 'a' vektörü sabitlenmiştir; 200 baytlık mesajın her bölünmesi ve bayt-bayt streaming tek atımlık özeti yeniden üretir; S565 bu implementasyonu yeniden kullanacaktır.
- Manifest girişi path'i ≤ 64 bayt ASCII alfasayısal + '. - _ /' ile sınırlıdır; başta/sonda '/', boş segment, '.' ve '..' segmentleri fail-closed reddedilir; giriş bayt sayısı 1..=67108864 aralığındadır ve rol kodları 1..4 dışında her değer InvalidRole verir.
- Manifest başlığı monoton sürüm (0 reddedilir), 32 baytlık öncül manifest hash'i (all-zero yalnız genesis için) ve 1..=16 giriş sayısı taşır; tabloyla uyuşmayan başlık sayısı, tekrarlanan path ve tekil Kernel/Dtb/Config rollerinin tekrarı fail-closed reddedilir; toplam paket boyutu checked aritmetikle 268435456 bayt sınırına karşı toplanır.
- Kanonik kodlama ASOSMF01 magic, little-endian sürüm, öncül hash, giriş sayısı ve giriş başına rol/path-uzunluğu/path/bayt/özet alanlarından oluşur; en çok 1741 bayttır, deterministiktir, decoder üzerinden round-trip eder ve SHA-256'sı manifest hash'idir; kesik, taşan, trailing-byte'lı, yanlış magic'li, geçersiz rollü ve tekrarlanan path'li kodlamalar fail-closed reddedilir.
- Zincir doğrulaması öncül→ardıl yönünde 1..=8 uzunlukla sınırlıdır; ilk manifest genesis olmak zorundadır, her ardıl öncülünün kodlamasının exact SHA-256'sını ve kesin olarak daha büyük bir sürümü taşımak zorundadır; hash uyuşmazlığı, sıfır öncül hash'i ve monoton olmayan sürüm fail-closed reddedilir.
- Gözlenen paket head manifest girişleriyle sayı, path, bayt ve özet olarak exact eşleşmek zorundadır; eksik, fazla, yeniden adlandırılmış, tekrarlanan, yeniden boyutlandırılmış veya yeniden hash'lenmiş her dosya fail-closed reddedilir.
- S545 paket fixture'ı aselsanos-rpi5.img 945760 B / ed1901a991e2f9e9ae3c16f254147a2b0180686a8d70ca5d7353374fee08d467 (Kernel), bcm2712-rpi-5-b.dtb 78703 B / 40a2fbe9c29e8b9a4912cf726a943068defb779fc052ec38e457a79c58abca00 (Dtb) ve config.txt 420 B / aef848bf6e0c324148eade5054a15c71a1e8c04814a3ed2e680056f87c1f9bba (Config) kimliklerini taşır; focused test evidence/rpi5/r1/sequence-545-candidate-freeze/package/SHA256SUMS dosyasını yeniden okur ve üç dondurulmuş dosyanın özetlerini modülün kendi SHA-256'sıyla yeniden hesaplayıp fixture ile bayt-bayt eşleştirir.
- İmza doğrulaması S564 kapsamı dışıdır: servis her imza doğrulama isteğini SignatureOutOfScope ile fail-closed reddeder, receipt'te signature_verified=false ve scope sequence=566 (S566/R2) sabitlenir.
- Servis exact replay'de aynı receipt ile Retained döner; yayın sonrası her sapma PublishedStateDrift ile fail-closed reddedilir ve hata enum'u 35 sıfırdan farklı, benzersiz tanı kodu taşır.
- Focused target 1 grup / 24 passed / 0 failed / 0 ignored / 0 filtered verdi.
- Implementation 36461 B / 67360375745aa1b55c0d5886d4aa49b43f46b52df450a8b3d24740f822c3bfde; focused test 30136 B / 3e0bdc02a57f3d29c163ff36fafbca97a3f3f0b20a9c8877a6a00eba62d034d8 SHA-256'dır.
- Proof 5835 B'dir.
- Modül unsafe, MMIO, asm!, crate::uart, crate::arch, spin:: veya #[no_mangle] içermez; hiçbir cihaz işlemi yapılmadı ve S540/S543 yeniden koşulmadı.
- RUNBOOK_EXECUTED_IN_S564=NO; supported-profile runtime observations=0, physical observations=0, SD/UART/power/new-raw=0/0/0/0, Boot-to-UI physically observed=false ve R1 acceptance=false'dur.
- S565 aşamalı güncelleme apply/rollback modelini aynı non-claim'lerle kaynak/host kapısı olarak modelleyecek ve S564'ün SHA-256 ile manifest zinciri makbuzlarını tüketecektir; SD, UART, power veya fiziksel güncelleme koşusu yetkisi vermez.
Sınır / bekleyen kanıt
- S564 yalnız kaynak/host modelidir; hiçbir donanım/panel/modem/board gözlemi yoktur ve hiçbir güncelleme SD karta yazılmamıştır.
- S540 ve S543 fiziksel RED immutable kalır; otomatik promotion yoktur ve S546 ayrı bir kapı olarak beklemededir.
- İmza doğrulaması modellenmemiştir ve S564'te açıkça kapsam dışıdır; S566/R2 kapsamındadır ve o zamana kadar her imza doğrulama isteği fail-closed reddedilir.
- Boot-to-UI fiziksel olarak gözlenmedi; R1 acceptance false kalır ve modül hiçbir production boot/IRQ/scheduler/driver yoluna bağlanmamıştır.
- S565 aşamalı güncelleme apply/rollback modeli tamamlanmadan güncelleme akışının uygulama tarafı modellenmiş sayılmaz; S565 de SD, UART, power veya fiziksel koşu yetkisi vermez.
Terminal komutları ve gerçek yanıtlar
S564 kaynak/host model kapısıdır; supported-profile runtime veya fiziksel PASS değildir. S540 ve S543 RED raw'ları ve kararları değişmez.
$ CARGO_INCREMENTAL=0 cargo test -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s564_r1_update_package_manifest_hash_chain_model -- --test-threads=1test result: ok. 24 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s
S564 focused=1 group / 24 passed / 0 failed
hardware=none physical=0 runbook=NO