BERK Hard RT Core — EAL7-hedefli deterministik yürütme motoru
Güvenlik-kritik gömülü sistemler için deterministik yürütme motoru: TLA+/TLC ile model denetimi yapılmış eşzamanlılık tasarımı, HSM entegrasyonu, değiştirilemez karar günlüğü ve WCET analizli zamanlama.
18,4 milyon durum. Sıfır hata.
Çekirdeğin eşzamanlılık modeli TLA+ ile modellendi ve TLC model denetçisiyle 18.404.041 durum üzerinde tarandı — 41 derinliğe kadar, hatasız.
Kanıtlanan özellikler
NoDeadlock, WriteLockExclusive, NoReadWriteConflict, DJRRecordsUnique, DJRVersionMonotonic, ValidAuthorityLevels, TypeInvariant — tümü makine-denetimli.
Karar günlüğü (DJR)
Değiştirilemez denetim izi: her karar benzersiz, sürümü monoton artan kayıtlarla günlüklenir. DPAL katmanı — Defensible, Provable, Auditable, Lawful.
HSM entegrasyonu
Donanım güvenlik modülü desteği: YubiHSM 2, TPM 2.0 ve PKCS#11. Çok-seviyeli yetki denetimi (Authority Checker) ile birlikte çalışır.
Hard real-time
WCET analizli deterministik zamanlama; arena tahsisçisi ile deterministik bellek; O(log n) uzamsal indeksleme (R-Tree) ve tombstone yaşam-döngüsü.
Gömülüye hazır
no_std derleme hedefi; lock-free eşzamanlılık ilkelleri; savunma kullanım senaryolarında yüksek işlem-hacmi (ops/sec) için tasarlandı.
EAL7-hedefli
Common Criteria yüksek-güvence sertifikasyonu için tasarlandı. BerkLink taktik veri bağlantısı ürününün çekirdeğini oluşturur.