EverCrypt: криптографиялық тексеру кітапханасы

Everest жобасы

Бастап зерттеушілер Мемлекеттік информатика және автоматика ғылыми-зерттеу институты (ИНРИЯ), Microsoft Research және Карнеги Меллон университеті таныстырды алғашқы сынақ басылымы EverCrypt крипто-кітапханасы Эверест жобасы шеңберінде және формальды сенімділікті растаудың математикалық әдістерін қолдана отырып әзірленген.

Оның мүмкіндіктері мен өнімділігі үшін, EverCrypt қолданыстағы крипто-кітапханаларға өте жақын (OpenSSL), бірақ олардан айырмашылығы сенімділік пен қауіпсіздіктің қосымша кепілдіктерін ұсынады.

Мысалы, тексеру процесі егжей-тегжейлі сипаттамаларды анықтауға дейін қайнайды бағдарламаның барлық әрекеттерін сипаттайтын және жазбаша кодтың математикалық дәлелі дайындалған сипаттамаларға сәйкес келеді.

Дәлелді сапаны бақылау әдістерінен айырмашылығы, тексеру сенімді кепілдіктер береді Бағдарлама әзірлеушілер қалағандай жұмыс істейді және қателіктердің нақты кластары жоқ.

Мысалы, спецификацияға сәйкестік жадпен қауіпсіз жұмыс істеуді және буфердің асып кетуіне әкелетін қателіктердің болмауын қамтамасыз етеді, сілтемелерді өшіру, бұрыннан босатылған жад аймақтарына қол жеткізу немесе жад блоктарын екі есе босату.

EverCrypt дегеніміз не?

EverCrypt сенімді типті және мәнді тексеруді қамтамасыз етеді- Компонент ешқашан параметрлерді басқа сәйкес келмейтін компонентке бермейді және басқа компоненттердің ішкі күйлеріне қол жеткізе алмайды.

Кіріс / шығыс әрекеті қарапайым математикалық функцияларға толығымен сәйкес келеді, олар криптографиялық стандарттарда анықталған.

Шабуылдан қорғау үшінші тарап арналарында, есептеулер кезіндегі тәртіп (мысалы, орындалу ұзақтығы немесе белгілі бір жадқа қол жетімділіктің болуы) бұл өңделетін құпия деректерге байланысты емес.

Жоба коды F * функционалды тілінде жазылған (F жұлдызы) , тәуелді типтер мен нақтылау жүйесін қамтамасыз етеді, бұл бағдарламалар үшін нақты сипаттамаларды (математикалық модель) орнатуға мүмкіндік береді және SMT формулалары мен көмекші тест құралдары арқылы іске асырудағы қателіктер мен дұрыстығына кепілдік береді.

F * ішіндегі код Apache 2.0 лицензиясы бойынша, ал соңғы модульдер C және ассемблер MIT лицензиясы бойынша таратылады.

F * сілтеме коды негізінде, ассемблер, C, OCaml, JavaScript құрылды және веб-құрастыру коды.

Кодтың кейбір бөліктері дайындалған жоба бойынша Windows ядросы Firefox-та қолданылып келеді , blockchain Tezos және VPN сымды қорғау.

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

Негізінде, EverCrypt HACL * және Vale-дің екі түрлі жобаларын біріктіреді, олардың негізінде бірыңғай API ұсынып, оларды нақты жобаларда қолдануға жарамды етеді.

HACL * төмен деңгейде жазылған* және оның мақсаты - C бағдарламаларында қолдану үшін криптографиялық примитивтерді ұсыну олар libsodium және NaCL стиліндегі API қолданады.

Жоба Вале белгілі бір тілді дамытты ассемблерде тексерулер жасау үшін домен.

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

EverCrypt кітапханасының алғашқы нұсқасы тексерілген іске асырудың ерекшеліктері келесі криптографиялық алгоритмдер C немесе ассемблер нұсқаларында ұсынылған (.

Осылардың ішінен жоба парағында мыналар ерекшеленеді:

  • Хэш алгоритмдері: 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. Құқықтар: Сіз кез-келген уақытта ақпаратты шектей, қалпына келтіре және жоя аласыз.