Djinious
Logica di sicurezza
Logica di voto 2oo3 e un trip a latching che resta vero una volta attivato.
REQ-SF-001 · 002Nove funzioni di sicurezza, dal requisito YAML al Rust embedded certificato
Il progetto di riferimento del voter porta nove funzioni di sicurezza — voto, latching, limitazione di slew rate, monitoraggio del trip, interblocchi e un misuratore di flusso con un confine in virgola mobile — attraverso tutti e tredici i gate, e riproduce ognuna su un Cortex-M4F emulato.
DjiniousSafe
- funzioni di sicurezza
- 9funzioni di sicurezzaREQ-SF-001 a REQ-SF-016
- gate superati
- 13gate superatiBUILD ACCEPTED
- casi on-target per flow_gauge
- 406casi on-target per flow_gauge0 falliti · 78 casi in virgola mobile
- differenze tra due build
- 0differenze tra due buildevidence.json, hash ELF inclusi
Il progetto
examples/voter è un progetto djsafe completo: un file di requisiti, le specifiche Lean a cui punta, e una sezione target che indica thumbv7em-none-eabihf sulla macchina QEMU netduinoplus2. È il progetto che viene consegnato a un valutatore esterno insieme a un pacchetto di evidenze.
Ogni requisito dice, in testo semplice, cosa deve fare la funzione — “L’uscita del voter deve essere vera se e solo se almeno due dei tre canali di ingresso sono veri” — e il suo testo normalizzato negli spazi bianchi è fissato tramite hash nelle evidenze, così un cambio di formulazione è un cambiamento che la build può vedere.
Cosa coprono le nove funzioni
Controllo a virgola fissa
Un limitatore di slew rate bloccato a ±100 per step entro [−1000, 1000], un monitor di trip a due stati con isteresi, e un blocco di guadagno Q4.
REQ-SF-010 · 011 · 012Divisione, radici e aritmetica estesa
Medie, rapporti, radici quadrate, moduli vettoriali e contatori modulo, inclusa l’aritmetica estesa i64 — certificata priva di panic.
REQ-SF-013 · 014Ingressi misti
Un interblocco di pressione che scatta all’abilitazione a ≥ 3000 e si azzera al reset sotto 2500, con la pressione nel caso peggiore mantenuta e un margine di sicurezza.
REQ-SF-015Un confine in virgola mobile
Un misuratore di flusso il cui valore del sensore entra come f32 IEEE-754 attraverso una conversione certificata solo-intera a Q4, e il cui margine esce come f32 convertito esattamente — nucleo a virgola fissa invariato.
REQ-SF-016Una build, gate per gate
Requisiti e dimostrazioni
I requisiti vengono analizzati con ID univoci; l’intero pacchetto Lean — specifiche, libreria di semantica, ogni teorema — si elabora e viene verificato dal kernel.
Esportazione fresca
Ogni artefatto derivato da Lean viene rigenerato dai moduli appena verificati, e una funzione che non è ben formata viene rifiutata in esportazione.
Passaggi di consegne fissati tramite hash
L’IR, i sorgenti delle specifiche e la libreria di semantica vengono sottoposti a hash sia da Lean sia da Rust, e i due devono concordare.
Tracciabilità
Ogni requisito è soddisfatto da qualche funzione, e ogni funzione cita solo requisiti noti.
Due generatori, un solo programma
“9 funzioni identiche per AST tra sgen-a e sgen-b”, poi canoniche a livello di byte per entrambi.
Certificati
Per ogni funzione, cinque teoremi sull’artefatto così come riletto dai byte distribuiti, verificati dal kernel Lean.
Riproduzione
Vettori di riferimento Lean rispetto al codice compilato sull’host, poi per ogni funzione sul target emulato, con ogni ELF sottoposto a hash.
Evidenze
Certificati, matrice di tracciabilità, manifest back-to-back e trascrizione on-target assemblati in un unico pacchetto.
Verificato da qualcuno diverso dalla pipeline
La guida alle evidenze fornisce a un valutatore cinque procedure che non dipendono dal report della pipeline stessa, ciascuna eseguita come scritto. Per flow_gauge: un terzo SHA-256 del sorgente delle specifiche corrisponde sia agli hash registrati sia all’intestazione del certificato; il certificato viene rieseguito attraverso il kernel con exit 0 e dipende solo da propext e Quot.sound; e l’ELF riprodotto a mano stampa “B2BT flow_gauge cases=406 failed=0 float_cases=78” con un hash uguale a quello nelle evidenze.
La guida è altrettanto esplicita sui limiti: la validità dei requisiti resta una revisione umana, nessuna affermazione riguarda i tempi o i limiti dello stack, e QEMU non è silicio.
Continua a esplorare
Casi d’uso correlati
Controllo e apprendimento per rinforzoControllo del cart-pole e RLIl benchmark canonico del controllo sottoattuato, affrontato end-to-end — dinamica non lineare, un LQR che stabilizza il pendolo invertito, un avviamento a oscillazione energetica, una policy di apprendimento per rinforzo model-free, e un gate di robustezza Monte Carlo.
DjiniousLab
ElettromagnetismoElettromagnetismo (FDTD)Risolvere le equazioni di Maxwell su una griglia — i campi elettrico e magnetico che si susseguono a salti nello spazio e nel tempo. Un risolutore FDTD autonomo riproduce i fenomeni ondulatori canonici: irradiazione, rifrazione, diffrazione, diffusione e risonanza di cavità. Il fratello a campo del CFD, in elettromagnetismo.DjiniousLab
Machine learning scientificoML scientifico (UDE)Scoprire la fisica mancante a partire dai dati con le Universal Differential Equations — mantieni la fisica che conosci, impara il divario con una rete neurale addestrata attraverso il solver ODE, poi rileggi il termine appreso come un’equazione simbolica che estrapola dove un modello a scatola nera non può.DjiniousLab