EverCrypt: криптографиялык текшерүү китепканасы

Everest долбоору

Изилдөөчүлөр Мамлекеттик информатика жана автоматика илим изилдөө институту (ИНРИА), Microsoft Research жана Карнеги Меллон университетинин бет ачары болду биринчи сынамык чыгарылышы EverCrypt крипто-китепканасы Эверест долбоорунун алкагында иштелип чыккан жана формалдуу ишенимдүүлүктү текшерүүнүн математикалык методдору колдонулган.

Анын мүмкүнчүлүктөрү жана натыйжалуулугу үчүн, EverCrypt учурдагы крипто китепканаларына жакын (OpenSSL), бирок алардан айырмаланып, ишенимдүүлүктүн жана коопсуздуктун кошумча кепилдиктерин берет.

Мисалы, текшерүү процесси толук мүнөздөмөлөрдү аныктоого чейин кайнайт программанын бардык жүрүм-турумун сүрөттөгөн жана жазылган коддун математикалык далили даярдалган техникалык шарттарга жооп берет.

Далилдүү сапатты контролдоо методдорунан айырмаланып, текшерүү ишенимдүү кепилдиктерди берет программа иштеп чыгуучулар каалагандай иштей берет жана каталардын конкреттүү түрлөрү жок.

Мисалы, спецификацияга ылайык эс тутум менен коопсуз иштөөнү жана буфердин ашып кетишине алып келүүчү каталардын жоктугун камсыз кылат, көрсөткүчтөрдү ажыратуу, мурунтан эле бошотулган эс тутумдарына кирүү же эс тутум блокторун эки эсе бошотуу.

EverCrypt деген эмне?

EverCrypt күчтүү түрүн жана баалуулугун текшерүүнү камсыз кылат- Компонент эч качан башка шайкеш келбеген компонентке параметрлерди өткөрбөйт жана башка компоненттердин ички абалына кире албайт.

Киргизүү / чыгаруу жүрүм-туруму жөнөкөй математикалык иш-аракеттерге толугу менен шайкеш келет, алар криптографиялык стандарттарда аныкталат.

Кол салуудан коргоо үчүнчү жактын каналдарында, эсептөө учурунда жүрүм-турум (мисалы, аткаруунун узактыгы же белгилүү бир эс тутумга кирүү мүмкүнчүлүктөрү) ал иштелип чыккан жашыруун маалыматтарга көз каранды эмес.

Долбоордун коду F * функционалдык тилинде жазылган (F жылдыз) , көз каранды түрлөрдүн жана тактоолордун тутумун камсыз кылат, бул программалар үчүн так спецификацияларды (математикалык модель) белгилөөгө жана SMT формулаларынын жана жардамчы тест куралдарынын жардамы менен ишке ашырууда каталардын туура жана туура эместигине кепилдик берет.

F * коду Apache 2.0 лицензиясына, ал эми акыркы модулдар C жана ассемблер MIT лицензиясына ылайык бөлүштүрүлөт.

F * маалымдама кодунун негизинде, ассемблер, C, OCaml, JavaScript түзүлдү жана желе жыйноо коду.

Кодекстин айрым бөлүктөрү даяр Долбоор тарабынан Firefox, Windows өзөгү колдонулуп келген , blockchain Tezos жана VPN Wireguard.

EverCrypt компоненттери

Чындыгында, EverCrypt HACL * жана Vale компанияларынан бири-бирине окшобогон эки долбоорду бириктирет, алардын негизинде бирдиктүү API камсыз кылуу жана аларды чыныгы долбоорлордо колдонууга ылайыктуу кылуу.

HACL * Төмөндө жазылган* жана анын максаты - C программаларында колдонуу үчүн криптографиялык примитивдерди камсыз кылуу алар libsodium жана NaCL стилиндеги APIлерди колдонушат.

долбоору Вале белгилүү бир тилди иштеп чыккан ассемблерде текшерүүлөрдү түзүү үчүн домен.

Төмөнкү тилдеги 110 миң сап HACL * коду жана Vale үчүн 25 миң сап коду бириктирилген жана алар 70 миң линияга жакын универсалдык тилде жазылган *, ал дагы иштелип жатат Эверест долбоорунун алкагында.

EverCrypt китепканасынын биринчи версиясы текшерилген жүзөгө ашыруунун өзгөчөлүктөрү төмөнкү криптографиялык алгоритмдердин С же ассемблер нускаларында сунуш кылынган (. колдонулганда.

Алардын ичинен, долбоордун бетинде төмөнкүлөр турат:

  • Хэш алгоритмдери: SHA2, SHA3, SHA1 жана MD5 бардык варианттары
  • Аныктыгын текшерүү коддору: Маалымат булагынын аныктыгын текшерүү үчүн SHA1, SHA2-256, SHA2-384 жана SHA2-512 үстүнөн HMAC.
  • HKDF ачкычын алгоритмдөө (HMAC негизиндеги кеңейтүү жана бөлүп алуу ачкычын чыгаруу функциясы)
  • ChaCha20 агымын шифрлөө (оптимизацияланбаган С версиясы бар)
  • Poly1305 Билдирүүнүн аныктыгын текшерүү алгоритми (MAC) (C жана ассемблердин версиясы)
  • Curve25519 эллиптикалык ийри сызыктары боюнча Diffie-Hellman протоколу (BMI2 жана ADX көрсөтмөлөрүнө негизделген оптимизацияланган С жана ассемблер версиялары)
  • Бөгөттөөчү шифрлөө режими AEAD (тастыкталган шифр) ChachaPoly (С версиясы оптималдаштырылган эмес)
  • AEAD AES-GCM блоктук шифрлөө режими (AES-NI оптимизациясы бар ассемблердин версиясы).

Биринчиден альфа версиясы, код текшерүү мурунтан эле аяктаган негизинен, бирок дагы деле болсо ачыла элек жерлер бар.

Мындан тышкары, API азырынча турукташтырыла элек, ал кеңейтилет төмөнкү альфа нускаларында (Бардык API үчүн түзүмдөрдү бирдиктүү кылуу пландаштырылууда.

Кемчиликтердин катарында x86_64 архитектурасын колдоо дагы белгиленди (биринчи этапта негизги максат ишенимдүүлүк, ал эми экинчи орунда оптимизация жана платформалар ишке ашырылат).

булагы: https://jonathan.protzenko.fr


Макаланын мазмуну биздин принциптерге карманат редакциялык этика. Ката жөнүндө кабарлоо үчүн чыкылдатыңыз бул жерде.

Комментарий биринчи болуп

Комментарий калтырыңыз

Сиздин электрондук почта дареги жарыяланбайт.

*

*

  1. Маалыматтар үчүн жооптуу: Мигель Анхель Гатан
  2. Маалыматтын максаты: СПАМды көзөмөлдөө, комментарийлерди башкаруу.
  3. Мыйзамдуулук: Сиздин макулдугуңуз
  4. Маалыматтарды берүү: Маалыматтар үчүнчү жактарга юридикалык милдеттенмелерден тышкары билдирилбейт.
  5. Маалыматтарды сактоо: Occentus Networks (ЕС) тарабынан уюштурулган маалыматтар базасы
  6. Укуктар: Каалаган убакта маалыматыңызды чектеп, калыбына келтирип жана жок кыла аласыз.

bool(чын)