Căile furtive explicite și implicite pentru a scurge sau compromite informații continuă să reprezinte o amenințare la adresa securității. Această lucrare prezintă o perfecționare a tehnicilor existente de urmărire a fluxului de informații la nivel de poartă (IFT) extinse la RTL, încurajând optimizarea securității în stadiu incipient. Paul Cunningham (Senior VP/GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, antreprenor, fost CTO Synopsys și acum Silvaco CTO) și continuăm seria noastră despre idei de cercetare. Ca întotdeauna, feedback binevenit.

Inovația

Alegerea din această lună este Înregistrați Urmărirea fluxului de informații la nivel de transfer pentru un design hardware sigur. Acest articol a apărut la DATE 2017 și a adunat 53 de citate impresionante. Autorii sunt de la Universitatea din California San Diego.

Acest grup a dezvoltat anterior tehnologia IFT la nivel de poartă (GLIFT), lansându-se ca produs sub Tortuga Logic (rebranded ulterior ca Cycuity). Tehnicile de flux de informații oferă o abordare mai generală și mai formală a modelării și raționamentului despre proprietățile de securitate decât testarea prin cazuri de utilizare a vulnerabilităților. Metoda se generalizează prin propagarea informațiilor de contaminare alături de evaluarea logică obișnuită, semnalând, să spunem, un semnal provenit dintr-un domeniu nesigur care controlează o selecție de condiții într-un domeniu securizat. Combinarea acestora cu metodele formale de verificare oferă potențialul de garanții puternice de securitate.

Extinderea analizei la RTL permite mai multe îmbunătățiri: scalabilitate la circuite mai mari, aplicare mai devreme în proiectare și o înțelegere oarecum îmbunătățită a dependențelor de nivel superior în intenția de proiectare, fără a fi nevoie de adnotări furnizate de utilizator. Autorii descriu, de asemenea, o metodă prin care designerii pot face un compromis între performanța de securitate și de verificare pentru a satisface nevoile diferite ale pieței.

punctul de vedere al lui Paul

Verificarea securității este ceva la care țin profund – nu putem avea încredere în datele digitale fără ea, iar acestea includ propriile mele date personale! Lucrarea din această lună este ușor de citit, evidențiind una dintre tehnicile principale în verificarea securității: adăugarea de biți „contaminați” (adică compromisi sau care nu mai sunt de încredere) la toate semnalele dintr-un proiect și îmbunătățirea modelelor de porți propagă biții contaminați prin porți, precum și valorile semnalului. .

Propagarea biților contaminați este conceptual aproape identică cu „propagarea X” în fluxurile principale de verificare a designului: dacă un semnal este contaminat, atunci este ca și cum nu îi cunoaștem valoarea, deoarece nu avem încredere în valoarea pe care o are.

Această lucrare propune două lucruri: în primul rând, adnotarea și propagarea biților contaminați la nivelul RTL, mai degrabă decât la nivelul porții; și în al doilea rând, să facem echivalentul a ceea ce instrumentele mainstream EDA numesc „eliminarea pesimismului X”. Acesta din urmă se referă la nu marcarea rezultatului unui operator ca X pur și simplu pentru că cel puțin una dintre intrările sale este X, ci mai degrabă la marcarea acestuia ca X numai dacă este cu adevărat X pe baza definiției acelui operator. De exemplu, luați în considerare c = a & b. Dacă a=0 atunci c=0 chiar dacă b este X. În mod echivalent, în verificarea securității vorbim, dacă a=0 și a nu este viciat, atunci c=0 și nu este viciat chiar dacă b este viciat. Pare ușor pentru „&”, devine puțin mai complicat pentru constructele if, else și case.

După cum vă puteți aștepta, lucrarea se încheie cu o analiză comparativă care arată clar că propagarea biților contaminați la RTL este mult mai rapidă decât la nivel de poartă și că propagarea „precisă” a biților contaminați (adică eliminarea pesimismului biților contaminați) reduce rata fals pozitive. pentru biți contaminați la ieșirile de proiectare cu un % semnificativ. Toată această evaluare comparativă se face într-un context de demonstrație formală, nu într-un context de simulare logică. Caz inchis.

