mireabulletinRussian Technological JournalRussian Technological Journal2782-32102500-316XRTU MIREA10.32362/2500-316X-2024-12-2-16-27mireabulletin-877Research ArticleИНФОРМАЦИОННЫЕ СИСТЕМЫ. ИНФОРМАТИКА. ПРОБЛЕМЫ ИНФОРМАЦИОННОЙ БЕЗОПАСНОСТИINFORMATION SYSTEMS. COMPUTER SCIENCES. ISSUES OF INFORMATION SECURITYТехнология анализа безопасности информационных потоков в программном обеспечении, реализующем бизнес-логику с использованием хранимых программных блоков баз данныхAnalysis of information flow security using software implementing business logic based on stored database program blockshttps://orcid.org/0000-0003-4306-789XТимаковА. А.TimakovA. А.

Тимаков Алексей Анатольевич, к.т.н., доцент, доцент кафедры информационной безопасности, Институт искусственного интеллекта

119454, Москва, пр-т Вернадского, д. 78

Scopus Author ID 57809572100

 

Aleksey A. Timakov, Cand. Sci. (Eng.), Associate Professor, Department of Information Security, Institute of Artificial Intelligence

78, Vernadskogo pr., Moscow, 119454

timakov@mirea.ruФГБОУ ВО «МИРЭА – Российский технологический университет»РоссияMIREA – Russian Technological UniversityRussian Federation20240504202412216–27Copyright © Тимаков А.А., 20242024Тимаков А.А.Timakov A.А.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.rtj-mirea.ru/jour/article/view/877

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

Objectives. Verification of software security is typically performed using dynamic and static analysis tools. The corresponding types of analysis do not usually consider the business logic of the software and do not rely on data access control policies. A modern approach to resolving this problem is to implement language-based information flow control. Despite a large amount of research, mechanisms for information flow control in software are not widely used in practice. This is because they are complex and impose increased demands on developers. The aim of the work is to transfer information flow control from the language level to the level of formal verification. This will enable the functions of controlling data integrity and confidentiality in software to be isolated into a separate task, which can be resolved by information security analysts.Methods. The research is based on general formal security methods for computer systems and formal verification methods. The algorithm developed by the author for checking security specifications and resolving security violations uses temporal logic of actions.Results. The technology is presented as a step-by-step approach to resolving specific tasks, including the following: designing a database (DB) for storing and processing sensitive information; analyzing dependencies and identifying relevant sets of program blocks in the DB; generating TLA+ specifications for the identified program blocks; labeling specifications according to global security policy rules and additional constraints; applying the specification verification algorithm, and resolving security violations while providing recommendations for software developers. The procedure also involves analyzing labeled data, in order to control the spread of verified program block output values in external software modules.Conclusions. The technology presented herein does not require developers to include redundant annotations describing security policy rules. The function of analyzing information flows with reference to predefined access restrictions is moved to a separate stage of the software development life cycle.

информационные потокиконтроль информационных потоковформальная верификацияязыковая платформаполитика безопасностиабстрактная семантикаинформационное невлияниеinformation flowsinformation flow controlformal verificationlanguage platformsecurity policyabstract semanticsnon-interferenceReferencesДевянин П.Н., Тележников В.Ю., Хорошилов А.В. Формирование методологии разработки безопасного системного программного обеспечения на примере операционных систем. Труды Института системного программирования РАН. 2021;33(5):25–40. https://doi.org/10.15514/ISPRAS-2021-33(5)-2Devyanin P.N., Telezhnikiv V.I., Khoroshilov A.V. Building a methodology for secure system software development on the example of operating systems. Trudy Instituta sistemnogo programmirovaniya RAN = Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(5):25–40 (in Russ.). https://doi.org/10.15514/ISPRAS-2021-33(5)-2Timakov 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/S0361768822040053Timakov 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/S0361768822040053Hedin 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-319Hedin 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-319Kozyri 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/3300000008Kozyri 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/3300000008Volpano 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-305Volpano 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-305Sabelfeld 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.856937Sabelfeld 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.856937Askarov 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.31Askarov 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.31Sutherland D. A model of information. In: Proceedings of the 9th National Security Conference. 1986. P. 175–183.Sutherland D. A model of information. In: Proceedings of the 9th National Security Conference. 1986. P. 175–183.Volpano D., Irvine C., Smith G. Sound type system for secure flow analysis. Journal of Computer Security (JCS). 1996;4(2–3): 167–187.Volpano D., Irvine C., Smith G. Sound type system for secure flow analysis. Journal of Computer Security (JCS). 1996;4(2–3): 167–187.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_8Mantel 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_8Myers 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.266669Myers 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.266669Graf 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.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.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_16Broberg 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_16Clarkson 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_15Clarkson 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_15Terauchi 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_24Terauchi 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Тимаков А.А. Вариант реализации процедуры анализа информационных потоков в программных блоках PL/SQL с использованием платформы PLIF. Программирование. 2023;4:39–57.Timakov A.A. Scenario of Information Flow Analysis Implementation in PL/SQL Program Units with PLIF Platform. Program. Comput. Soft. 2023;49(4):215–231. https://doi.org/10.1134/S0361768823040114 [Original Russian Text: Timakov A.A. Scenario of Information Flow Analysis Implementation in PL/SQL Program Units with PLIF Platform. Programmirovanie. 2023;4:215–231 (in Russ.).]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.1706349Broberg 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.1706349Sabelfeld A., Sands D. Declassification: Dimensions and principles. Journal of Computer Security (JCS). 2009;17(5):517–548. http://doi.org/10.3233/JCS-2009-0352Sabelfeld A., Sands D. Declassification: Dimensions and principles. Journal of Computer Security (JCS). 2009;17(5):517–548. http://doi.org/10.3233/JCS-2009-0352Youn 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.3199Youn 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

The authors declare that there are no conflicts of interest present.