Printsiplar, siyosatlar va himoya Dasturiy ta'minot xavfsizligi

6.1 Dasturiy ta'minotni tekshirish
Dasturiy ta'minotni tekshirish berilgan spetsifikatsiyaga
muvofiq kodning to'g'riligini tasdiqlaydi . Xavfsizlik cheklovlari
(masalan, xotira yoki turdagi xavfsizlik buzilishi) kodlangan
va tekshirish jarayoniga konfiguratsiya sifatida berilgan.
Cheklangan modelni tekshirish yoki mavhum talqin kabi
rasmiy tekshirishning turli shakllari mavjud . Ularning barchasi
berilgan kod qismi rasmiy spetsifikatsiyaga mos kelishini
isbotlaydi va xavfsizlik siyosatini buzish mumkin emasligini kafolatlaydi.
Rasmiy tasdiqlangan kodning ba'zi taniqli misollari seL4 [14],
rasmiy tasdiqlangan operatsion tizim yadrosi yoki CompCert.
58
Dasturiy ta'minotning zaifliklaridan himoya qilish to'rtta o'lchov
bo'yicha mumkin: (i) kodning xatosizligini kafolatlaydigan dasturiy
ta'minotning to'g'riligini rasman isbotlash (ma'lum bir
spetsifikatsiyaga muvofiq), (ii) dasturiy ta'minotni xavfsiz dasturlash
tilida qayta yozish, (iii) dasturiy ta'minot Dasturiy ta'minotning
kamchiliklarini zarar yetkazishidan oldin aniqlaydigan sinovlar va
(iv) tuzatilmagan yoki noma'lum zaifliklar mavjud bo'lganda tizimni
himoya qiladigan yumshatishlar.
6 Mudofaa strategiyasi
Machine Translated by Google

---

Dasturiy ta'minotni tekshirishning asosiy muammosi miqyoslilikdir.
Avtomatik dasturiy ta'minotni tekshirish kodning chiziqli o'sishi bilan
tekshirish narxining eksponentsial o'sishi bilan 100 qator kodlargacha
o'lchaydi . Misol tariqasida, seL4 yadrosini tekshirishni inson tomonidan
tekshirish bir necha yilga to'g'ri keladi.
[19], rasmiy tasdiqlangan kompilyator. seL4 uchun operatsion tizim
tushunchalari isbot tizimi ustidagi yuqori darajadagi siyosatlar sifatida
kodlangan . Yuqori darajadagi operatsion tizim siyosatining to'g'riligini
isbotlagandan so'ng , ikkinchi bosqichda yuqori darajadagi siyosat va
past darajadagi amalga oshirish o'rtasidagi ekvivalentlik isbotlanadi.
CompCert uchun kompilyatorning individual qadamlari va o'zgarishlari
to'g'ri ekanligi isbotlangan. Bu tekshirilgan kompilyator o'zgarishlari
har doim to'g'ri bo'lishini kafolatlaydi va kompilyatsiya jarayonining bir
qismi sifatida hech qanday xatolikka yo'l qo'ymaydi.