- Код статьи
- 10.31857/S0132347423040118-1
- DOI
- 10.31857/S0132347423040118
- Тип публикации
- Статус публикации
- Опубликовано
- Авторы
- Том/ Выпуск
- Том / Номер выпуска 4
- Страницы
- 39-57
- Аннотация
- Формальное доказательство эффективности реализуемых мер защиты и безопасности вычислений (обработки информации) является важнейшим условием доверия к критическим информационным системам. Важно понимать, что при построении таких систем формальная проверка безопасности должна применяться на всех инфраструктурных уровнях (от физического до прикладного). В настоящее время на практике проблемой остается формальная проверка безопасности вычислений на прикладном уровне, требующая сложной разметки элементов среды вычислений. Для решения данной задачи традиционно используются методы, в основе которых лежит контроль информационных потоков (КИП). В отличие от методов на основе управления доступом, нашедших широкое практическое применение в операционных системах (ОС) и системах управления базами данных (СУБД), КИП в программном обеспечении на практике применяется весьма ограниченно и в основном сводится к анализу помеченных данных – Taint Tracking. В работе приводится вариант реализации КИП в программных блоках PL/SQL с использованием платформы PLIF. Кроме того, описана общая схема проверки безопасности вычислений в приложениях уровня предприятия, работающих с реляционными базами данных. Преимуществом подхода можно считать явное разделение функций разработчиков программного обеспечения и аналитиков безопасности.
- Ключевые слова
- Дата публикации
- 17.09.2025
- Год выхода
- 2025
- Всего подписок
- 0
- Всего просмотров
- 18
Библиография
- 1. Latham D.C. Department of defense trusted computer system evaluation criteria // Department of Defense, 1986. T. 198.
- 2. Infrastructure P.K., Profile T.P. Common criteria for information technology security evaluation // National Security Agency, 2002.
- 3. Девянин П.Н., Леонова М.А. Применение подтипов и тотальных функций формального метода Event-B для описания и верификации МРОСЛ ДП-модели // Программная инженерия. 2020. Т. 11. № 4. С. 230–241.
- 4. Тимаков А.А. Контроль информационных потоков в программных блоках баз данных на основе формальной верификации // Программирование. 2022. № 4. С. 27–49
- 5. Denning E. Dorothy A lattice model of secure information flow // Communications of the ACM. 1976. № 5. P. 236–243.
- 6. Шайтура С.В., Питкевич П.Н. Методы резервирования данных для критически важных информационных систем предприятия // Российский технологический журнал. 2022. Т. 10 (1). С. 28–34.
- 7. Timakov A. PLIF. 2021. GitHub. https:// github.com/timimin/plif.
- 8. Konnov I., Kukovec J., Tran T.-H. TLA+ model checking made symbolic // Proceedings of the ACM on Programming Languages. 2019. V. 3. OOPSLA. P. 1–30.
- 9. Broberg Niklas, Sands David Paralocks: Role-based information flow control and beyond // Conference Record of the Annual ACM Symposium on Principles of Programming Languages. 2010. P. 431–444.
- 10. Broberg Niklas, Sands David Flow locks: Towards a core calculus for dynamic flow policies // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2006. No March. P. 180–196.
- 11. Broberg N. Thesis for the Degree of Doctor of Engineering Practical, Flexible Programming with Information Flow Control. 2011.
- 12. Hedin Daniel, Sabelfeld Andrei A Perspective on Information-Flow Control // Software safety and securit. 2012. P. 319–347.
- 13. Methni A., Lemerre M., Hedia B.B., Barkaoui K., Haddad S. An Approach for Verifying Concurrent C Programs // 8th Junior Researcher Workshop on Real-Time Computing. 2014. P. 33–36.
- 14. Fernandes A. tlaplus-graph-explorer. 2021. GitHub. https:// github.com/afonsonf/tlaplus-graph-explorer.
- 15. Hedin Daniel, Sabelfeld Andrei A Perspective on Information-Flow Control // Software safety and security. 2012. P. 319–347.
- 16. Kristensen E. CodeQL. 2022. GitHub. https:// github.com/github/codeql.
- 17. V. Delfit, Broberg Niklas, Sands David A Datalog semantics for Paralocks // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2013. P. 305–320.
- 18. Harrison M.A ., Ruzzo W.L., Ullman J.D. Protection in operating systems // Communications of the ACM. 1976. V. 19. № 8. P. 461–471.
