אימות פורמלי של ארכיטקטורת הצפנה מסודרת

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

תקציר:

"ארכיטקטורות עם אמון נמוך עובדות על, מנקודת המבט של תוכנה, נתונים מוצפנים תמיד, ומפחיתות משמעותית את כמות אמון החומרה לרכיב מובלעת קטן ללא תוכנה. במאמר זה, אנו מבצעים אימות פורמלי מלא של ארכיטקטורת אמון ספציפית, ארכיטקטורת Sequestered Encryption (SE), כדי להראות שהעיצוב מאובטח מפני חשיפה ישירה של נתונים וערוצים צדדיים דיגיטליים עבור כל התוכניות האפשריות. ראשית, אנו מגדירים את דרישות האבטחה של ארכיטקטורת ISA of SE עם אמון נמוך. במבט כלפי מעלה, ISA זה משמש כהפשטה של ​​החומרה עבור התוכנה, ומשמש כדי להראות כיצד כל תוכנה הכוללת הוראות אלו אינה יכולה לדלוף מידע, כולל דרך ערוצי צד דיגיטליים. במבט כלפי מטה, ISA זה הוא מפרט לחומרה, ומשמש להגדרת חובות ההוכחה לכל מימוש RTL הנובע מדרישות האבטחה ברמת ה-ISA. אלה מכסים גם דליפה פונקציונלית וגם דיגיטלית של ערוץ צדדי. לאחר מכן, אנו מראים כיצד ניתן למלא את חובות ההוכחה הללו בהצלחה באמצעות כלי אימות פורמליים מסחריים. אנו מדגימים את היעילות של טכניקת אימות האבטחה RTL שלנו עבור שבעה יישומים נכונים וטעים שונים של ארכיטקטורת SE."

מצא נייר טכני כאן. פורסם בספטמבר 2023 (הדפסה מוקדמת).

טאן, צ'ינהאן, יונתן פישה, שיבו צ'ן, לורן בינרקי, ז'אן-בטיסט ג'נין, שראד מאליק וטוד אוסטין. "אימות אבטחה של ארכיטקטורות בעלות אמון נמוך." arXiv preprint arXiv:2309.00181 (2023).

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

• הפצת תוכן ויחסי ציבור מופעל על ידי SEO. קבל הגברה היום.
• PlatoData.Network Vertical Generative Ai. העצים את עצמך. גישה כאן.
• PlatoAiStream. Web3 Intelligence. הידע מוגבר. גישה כאן.
• PlatoESG. רכב / רכבים חשמליים, פחמן, קלינטק, אנרגיה, סביבה, שמש, ניהול פסולת. גישה כאן.
• PlatoHealth. מודיעין ביוטכנולוגיה וניסויים קליניים. גישה כאן.
• ChartPrime. הרם את משחק המסחר שלך עם ChartPrime. גישה כאן.
• BlockOffsets. מודרניזציה של בעלות על קיזוז סביבתי. גישה כאן.
• מקור: https://semiengineering.com/formal-verification-of-a-sequestered-encryption-architecture/