Expliciete en impliciete sluippaden om informatie te lekken of in gevaar te brengen, blijven een bedreiging voor de veiligheid vormen. In dit artikel wordt gekeken naar een verfijning van de bestaande gate-level information flow tracking (IFT)-technieken, uitgebreid naar RTL, waardoor beveiligingsoptimalisatie in een vroeg stadium wordt aangemoedigd. Paul Cunningham (Senior VP/GM, Verification bij Cadence), Raúl Camposano (Silicon Catalyst, ondernemer, voormalig CTO van Synopsys en nu CTO van Silvaco) en ik vervolgen onze serie over onderzoeksideeën. Zoals altijd: feedback welkom.
De innovatie
De keuze van deze maand is Registreer informatiestroom op overdrachtsniveau voor aantoonbaar veilig hardwareontwerp. Dit artikel verscheen op DATE 2017 en heeft maar liefst 53 citaten verzameld. De auteurs zijn afkomstig van de Universiteit van Californië in San Diego.
Deze groep ontwikkelde eerder gate-level IFT (GLIFT) -technologie en werd gelanceerd als een product onder Tortuga Logic (later omgedoopt tot Cycuity). Informatiestroomtechnieken bieden een meer algemene en formele benadering voor het modelleren en redeneren over beveiligingseigenschappen dan het testen op basis van gebruiksscenario's voor kwetsbaarheden. De methode generaliseert door besmettingsinformatie te verspreiden naast reguliere logische evaluatie, waarbij bijvoorbeeld een signaal wordt gemarkeerd dat afkomstig is van een onveilig domein en dat een voorwaardeselectie in een beveiligd domein bestuurt. De combinatie hiervan met formele verificatiemethoden biedt mogelijkheden voor sterke veiligheidsgaranties.
Het uitbreiden van de analyse naar RTL maakt verschillende verbeteringen mogelijk: schaalbaarheid naar grotere circuits, toepassing eerder in het ontwerp en een enigszins verbeterd begrip van afhankelijkheden op een hoger niveau in de ontwerpintenties zonder de noodzaak van door de gebruiker aangeleverde annotaties. De auteurs beschrijven ook een methode waarmee ontwerpers een afweging kunnen maken tussen beveiligings- en verificatieprestaties om aan verschillende marktbehoeften te voldoen.
De mening van Paul
Beveiligingsverificatie is iets waar ik veel waarde aan hecht – zonder digitale gegevens kunnen we niet vertrouwen, en dit geldt ook voor mijn eigen persoonlijke gegevens! Het artikel van deze maand is gemakkelijk te lezen en benadrukt een van de meest voorkomende technieken bij beveiligingsverificatie: het toevoegen van “besmette” (d.w.z. gecompromitteerde of niet langer vertrouwde) bits aan alle signalen in een ontwerp en het verbeteren van poortmodellen, propageren besmette bits door poorten, evenals signaalwaarden .
De voortplanting van besmette bits is conceptueel bijna identiek aan “X-propagatie” in reguliere ontwerpverificatiestromen: als een signaal besmet is, is het alsof we de waarde ervan niet kennen, omdat we de waarde die het heeft niet vertrouwen.
Dit artikel stelt twee dingen voor: ten eerste, het uitvoeren van annotatie en propagatie van besmette bits op RTL-niveau in plaats van op poortniveau; en ten tweede, het equivalent doen van wat reguliere EDA-instrumenten ‘verwijdering van het X-pessimisme’ noemen. Dit laatste verwijst naar het niet markeren van het resultaat van een operator als X simpelweg omdat ten minste één van zijn invoer X is, maar om het resultaat alleen als X te markeren als het werkelijk X is, gebaseerd op de definitie van die operator. Beschouw bijvoorbeeld c = a & b. Als a=0, dan is c=0, zelfs als b X is. Op dezelfde manier kun je bij veiligheidsverificatie zeggen: als a=0 en a niet besmet is, dan is c=0 en is het niet besmet, zelfs als b wel besmet is. Lijkt gemakkelijk voor “&”, wordt een beetje lastiger voor if, else en case-constructies.
Zoals je kunt verwachten, besluit het artikel met een aantal benchmarks waaruit duidelijk blijkt dat het verspreiden van besmette bits bij RTL veel sneller gaat dan op poortniveau, en dat “precieze” voortplanting van besmette bits (dat wil zeggen het verwijderen van besmette bitspessimisme) het aantal vals-positieve resultaten vermindert. voor besmette bits bij ontwerpuitgangen met een aanzienlijk percentage. Al deze benchmarking wordt gedaan in een formele bewijscontext, niet in een logische simulatiecontext. Zaak gesloten.
Wens jullie allemaal fijne feestdagen!
De mening van Raúl
Information Flow Tracking (IFT) is een computerbeveiligingstechniek die modelleert hoe informatie zich voortplant terwijl een systeem werkt. Het werd in de jaren 70 geïntroduceerd door Denning, er is een goede introductie en overzicht te vinden hier. Het basisidee is om gegevens te labelen met een beveiligingsklasse en deze labels vervolgens bij te houden terwijl de gegevens worden gebruikt voor berekeningen. Voor de doeleinden van het beoordeelde artikel geeft het label slechts een beetje aan dat de gegevens “smet” (label=1, niet vertrouwd). De meest conservatieve benadering bij het gebruik van dit label is dat de uitvoer van elke bewerking wordt betrokken smet gegevens zijn smet; of omgekeerd: alleen bewerkingen waarbij alle invoergegevens aanwezig zijn niet bederven opbrengst a niet bederven uitgang. Het artikel versoepelt deze aanpak op de een of andere manier, zoals ik later zal uitleggen.
Computerbeveiliging is gericht op het behouden van informatie vertrouwelijkheid en integriteit. Vertrouwelijkheid betekent dat informatie alleen wordt bekendgemaakt aan bevoegde entiteiten. IFT verifieert of geheime informatie ooit kan worden onthuld door bij te houden dat alle locaties waar de informatie naartoe stroomt ook geheim zijn (niet bederven), een geheime sleutel lekt bijvoorbeeld niet buiten een beperkte geheugenruimte. Integriteit is het omgekeerde: om de nauwkeurigheid en consistentie van gegevens te behouden, mogen niet-vertrouwde entiteiten niet met vertrouwde informatie werken. De manier waarop informatie door een computersysteem stroomt, is van cruciaal belang om de vertrouwelijkheid en integriteit te bepalen. IFT is een van de meest gebruikte technieken voor het modelleren en redeneren over beveiliging.
Het artikel bespreekt bestaande IFT-benaderingen op poortniveau en RTL-niveau. Op poortniveau is reconvergentie een bron van onnauwkeurigheid. In een multiplexer zal een kleurselectiesignaal a opleveren smet uitvoer, zelfs als beide ingangen dat zijn niet bederven. Door een multiplexer op RTL-niveau te modelleren, kan dit worden opgelost. Bestaande benaderingen op RTL-niveau brengen de noodzaak met zich mee om de RTL-code te wijzigen. Het door de auteurs geïmplementeerde systeem, RTLIFT, verhelpt beide bovenstaande tekortkomingen. Het biedt een bibliotheek met RTL-operators waarmee verschillende benaderingen van IFT kunnen worden geïmplementeerd, zoals het bederven van de output als er input is. smet (conservatief) of een meer genuanceerde benadering, zoals het alleen bederven van uitgangen voor een multiplexer als een van de data-ingangen smet (voorkomt valse positieven). Het biedt ook een automatische vertaling van een RTL-ontwerp in Verilog naar een IFT-verbeterde versie die kan worden gebruikt voor verificatiedoeleinden.
De resultaten op cryptografische kernen laten zien dat RTLIFT ongeveer 5 keer sneller is dan IFT op poortniveau (GLIFT). Op een verzameling van 8 optellers, vermenigvuldigers en controlepadlogica laat RTLIFT een afname van 5% -37% zien in valse positieven (valse positieven). smet) over GLIFT voor een simulatie van 220 willekeurige invoermonsters.
Een uitgebreid artikel over beveiliging, dat IFT uitbreidt naar RTL, heel plezierig om te lezen!
Deel dit bericht via:
- Door SEO aangedreven content en PR-distributie. Word vandaag nog versterkt.
- PlatoData.Network Verticale generatieve AI. Versterk jezelf. Toegang hier.
- PlatoAiStream. Web3-intelligentie. Kennis versterkt. Toegang hier.
- PlatoESG. carbon, CleanTech, Energie, Milieu, Zonne, Afvalbeheer. Toegang hier.
- Plato Gezondheid. Intelligentie op het gebied van biotech en klinische proeven. Toegang hier.
- Bron: https://semiwiki.com/eda/339962-information-flow-tracking-at-rtl-innovation-in-verification/
