Технология анализа безопасности информационных потоков в программном обеспечении, реализующем бизнес-логику с использованием хранимых программных блоков баз данных

Цели. Проверка свойств безопасности программного обеспечения (ПО) при построении информационных систем с высоким уровнем доверия, как правило, осуществляется с использованием инструментов динамического и статического анализа. Соответствующие виды анализа обычно не учитывают бизнес-логику ПО и не опираются на политику управления доступом к данным. Современным направлением решения проблемы является контроль информационных потоков. Несмотря на большое количество проведенных исследований, механизмы контроля информационных потоков в ПО пока не находят широкого применения на практике, поскольку обладают значительной сложностью и диктуют повышенные требования к разработчикам. Целью работы является перенос контроля информационных потоков с языкового уровня на уровень формальной верификации и выделение функции контроля целостности и конфиденциальности данных в ПО в самостоятельную задачу, решаемую аналитиками информационной безопасности.
Методы. Исследование опирается на общие формальные методы безопасности компьютерных систем и методы формальной верификации. Разработанный автором алгоритм проверки спецификаций использует аппарат темпоральной логики действий.
Результаты. Представлена технология, предполагающая поэтапное решение частных задач: проектирование базы данных (БД) для хранения и обработки подлежащей защите информации, анализ зависимостей и выделение релевантного множества программных блоков БД, генерация спецификаций TLA+ выделенных программных блоков БД, разметка спецификаций в соответствии с правилами глобальной политики безопасности и дополнительными ограничениями, применение алгоритма проверки спецификаций и устранение нарушений инварианта безопасности с внесением рекомендаций для разработчиков ПО, применение процедуры анализа помеченных данных для контроля распространения выходных значений верифицированных программных блоков БД во внешних программных модулях.
Выводы. Представленная технология не требует от разработчиков внесения избыточных аннотаций, описывающих правила политики безопасности. Функция анализа информационных потоков с привязкой к заданным в системе ограничениям доступа выносится на отдельный этап жизненного цикла разработки ПО. 

1. Девянин П.Н., Тележников В.Ю., Хорошилов А.В. Формирование методологии разработки безопасного системного программного обеспечения на примере операционных систем. Труды Института системного программирования РАН. 2021;33(5):25–40. https://doi.org/10.15514/ISPRAS-2021-33(5)-2

2. Timakov A.A. Information flow control in software DB units based on formal verification. Program. Comput. Soft. 2022;48(4):265–285. https://doi.org/10.1134/S0361768822040053

3. Hedin D., Sabelfeld A. A Perspective on Information-Flow Control. In: Software Safety and Security. 2012;33:319–347. https://doi.org/10.3233/978-1-61499-028-4-319

4. Kozyri E., Chong S., Myers A.C. Expressing Information Flow Properties. Foundations and Trends® in Privacy and Security. 2022;3(1):1–102. http://doi.org/10.1561/3300000008

5. Volpano D., Smith G. Probabilistic noninterference in a concurrent language. Journal of Computer Security (JCS). 1999;7(2):231–253. http://doi.org/10.3233/JCS-1999-72-305

6. Sabelfeld A., Sands D. Probabilistic noninterference for multi-threaded programs. In: Proceedings 13th IEEE Computer Security Foundations Workshop (CSFW-13). 2000. P. 200–214. https://doi.org/10.1109/CSFW.2000.856937

7. Askarov A., Chong S. Learning is Change in Knowledge: Knowledge-Based Security for Dynamic Policies. In: Proceedings 25th IEEE Computer Security Foundations Symposium (CSF 2012). 2012. P. 308–322. https://doi.org/10.1109/CSF.2012.31

8. Sutherland D. A model of information. In: Proceedings of the 9th National Security Conference. 1986. P. 175–183.

9. Volpano D., Irvine C., Smith G. Sound type system for secure flow analysis. Journal of Computer Security (JCS). 1996;4(2–3): 167–187.

10. Mantel H., Sudbrock H. Types vs. PDGs in information flow analysis. In: Albert E. (Ed.). Logic-Based Program Synthesis and Transformation. The 22nd International Symposium, LOPSTR 2012. Proceedings. Springer. 2012. Р. 106–121. https://doi.org/10.1007/978-3-642-38197-3_8

11. Myers A.C., Liskov B. A decentralized model for information flow control. ACM SIGOPS Operating Systems Review. 1997;5:129–142. https://doi.org/10.1145/268998.266669

12. Graf J., Hecker M., Mohr M., Snelting G. Checking applications using security APIs with JOANA. In: 8th International Workshop on Analysis of Security APIs. Proceedings. 2015. P. 118–129.

13. Broberg N., van Delft B., Sands D. Paragon for practical programming with information-flow control. In: Shan C. (Ed.). Programming Languages and Systems: The 11th Asian Symposium, APLAS 2013. Proceedings. Springer. 2013. Р. 217–232. https://doi.org/10.1007/978-3-319-03542-0_16

14. Clarkson M.R., Finkbeiner B., Koleini M., Micinski K.K., Rabe M.N., Sánchez C. Temporal logics for hyperproperties. In: Abadi M., Kremer S. (Eds.). Principles of Security and Trust: The Third International Conference, POST 2014. Proceedings. Berlin, Heidelberg: Springer; 2014. Р. 265–284. https://doi.org/10.1007/978-3-642-54792-8_15

15. Terauchi T., Aiken A. Secure information flow as a safety problem. In: Hankin C., Siveroni I. (Eds.). In: Static Analysis: The 12th International Static Symposium, SAS 2005. Proceedings. Berlin, Heidelberg: Springer. 2005. P. 352–367. https://doi.org/10.1007/11547662_24

16. Тимаков А.А. Вариант реализации процедуры анализа информационных потоков в программных блоках PL/SQL с использованием платформы PLIF. Программирование. 2023;4:39–57.

17. Broberg N., Sands D. Paralocks: Role based information flow control and beyond. In: Proceedings of the Conference Record of the Annual ACM Symposium on Principles of Programming Languages. 2010. P. 431–444. https://doi.org/10.1145/1706299.1706349

18. Sabelfeld A., Sands D. Declassification: Dimensions and principles. Journal of Computer Security (JCS). 2009;17(5):517–548. http://doi.org/10.3233/JCS-2009-0352

19. Youn D., Lee S., Ryu S. Declarative static analysis for multilingual programs using CodeQL. Software: Practice and Experience. 2023;53(7):1472–1495. https://doi.org/10.1002/spe.3199