ВАРИАНТ РЕАЛИЗАЦИИ ПРОЦЕДУРЫ АНАЛИЗА ИНФОРМАЦИОННЫХ ПОТОКОВ В ПРОГРАММНЫХ БЛОКАХ PL/SQL С ИСПОЛЬЗОВАНИЕМ ПЛАТФОРМЫ PLIF
- Авторы: Тимаков А.А.1
-
Учреждения:
- МИРЭА – Российский технологический университет
- Выпуск: № 4 (2023)
- Страницы: 39-57
- Раздел: ИНФОРМАЦИОННАЯ БЕЗОПАСНОСТЬ
- URL: https://journals.rcsi.science/0132-3474/article/view/137640
- DOI: https://doi.org/10.31857/S0132347423040118
- EDN: https://elibrary.ru/RDRCOC
- ID: 137640
Цитировать
Аннотация
Формальное доказательство эффективности реализуемых мер защиты и безопасности вычислений (обработки информации) является важнейшим условием доверия к критическим информационным системам. Важно понимать, что при построении таких систем формальная проверка безопасности должна применяться на всех инфраструктурных уровнях (от физического до прикладного). В настоящее время на практике проблемой остается формальная проверка безопасности вычислений на прикладном уровне, требующая сложной разметки элементов среды вычислений. Для решения данной задачи традиционно используются методы, в основе которых лежит контроль информационных потоков (КИП). В отличие от методов на основе управления доступом, нашедших широкое практическое применение в операционных системах (ОС) и системах управления базами данных (СУБД), КИП в программном обеспечении на практике применяется весьма ограниченно и в основном сводится к анализу помеченных данных – Taint Tracking. В работе приводится вариант реализации КИП в программных блоках PL/SQL с использованием платформы PLIF. Кроме того, описана общая схема проверки безопасности вычислений в приложениях уровня предприятия, работающих с реляционными базами данных. Преимуществом подхода можно считать явное разделение функций разработчиков программного обеспечения и аналитиков безопасности.
Об авторах
А. А. Тимаков
МИРЭА – Российский технологический университет
Автор, ответственный за переписку.
Email: timakov@mirea.ru
Россия, 119454, Москва, Проспект Вернадского, д. 78
Список литературы
- Latham D.C. Department of defense trusted computer system evaluation criteria // Department of Defense, 1986. T. 198.
- Infrastructure P.K., Profile T.P. Common criteria for information technology security evaluation // National Security Agency, 2002.
- Девянин П.Н., Леонова М.А. Применение подтипов и тотальных функций формального метода Event-B для описания и верификации МРОСЛ ДП-модели // Программная инженерия. 2020. Т. 11. № 4. С. 230–241.
- Тимаков А.А. Контроль информационных потоков в программных блоках баз данных на основе формальной верификации // Программирование. 2022. № 4. С. 27–49
- Denning E. Dorothy A lattice model of secure information flow // Communications of the ACM. 1976. № 5. P. 236–243.
- Шайтура С.В., Питкевич П.Н. Методы резервирования данных для критически важных информационных систем предприятия // Российский технологический журнал. 2022. Т. 10 (1). С. 28–34.
- Timakov A. PLIF. 2021. GitHub. https:// github.com/timimin/plif.
- 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.
- 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.
- 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.
- Broberg N. Thesis for the Degree of Doctor of Engineering Practical, Flexible Programming with Information Flow Control. 2011.
- Hedin Daniel, Sabelfeld Andrei A Perspective on Information-Flow Control // Software safety and securit. 2012. P. 319–347.
- 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.
- Fernandes A. tlaplus-graph-explorer. 2021. GitHub. https:// github.com/afonsonf/tlaplus-graph-explorer.
- Hedin Daniel, Sabelfeld Andrei A Perspective on Information-Flow Control // Software safety and security. 2012. P. 319–347.
- Kristensen E. CodeQL. 2022. GitHub. https:// github.com/github/codeql.
- 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.
- Harrison M.A ., Ruzzo W.L., Ullman J.D. Protection in operating systems // Communications of the ACM. 1976. V. 19. № 8. P. 461–471.