EverCrypt: ספריית אימות הצפנה

פרויקט האוורסט

חוקרים מ המכון הממלכתי לחקר מידע ואוטומציה (INRIA), מחקר של מיקרוסופט ואוניברסיטת קרנגי מלון הציגו מהדורת הניסיון הראשונה של ספריית הקריפטו של EverCrypt פותח במסגרת פרויקט האוורסט ובאמצעות שיטות מתמטיות לאימות אמינות פורמלי.

על יכולותיו וביצועיו, EverCrypt קרוב מאוד לספריות הצפנה הקיימות (OpenSSL) אך זה, בניגוד אליהם, מציע ערבויות נוספות לאמינות וביטחון.

לדוגמה: תהליך האימות מסתכם בהגדרת מפרטים מפורטים המתארים את כל התנהגויות התוכנית וההוכחה המתמטית שהקוד הכתוב עונה על מפרטים מוכנים.

בניגוד לשיטות בקרת איכות מבוססות ראיות, אימות מספק ערבויות אמינות שהתוכנית תפעל רק כפי שהתכוונו המפתחים ואין סוגים ספציפיים של שגיאות.

לדוגמא, עמידה במפרט מבטיח עבודה בטוחה עם הזיכרון והיעדר שגיאות המובילות להצפת מאגר, למצביעי הפרשות, לגישה לאזורי זיכרון שכבר שוחררו, או לשחרור כפול של חסימות זיכרון.

מה זה EverCrypt?

EverCrypt מספק בדיקת סוג וערך חזקה- רכיב לעולם לא יעביר פרמטרים לרכיב האחר שאינו תואם ולא יקבל גישה למצבים הפנימיים של הרכיבים האחרים.

התנהגות הקלט / הפלט תואם לחלוטין לפעולות פשוטות בתפקוד מתמטיקה, המוגדרים בסטנדרטים הצפנתיים.

כדי להגן מפני התקפות בערוצי צד שלישי, התנהגות במהלך חישובים (למשל, משך הביצוע או נוכחות הגישות לזיכרון מסוים) זה לא תלוי בנתונים הסודיים שעובדים.

קוד הפרויקט כתוב בשפה הפונקציונלית F * (כוכב F) , המספקת מערכת מסוגים ועידונים תלויים, המאפשרים לקבוע מפרט מדויק (מודל מתמטי) לתוכניות ולהבטיח את נכונותם והיעדרן של טעויות ביישום באמצעות נוסחאות SMT וכלי בדיקה עזר.

הקוד ב- F * מופץ תחת רישיון אפאצ'י 2.0, והמודולים הסופיים ב- C והמאסף תחת רישיון MIT.

בהתבסס על קוד ההתייחסות F *, assembler, C, OCaml, JavaScript נוצר וקוד הרכבת האינטרנט.

חלקים מסוימים של הקוד מוכן על ידי הפרויקט כבר משתמשים ב- Firefox, ליבת Windows , הבלוקצ'יין של Tezos ו- VPN Wireguard.

רכיבי EverCrypt

בעצם, EverCrypt משלב שני פרויקטים שונים בעבר מ- HACL * ו- Vale, מתן API מאוחד המבוסס עליהם והופך אותם למתאימים לשימוש בפרויקטים אמיתיים.

HACL * כתוב בשפה נמוכה* ומטרתה לספק פרימיטיבים קריפטוגרפיים לשימוש בתוכניות C ש הם משתמשים ב- APIs בסגנון libsodium ו- NaCL.

proyecto אל וייל פיתח שפה ספציפית דומיין ליצירת אימות במאסף.

כ -110 אלף שורות קוד HACL * בשפה נמוכה * ו -25 אלף שורות קוד עבור Vale משולבות והם נכתבו מחדש בכ -70 אלף שורות קוד בשפה האוניברסלית F *, שגם היא מפותחת כחלק מפרויקט האוורסט.

הגרסה הראשונה של ספריית EverCrypt כולל יישומים מאומתים מאלגוריתמי ההצפנה הבאים מוצע בגרסאות C או הרכבה (בעת השימוש ב-.

מתוכם הדברים הבאים בולטים בדף הפרויקט:

  • אלגוריתמי Hash: כל הגרסאות של SHA2, SHA3, SHA1 ו- MD5
  • קודי אימות: HMAC מעל SHA1, SHA2-256, SHA2-384 ו- SHA2-512 לאימות מקור נתונים
  • אלגוריתם של יצירת מפתח HKDF (תמצית והרחבה מבוססת HMAC המבוססת על HMAC)
  • הצפנת זרם ChaCha20 (גרסת C ללא אופטימיזציה זמינה)
  • אלגוריתם אימות הודעות Poly1305 (MAC) (גרסת C ומרכב)
  • פרוטוקול Diffie-Hellman על עקומות אליפטיות Curve25519 (גרסאות C ומרכב עם אופטימיזציות המבוססות על הוראות BMI2 ו- ADX)
  • חסום מצב צופן AEAD (צופן מאומת) ChachaPoly (גרסה C לא מותאמת)
  • מצב הצפנת בלוק AEAD AES-GCM (גרסת הרכבה עם אופטימיזציות AES-NI).

בראשון גרסת אלפא, אימות הקוד כבר הושלם בעיקר, אך עדיין ישנם אזורים שנחשפו.

בנוסף, API עדיין לא התייצב, שיורחב בגרסאות האלפא הבאות (מתוכנן לאחד מבנים עבור כל ממשקי ה- API.

בין הפגמים מודגשת גם תמיכה בארכיטקטורת x86_64 (בשלב הראשון, המטרה העיקרית היא אמינות, בעוד שמייצבים אופטימיזציה ופלטפורמות במקום השני).

מקור: https://jonathan.protzenko.fr


היה הראשון להגיב

השאירו את התגובה שלכם

כתובת הדוא"ל שלך לא תפורסם. שדות חובה מסומנים *

*

*

  1. אחראי לנתונים: מיגל אנחל גטון
  2. מטרת הנתונים: בקרת ספאם, ניהול תגובות.
  3. לגיטימציה: הסכמתך
  4. מסירת הנתונים: הנתונים לא יועברו לצדדים שלישיים אלא בהתחייבות חוקית.
  5. אחסון נתונים: מסד נתונים המתארח על ידי Occentus Networks (EU)
  6. זכויות: בכל עת תוכל להגביל, לשחזר ולמחוק את המידע שלך.