Истраживачи из Државни институт за истраживање информатике и аутоматизације (ИНРИА), Представили су Мицрософт Ресеарцх и Царнегие Меллон Университи прво пробно издање крипто библиотека ЕверЦрипт развијен у оквиру пројекта Еверест и користећи математичке методе формалне провере поузданости.
Због својих могућности и перформанси, ЕверЦрипт је врло близу постојећих крипто библиотека (ОпенССЛ), али то, за разлику од њих, нуди додатне гаранције поузданости и сигурности.
Нпр поступак верификације своди се на дефинисање детаљних спецификација који описују сва понашања програма и математички доказ да је писани код задовољава припремљене спецификације.
За разлику од метода контроле квалитета заснованих на доказима, верификација пружа поуздане гаранције да ће се програм покретати само онако како су програмери намеравали и да нема специфичних врста грешака.
На пример, усклађеност са спецификацијом осигурава сигуран рад са меморијом и одсуство грешака које доводе до преливања бафера, на дереференце показиваче, приступ већ ослобођеним меморијским областима или двоструко ослобађање меморијских блокова.
Шта је ЕверЦрипт?
ЕверЦрипт пружа робусну проверу типа и вредности- Компонента никада неће проследити параметре другој компоненти која није у складу и неће добити приступ унутрашњим стањима осталих компоненти.
Понашање улаз / излаз у потпуности одговара једноставним акцијама математичке функције, који су дефинисани у криптографским стандардима.
За заштиту од напада на независним каналима, понашање током прорачуна (на пример, трајање извршења или присуство приступа одређеној меморији) не зависи од тајних података који се обрађују.
Код пројекта написан је на функционалном језику Ф * (Ф звезда) , који обезбеђује систем зависних типова и пречишћавања, који омогућавају успостављање тачних спецификација (математички модел) за програме и гарантовање исправности и одсуства грешака у имплементацији помоћу СМТ формула и помоћних алата за тестирање.
Код у Ф * дистрибуира се под лиценцом Апацхе 2.0, а коначни модули у језику Ц и асемблер под лиценцом МИТ.
На основу референтног кода Ф *, асемблер, Ц, ОЦамл, генерише се ЈаваСцрипт и код веб окупљања.
Неки делови кода припремљено по пројекту се већ користе у Фирефоку, Виндовс језгру , блоцкцхаин оф Тезос и ВПН Вирегуард.
ЕверЦрипт компоненте
У суштини, ЕверЦрипт комбинује два претходно различита пројекта од ХАЦЛ * и Вале, пружајући јединствени АПИ заснован на њима и чинећи их погодним за употребу у стварним пројектима.
ХАЦЛ * је написан малим словом* а његов циљ је да обезбеди криптографске примитиве за употребу у Ц програмима који користе АПИ либсодиум и НаЦЛ стила.
Пројекат Вале је развио специфичан језик домена за креирање верификација у асемблеру.
Комбиновано је око 110 хиљада редова ХАЦЛ * кода на језику Лов * и 25 хиљада редова кода за Вале а преписани су у око 70 хиљада редова кода на универзалном језику Ф *, који се такође развија у оквиру пројекта Еверест.
Прва верзија библиотеке ЕверЦрипт садржи верификоване имплементације следећих криптографских алгоритама предложен у верзији Ц или асемблеру (када се користи.
Од њих се на страници пројекта истичу:
- Хасх алгоритми: све варијанте СХА2, СХА3, СХА1 и МД5
- Кодови за аутентификацију: ХМАЦ преко СХА1, СХА2-256, СХА2-384 и СХА2-512 за аутентификацију извора података
- ХКДФ алгоритам генерисања кључева (функција извлачења и проширивања кључа на основу ХМАЦ-а)
- Шифровање тока ЦхаЦха20 (доступна је неоптимизирана верзија Ц)
- Поли1305 алгоритам за потврду идентитета порука (МАЦ) (Ц и асемблерска верзија)
- Диффие-Хеллманов протокол на елиптичним кривуљама Цурве25519 (верзије Ц и асемблера са оптимизацијама на основу БМИ2 и АДКС упутстава)
- Режим блок-шифре АЕАД (оверена шифра) ЦхацхаПоли (верзија Ц није оптимизована)
- АЕАД АЕС-ГЦМ режим шифровања блока (верзија асемблера са АЕС-НИ оптимизацијама).
У првом алфа верзија, верификација кода је већ завршена углавном, али још увек постоје нека откривена подручја.
Поред тога, АПИ још увек није стабилизован, који ће бити проширен у следећим алфа верзијама (Планирано је обједињавање структура за све АПИ-је.
Међу недостацима је истакнута и подршка за архитектуру к86_64 (у првој фази главни циљ је поузданост, док ће оптимизација и платформе бити примењене на другом месту).
izvor: https://jonathan.protzenko.fr