Na Seminaru za matematičku logiku i računarstvo, u ponedjeljak 9. veljače 2026. u 17:15 sati, u predavaonici 105, PMF-MO, 

Sophie Weber (PMF-MO) održat će predavanje 

 

Formalna verifikacija zaštite integriteta SEV-SNP tehnologije

 

Sažetak: 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.

 

Link za Zoom prijenos: https://zoom.us/j/93216379543?pwd=puZs1L9Gjc7U2dwVG6pI5aFeMe2xw0.1
(Meeting ID: 932 1637 9543  )