Використання системи формальної логіки PVS в методі формального доведення захищеності при побудові систем захисту інформації
DOI:
https://doi.org/10.15587/2706-5448.2021.229539Ключові слова:
інформаційно-телекомунікаційна система, система захисту інформації, політика безпеки, метод формального доведення захищеності, мова специфікаціїАнотація
Об’єктом дослідження є інформаційно-телекомунікаційна система (ІТС) та забезпечення захисту інформації, що зберігається, обробляється та циркулює в ній. Одним з найбільш проблемних місць при створенні захищених ІТС є логічна суперечливість і неповнота політики безпеки інформації. Тобто набору законів, правил, обмежень, рекомендацій та ін., які регламентують порядок обробки інформації та спрямовані на захист інформації від визначеної множини загроз. Підставою для таких проблем зазвичай є відсутність передпроєктного моделювання системи захисту інформації як складової інформаційно-телекомунікаційної системи, що врешті спричиняє вразливість останньої.
Важливою передумовою створення захищеної ІТС є побудова суб’єктно-об’єктної моделі системи, що дозволяє визначити зв’язки між об’єктами, їх особливості, змоделювати інформаційні потоки та різновиди доступів до інформаційних та інфраструктурних ресурсів. За наявної чіткої, повної та несуперечливої суб’єктно-об’єктної моделі ІТС стає можливим застосування математичних методів до моделювання процесів її функціонування, в тому числі і для вирішення задачі формального доведення захищеності.
В роботі розглянуто основну ідею методу формального доведення захищеності, який може використовуватися при побудові систем захисту інформації або оцінці захищеності створеної інформаційно-телекомунікаційної системи. Показано, що для його реалізації можливе застосування методології автоматичного доведення теорем. Одним із шляхів вирішення цієї задачі, що пропонується в роботі, є використання системи формальної логіки PVS (Prototype Verification System), яка широко застосовується для написання специфікацій та конструювання доведень. Розглянуто основні складові цієї системи, а також можливості її використання для автоматичного доведення тверджень про неможливість несанкціонованого доступу в умовах визначеної політики безпеки. Наведено приклад застосування системи PVS для формального доведення захищеності системи в рамках політики безпеки Белла-ЛаПадула.
Посилання
- Antoniuk, A. A., Zhora, V. V. (2005). Obobshchenye modely uhroz v ynformatsyonno-telekommunykatsyonnoi systeme. Pravove, normatyvne ta metrolohichne zabezpechennia systemy zakhystu informatsii v Ukraini, 11, 50–54.
- Glushkov, V. M. (1980). Sistema avtomatizatsii dokazatelstv. Avtomatizatsiia obrabotki matematicheskikh tekstov. Kyiv: IK AN USSR, 3–30.
- Bishop, M. (2018). Computer Security Art and Science. Addison Wesley Professional, 2865.
- Owre, S., Shankar, N., Rushby, J. M., Stringer-Calvert, D. W. J. (2020). PVS System Guide Version 7.1. SRI International. Available at: https://pvs.csl.sri.com/doc/pvs-system-guide.pdf
- Owre, S., Shankar, N. Rushby, J. M., Stringer-Calvert, D. W. J. (2020). PVS Language Reference Version 7.1. SRI International. Available at: https://pvs.csl.sri.com/doc/pvs-language-reference.pdf
- Owre, S., Shankar, N., Rushby, J. M., Stringer-Calvert, D. W. J. (2020). PVS Prover Guide Version 7.1. SRI International. Available at: https://pvs.csl.sri.com/doc/pvs-prover-guide.pdf
- Antoniuk, A. O., Zhora, V. V. (2007). Vikoristannia dokazovogo metodu dlia proektuvannia ta otsіnki rіvnia zakhischenostі іnformatsіino-telekomunіkatsіinoї sistemi. Problemi programuvannia, 3, 88–96.
- Muñoz, C. A., Demasi, R. A.; Meyer, B., Nordio, M. (Eds.) (2012). Advanced Theorem Proving Techniques in PVS and Applications. Tools for Practical Software Verification. LASER 2011. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 7682. doi: http://doi.org/10.1007/978-3-642-35746-6_4
- McGuinness, D. L.; Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., Patel-Schneider, P. F. (Eds.) (2010). The Description Logic Handbook. Theory, Implementation and Applications. Cambridge: University Press, 624. doi: http://doi.org/10.1017/cbo9780511711787
- Turhan, A. Y.; Rudolph, S., Gottlob, G., Horrocks, I., van Harmelen, F. (Eds.) (2013). Introductions to Description Logics – A Guided Tour. Reasoning Web. Semantic Technologies for Intelligent Data Access. Reasoning Web 2013. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, 8067. doi: http://doi.org/10.1007/978-3-642-39784-4_3
- Bell, D. E., La Padula, L. J. (1976). Secure Computer Systems: Mathematical foundations and model. Report ESD-TR-73-278. Mitre Corp. Bedford. Available at: http://www-personal.umich.edu/~cja/LPS12b/refs/belllapadula1.pdf
##submission.downloads##
Опубліковано
Як цитувати
Номер
Розділ
Ліцензія
Авторське право (c) 2021 Віктор Володимирович Жора, Олександр Борисович Синецький
Ця робота ліцензується відповідно до Creative Commons Attribution 4.0 International License.
Закріплення та умови передачі авторських прав (ідентифікація авторства) здійснюється у Ліцензійному договорі. Зокрема, автори залишають за собою право на авторство свого рукопису та передають журналу право першої публікації цієї роботи на умовах ліцензії Creative Commons CC BY. При цьому вони мають право укладати самостійно додаткові угоди, що стосуються неексклюзивного поширення роботи у тому вигляді, в якому вона була опублікована цим журналом, але за умови збереження посилання на першу публікацію статті в цьому журналі.