Vă doresc tuturor Sărbători Fericite!

Viziunea lui Raul

Urmărirea fluxului de informații (IFT) este o tehnică de securitate computerizată care modelează modul în care informațiile se propagă pe măsură ce calculează un sistem. A fost introdus în anii 70 de către Denning, o introducere bună și un sondaj pot fi găsite aici. Ideea de bază este să etichetați datele cu o clasă de securitate și apoi să urmăriți aceste etichete pe măsură ce datele sunt utilizate pentru calcule. În scopul lucrării revizuite, eticheta este doar un pic care indică faptul că datele sunt „altera” (etichetă=1, de încredere). Cea mai conservatoare abordare în utilizarea acestei etichete este că rezultatul oricărei operațiuni care implică altera datele sunt altera; sau spus invers, numai operațiunile cu toate datele de intrare fiind nu pata randament a nu pata ieșire. Lucrarea relaxează cumva această abordare, așa cum voi explica mai târziu.

Securitatea computerelor vizează menținerea informațiilor confidențialitate și integritate. Confidențialitatea înseamnă că informațiile sunt dezvăluite numai entităților autorizate. IFT verifică dacă informațiile secrete pot fi vreodată dezvăluite, urmărind că toate locațiile către care circulă sunt și secrete (nu pata), de exemplu, o cheie secretă nu se scurge în afara unui spațiu de memorie restricționat. Integritatea este invers: pentru a menține acuratețea și consistența datelor, entităților care nu au încredere nu au voie să opereze pe informații de încredere. Modul în care informațiile circulă într-un sistem de calcul este crucial pentru a determina confidențialitatea și integritatea. IFT este printre cele mai utilizate tehnici de modelare și raționament despre securitate.

Lucrarea analizează abordările IFT existente la nivel de poartă și RTL. La nivelul porții, reconvergența este o sursă de imprecizie. Într-un multiplexor, un semnal de selectare a pată va produce a altera ieșire chiar dacă ambele intrări sunt nu pata. Modelarea unui multiplexor la nivel RTL permite remedierea acestui lucru. Abordările existente la nivel RTL implică necesitatea modificării codului RTL. Sistemul implementat de autori, RTLIFT, remediază ambele deficiențe de mai sus. Oferă o bibliotecă de operatori RTL care permite implementarea diferitelor abordări ale IFT, cum ar fi influențarea ieșirilor dacă orice intrare este altera (conservatoare) sau o abordare mai nuanțată, cum ar fi afectarea ieșirilor pentru un multiplexor numai dacă una dintre intrările de date este altera (evită fals pozitive). De asemenea, oferă o traducere automată a unui design RTL în Verilog într-o versiune îmbunătățită IFT, care poate fi utilizată în scopuri de verificare.

Rezultatele privind nucleele criptografice arată că RTLIFT este de aproximativ 5 ori mai rapid decât IFT la nivel de poartă (GLIFT). Pe o colecție de 8 sumatori, multiplicatori și logica căii de control, RTLIFT arată o scădere cu 5%-37% a rezultatelor false pozitive (false altera) peste GLIFT pentru o simulare de 2²⁰ mostre aleatorii de intrare.

O lucrare cuprinzătoare despre securitate, care extinde IFT la RTL, o lectură foarte plăcută!

Distribuie această postare prin:

• Distribuție de conținut bazat pe SEO și PR. Amplifică-te astăzi.
• PlatoData.Network Vertical Generative Ai. Împuterniciți-vă. Accesați Aici.
• PlatoAiStream. Web3 Intelligence. Cunoștințe amplificate. Accesați Aici.
• PlatoESG. carbon, CleanTech, Energie, Mediu inconjurator, Solar, Managementul deșeurilor. Accesați Aici.
• PlatoHealth. Biotehnologie și Inteligență pentru studii clinice. Accesați Aici.
• Sursa: https://semiwiki.com/eda/339962-information-flow-tracking-at-rtl-innovation-in-verification/