• [^] # Re: SeL4

    Posté par . En réponse au journal KataOS, un OS sécurisé basé sur SeL4 écrit en Rust ... par Google. Évalué à 8.

    Bah, seL4 ça n'est pas juste du C, c'est du C+des preuves formelles qui fournissent plus d'"assurances" que Rust.
    Et en plus avec le C, il existe un compilateur "prouvé formellement" CompCert, chose que Rust n'a pas donc tout bug du compilateur Rust peut impacter ta sécurité..

    Sauf qu'évidemment pour tout changement de seL4, il faut "refaire" les preuves!
    Et KataOS a modifié seL4 sans pour autant faire évoluer les preuves (pour le moment).