Učitavanje video playera...
01:15:57
Sophie Weber: Formalna verifikacija zaštite integriteta SEV-SNP tehnologije
Pojam formalne verifikacije obuhvaća modeliranje nekog sustava iz stvarnog svijeta jezikom simboličke logike te verifikaciju svojstava tog modela. Uvest ćemo pojam prepisivanja multiskupa (multiset rewriting) kao metodu formalne verifikacije te alat za automatsko dokazivanje Tamarin.
Definirat ćemo pojam pouzdane okoline za izvršavanje (trusted execution environment) i opisati AMD-ovu tehnologiju SEV-SNP kao jedan primjer ovakve okoline. Ovakva okolina koristi se u kontekstu izvršavanja programa na udaljenom računalu (npr. AWS, Azure, Google Colab i sl.) kada želimo osigurati tajnost i integritet podataka koje čuvamo i obrađujemo na udaljenom računalu.
Proći ćemo kroz modele (Paradžik et al., 2025. i Weber, 2025.) koji u Tamarinu modeliraju SEV-SNP platformu te provjeravaju sigurnosna svojstva vezana za SEV-SNP. Paradžik et al. (2025.) pronalazi 4 potencijalna napada vezana uz autentičnost podataka i sigurnost SEV-SNP platforme. Weber (2025.) dokazuje sva očekivana svojstva vezana za integritet memorije na platformi.
