Printsiplar, siyosatlar va himoya Dasturiy ta'minot xavfsizligi

bekor
func(int a,
int
b,
int
c) { 2
int
x = 0, y
= 0, z = 0; 3 ,
agar
(a) x = -2; 4
agar
(b < 5)
{ agar (!a && c) y = 1; z = 2;
6 Mudofaa strategiyasi
8 assert(x + y + z != 3); 9 }
7
5
6
Yo'l sharti - bu barcha tarmoq qarorlarini (hozircha) kodlaydigan ramziy
kirishlar ustidagi kvantifikatorsiz formuladir . Yo'lni amalga oshirish
mumkin yoki yo'qligini aniqlash uchun ramziy ijro mexanizmi yo'l
holatining qoniqtirilishini tekshiradi. Cheklovlar to'plamini hisobga olgan
holda, SMT hal qiluvchi qoniqarli topshiriq, hisoblagich misoli yoki vaqt
tugashini ta'minlaydi.
Ramziy bajarilish dasturdagi barcha yo‘llarni aniq baholash imkonini
bersa-da , cheksiz bajarilish izlariga olib keladigan tsikllar va rekursiyalar
bilan bog‘liq qiyinchiliklarga duch keladi. Yo'l portlashi yana bir
qiyinchilikdir, chunki har bir filial kuzatilgan yo'llar va holat sonini ikki
baravar oshiradi . Atrof-muhitni modellashtirish, masalan, tizim
qo'ng'iroqlari orqali ham modellashtirish kerak bo'lgan operatsion tizim
holati miqdori tufayli murakkab . Nihoyat, massiv ma'lumotlari ham,
indeks ham ramziy bo'lgan ramziy ma'lumotlar qiyin , chunki ixtiyoriy
ma'lumotlar mumkin bo'lgan echimlar sonini oshiradi.
Machine Translated by Google

---

!a0 && c0
y=1 z=2
Shart: !a0
&& b0 >= 5
Shart :
a0
&& b0 < 5
&& !(!a0 && c0) Shart: !a0 && b0
< 5 && !a0 &&
c0
buzilishi!
imkonsiz!
Vaziyat: !a0
&& b0 < 5 && !
(!a0 && c0)
!a0 && c0
y=1 z=2
x=0, y=0, z=0
Vaziyat: a0