Tutkijat Valtion tietotekniikan ja automaation tutkimuslaitos (INRIA), Microsoft Research ja Carnegie Mellon University esittivät - ensimmäinen kokeiluversio EverCrypt-salauskirjasto kehitetty Everest-projektin puitteissa ja käyttäen muodollisen luotettavuuden todentamisen matemaattisia menetelmiä.
Sen ominaisuuksien ja suorituskyvyn vuoksi EverCrypt on hyvin lähellä olemassa olevia salauskirjastoja (OpenSSL), mutta se, toisin kuin he, tarjoaa lisätakeita luotettavuudesta ja turvallisuudesta.
Esimerkiksi todentamisprosessi päättyy yksityiskohtaisten eritelmien määrittelyyn jotka kuvaavat kaikkia ohjelman käyttäytymismalleja ja matemaattinen todiste siitä, että kirjoitettu koodi täyttää valmistetut vaatimukset.
Toisin kuin näyttöön perustuvat laadunvalvontamenetelmät, todentaminen antaa luotettavat takuut että ohjelma toimii vain kehittäjien tarkoituksella eikä siinä ole erityisiä virheitä.
Esimerkiksi eritelmän noudattaminen varmistaa turvallisen työskentelyn muistin kanssa ja virheiden puuttumisen, jotka johtavat puskurin ylivuotoon, poikkeamaosoitteisiin, pääsyyn jo vapautuneille muistialueille tai kaksinkertaiselle muistilohkojen vapauttamiselle.
Mikä on EverCrypt?
EverCrypt tarjoaa vankan tyypin ja arvon tarkistuksen- Komponentti ei koskaan välitä parametreja muulle yhteensopimattomalle komponentille eikä pääse muiden komponenttien sisäisiin tiloihin.
Tulo- / lähtökäyttäytyminen noudattaa täysin yksinkertaisia matemaattisten toimintojen toimintoja, jotka määritellään salaustandardeissa.
Suojaa hyökkäyksiltä kolmannen osapuolen kanavilla, käyttäytyminen laskelmien aikana (esimerkiksi suorituksen kesto tai pääsy tiettyyn muistiin) se ei riipu käsiteltävistä salaisista tiedoista.
Projektin koodi on kirjoitettu toiminnallisella kielellä F * (F-tähti) , joka tarjoaa riippuvien tyyppien ja tarkennusten järjestelmän, joiden avulla voidaan määrittää ohjelmille tarkat erittelyt (matemaattinen malli) ja taata toteutuksen oikeellisuus ja virheiden puuttuminen SMT-kaavojen ja aputestityökalujen avulla.
F *: n koodi jaetaan Apache 2.0 -lisenssillä, ja lopulliset moduulit C: ssä ja assembler MIT-lisenssillä.
Viitekoodin F * perusteella assembler, C, OCaml, JavaScript on luotu ja verkkoasennuskoodi.
Jotkut koodin osat valmistetut ovat jo käytössä Firefoxissa, Windows-ytimessä , lohkoketju Tezos ja VPN Wireguard.
EverCrypt-komponentit
Pohjimmiltaan EverCrypt yhdistää kaksi aiemmin erilaista projektia HACL *: lta ja Valelta, tarjoamalla niihin perustuvan yhtenäisen sovellusliittymän ja tekemällä niistä sopivia käytettäväksi todellisissa projekteissa.
HACL * on kirjoitettu matalalla* ja sen tavoitteena on tarjota salausprimitiivejä käytettäväksi C-ohjelmissa, jotka he käyttävät libsodium- ja NaCL-tyyppisiä sovellusliittymiä.
El proyecto Vale kehitti tietyn kielen verkkotunnuksen avulla luomaan tarkistuksia kokoonpanijaan.
Noin 110 tuhatta riviä HACL * -koodia matalalla * kielellä ja 25 tuhatta riviä Vale-koodia yhdistetään ja ne kirjoitetaan uudelleen noin 70 tuhanteen koodiriviin yleiskielellä F *, jota myös kehitetään osana Everest-hanketta.
EverCrypt-kirjaston ensimmäinen versio sisältää vahvistettuja toteutuksia seuraavista salausalgoritmeista ehdotettu C - tai assembler - versioina (kun käytetään.
Näistä seuraavat erottuvat projektisivulta:
- Hash-algoritmit: kaikki SHA2-, SHA3-, SHA1- ja MD5-variantit
- Todennuskoodit: HMAC SHA1, SHA2-256, SHA2-384 ja SHA2-512 kautta tietolähteen todennukseen
- HKDF-avaimen luontialgoritmi (HMAC-pohjainen purku- ja laajennusavaimen johtofunktio)
- ChaCha20-salauksen salaus (ei-optimoitu C-versio saatavana)
- Poly1305-sanoman todennusalgoritmi (MAC) (C- ja assembler-versio)
- Diffie-Hellman-protokolla elliptisillä käyrillä Curve25519 (C- ja assembler-versiot optimoinnilla BMI2- ja ADX-ohjeiden perusteella)
- Estä salaustila AEAD (todennettu salaus) ChachaPoly (versiota C ei optimoitu)
- AEAD AES-GCM -lohkosalaustila (assembler-versio AES-NI-optimoinnilla).
Ensimmäisessä alfaversio, koodin vahvistus on jo saatu päätökseen suurelta osin, mutta joitain alueita on vielä paljastettu.
Lisäksi, API ei ole vielä vakiintunut, jota laajennetaan seuraavissa alfaversioissa (Kaikkien sovellusliittymien rakenteita on tarkoitus yhtenäistää.
Virheistä tuetaan myös x86_64-arkkitehtuurin tukea (ensimmäisessä vaiheessa päätavoitteena on luotettavuus, kun taas optimointi ja alustat toteutetaan toiseksi).
lähde: https://jonathan.protzenko.fr