ایور کریپټ: د کریپټوګرافیک تایید کتابتون

د په انفارمټیکس او اتوماتیک کې د څیړنې لپاره دولتي انستیتیوت (INRIA), د مایکروسافټ ریسرچ او کارنیګي میلون پوهنتون وړاندې کړل د د ایورکریټ کریپټو کتابتون د ایوریسټ پروژې کاري چوکاټ کې وده کړې او د رسمي اعتبار تایید ریاضياتي میتودونو کارولو سره.

د دې د وړتیاو او کړنو لپاره ، ایور کریپټ موجود کریپټو کتابتونونو ته خورا نږدې دی (OpenSSL) مګر دا ، د دوی په خلاف ، د اعتبار او امنیت اضافي تضمین وړاندیز کوي.

د مثال په توګه، د تایید پروسه د تفصيلي مشخصاتو تعریف کولو ته وده کوي چې د برنامه ټول چلندونه بیانوي او د ریاضیاتو ثبوت چې لیکل شوی کوډ دی چمتو شوي توضیحات پوره کوي.

د شواهدو پر بنسټ د کیفیت کنټرول میتودونو برخلاف ، تصدیق باوري تضمینونه وړاندې کوي دا چې برنامه به یوازې د پرمخ وړونکو په توګه پرمخ وځي او کومې ځانګړې غلطي شتون نلري.

د مثال په توګه ، د مشخصاتو سره موافقت د حافظې سره خوندي کار تضمینوي او د غلطیو نشتوالی چې د بفر پراخه کیدو لامل کیږي، اشاره کونکي نښو ته ، دمخه آزاد شوي حافظې سیمو ته لاسرسی ، یا د حافظې بلاکونو دوه چنده کول.

ایور کریپټ څه شی دی؟

تلپاتې قوي ب andه او ارزښت ارزونه وړاندې کوي- یوه برخه به هیڅکله نور غیر تعمیل برخې ته پیرامیټونه نه انتقالوي او د نورو اجزا داخلي حالتونو ته به لاسرسی ونلري.

ننوت / وتلي چال په بشپړ ډول د ساده ریاضي فعالیت افعالاتو سره مطابقت لري، کوم چې د کریپټوګرافیک معیارونو کې تعریف شوي.

د بریدونو په وړاندې د ساتنې لپاره په دریم ګوند چینلونو کې ، د محاسبې په جریان کې چلند (د مثال په توګه ، د اعدام موده یا ځانګړي حافظې ته د لاسرسي شتون) دا په پټو معلوماتو پورې اړه نلري چې پروسس کیږي.

د پروژې کوډ په فعاله ژبه F لیکل شوی (F ستوری) , دا د انحصار ډولونه او تصفیه کولو سیستم چمتو کوي، کوم چې د برنامو لپاره دقیق مشخصات (ریاضياتي ماډل) رامینځته کولو ته اجازه ورکوي او د SMT فارمولونو او معاون ازموینې وسیلو په واسطه پلي کولو کې د غلطیتونو نشتوالۍ او تضمین تضمینوي.

په F * کې کوډ د اپاچي 2.0 جواز لاندې توزیع شوی ، او په C کې وروستي ماډلونه او د MIT لایسنس لاندې راټولونکي.

د حوالې کوډ F * پراساس ، راټولونکی ، C ، OCaml ، جاواسکریپټ تولید شوی او د ویب مجلس کوډ.

د کوډ ځینې برخې چمتو شوی د پروژې لخوا لا دمخه په فایرفاکس ، وینډوز کارنیل کې کارول شوي دي د Tezos او VPN Wireguard.

د تل لپاره کریپټ برخې

په لنډ ډول ، ایور کریپټ د HACL * او ویل څخه دوه پخوانۍ بیلابیل پروژې راټولوي، د دوی پراساس یو متحد API چمتو کول او دوی ته په ریښتیني پروژو کې د کارونې لپاره مناسب چمتو کول.

HACL * په ټیټ کې لیکل شوی* او د دې هدف د C برنامو کې د کارونې لپاره کریپټوګرافیک لومړني چمتو کول دي چې دوی د لیبسوډیم او NaCL سټایل API کاروي.

پروژه ویل یوه ځانګړې ژبه رامینځته کړه ډومین په راډیکال کې د تاییداتو رامینځته کولو لپاره.

په ټیټ * ژبه کې د HACL * کوډ شاوخوا 110 زره لینونه او د Vale لپاره 25 زره لینونه یوځای شوي او دوی په نړیواله ژبه F * کې د کوډ شاوخوا شاوخوا 70 زره لینونو کې بیا لیکل شوي ، کوم چې ورته وده ورکول کیږي د ایوریسټ پروژې برخې په توګه.

د ایور کریپټ کتابتون لومړۍ نسخه د تایید شوي پلي کونکي ب featuresې د لاندې کریپټوګرافیک الګوریتمونو څخه په سي یا ارسبل نسخو کې وړاندیز شوی (کله چې د.

له دې جملې څخه لاندې د پروژې په پا onه کې څرګند دي:

• د هش الګوریتمونه: د SHA2 ، SHA3 ، SHA1 ، او MD5 ټول ډولونه
• د تصدیق کولو کوډونه: د ډیټا سرچینې تصدیق لپاره HMAC په SHA1 ، SHA2-256 ، SHA2-384 ، او SHA2-512 باندې
• د HKDF کلي د نسل الګوریتم (د HMAC پر بنسټ توسعې او استخراج کلیدي استخراج کولو فعالیت)
• د ChaCha20 جریان کوډ ورکول (غیر مطلوب C نسخه شتون لري)
• Poly1305 د پیغام تصدیق الګوریتم (MAC) (سي او راټولونکی نسخه)
• د بیضوي منحنی curve 25519 په اړه دفا - هیلمن پروتوکول (د BMI2 او ADX لارښوونو پراساس د اصلاح کولو سره C او د راټولولو نسخې)
• د بلوک کولو کوډ حالت AEAD (تایید شوي کوډیز) چاچاپولي (نسخه C مطلوب نه شوې)
• د AEAD AES-GCM بلاک کوډیز کولو حالت (د AES-NI اصلاحاتو سره د راټولولو نسخه).

په لومړي کې د الفا نسخه ، د کوډ تایید لا دمخه بشپړ شوی په لویه کچه ، مګر لاهم یو شمیر ساحې خلاصې دي.

همدارنګه، API لاهم ثبات نلري، کوم چې به پراخه شي په الفا نسخو کې (دا پلان شوی چې د ټولو APIs لپاره جوړښتونه متحد کړي.

د نیمګړتیاو په مینځ کې ، د x86_64 معمار سره مطابقت هم روښانه شوی (په لومړي مرحله کې ، اصلي هدف د اعتبار وړ دی ، پداسې حال کې چې اصلاح او پلیټ فارم به په دوهم ځای کې پلي شي).

سرچینه: https://jonathan.protzenko.fr