A leválasztott titkosítási architektúra formális ellenőrzése

A Princeton Egyetem, a Michigani Egyetem és a Lafayette College kutatói „Security Verification of Low-Trust Architectures” címmel jelentek meg egy műszaki dokumentumot.

Absztrakt:

„Az alacsony megbízhatóságú architektúrák a szoftver szempontjából mindig titkosított adatokon dolgoznak, és jelentősen csökkentik a hardveres megbízhatóságot egy kis, szoftvermentes enklávé komponensre. Ebben a cikkben egy speciális alacsony megbízhatóságú architektúra, a Sequestered Encryption (SE) architektúra teljes formális ellenőrzését hajtjuk végre, hogy megmutassuk, a tervezés biztonságos a közvetlen adatfelfedéssel és a digitális mellékcsatornákkal szemben minden lehetséges program esetében. Először meghatározzuk az alacsony megbízhatóságú SE architektúra ISA biztonsági követelményeit. Felfelé nézve ez az ISA a szoftver hardverének absztrakciójaként szolgál, és annak bemutatására szolgál, hogy az ezeket az utasításokat tartalmazó programok hogyan nem szivároghatnak ki információt, beleértve a digitális oldalcsatornákon keresztül is. Lefelé nézve ez az ISA a hardver specifikációja, és az ISA-szintű biztonsági követelményekből adódó bármely RTL implementáció bizonyítási kötelezettségeinek meghatározására szolgál. Ezek mind a funkcionális, mind a digitális oldalcsatornás szivárgásra vonatkoznak. Ezután bemutatjuk, hogyan lehet ezeket a bizonyítási kötelezettségeket sikeresen teljesíteni kereskedelmi formális ellenőrző eszközök segítségével. Bemutatjuk az RTL biztonsági ellenőrzési technikánk hatékonyságát az SE architektúra hét különböző helyes és hibás megvalósításához.”

Keresse meg a műszaki papír itt. Megjelent 2023. szeptember (előnyomat).

Tan, Qinhan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik és Todd Austin. „Az alacsony megbízhatóságú architektúrák biztonsági ellenőrzése.” arXiv preprint arXiv:2309.00181 (2023).

Kapcsolódó olvasás
A biztonság és biztonság ellenőrzése és tesztelése
A biztonságos és biztonságos rendszerek biztosítása érdekében a funkcionális ellenőrzést túlmutatják a lehetőségein. Új támogatás érkezik hardverből és szoftverből.
Új fogalmak szükségesek a biztonsági ellenőrzéshez
Miért olyan nehéz meggyőződni arról, hogy a hardver megfelelően működik, és képes észlelni a terepen esetlegesen felbukkanó sebezhetőségeket?

• SEO által támogatott tartalom és PR terjesztés. Erősödjön még ma.
• PlatoData.Network Vertical Generative Ai. Erősítse meg magát. Hozzáférés itt.
• PlatoAiStream. Web3 Intelligence. Felerősített tudás. Hozzáférés itt.
• PlatoESG. Autóipar / elektromos járművek, Carbon, CleanTech, Energia, Környezet, Nap, Hulladékgazdálkodás. Hozzáférés itt.
• PlatoHealth. Biotechnológiai és klinikai vizsgálatok intelligencia. Hozzáférés itt.
• ChartPrime. Emelje fel kereskedési játékát a ChartPrime segítségével. Hozzáférés itt.
• BlockOffsets. A környezetvédelmi ellentételezési tulajdon korszerűsítése. Hozzáférés itt.
• Forrás: https://semiengineering.com/formal-verification-of-a-sequestered-encryption-architecture/