Programming and Computer SoftwareProgramming and Computer SoftwareПрограммирование0132-34743034-5847The Russian Academy of Sciences69567010.7868/S3034584725040079INFORMATION SECURITYИНФОРМАЦИОННАЯ БЕЗОПАСНОСТЬResearch ArticlePLIF PLATFORM: MODELING AND VERIFICATION OF INFORMATION FLOWS IN SOFTWARE DB UNITS USING THE TEMPORAL LOGIC OF ACTIONS TLA+Платформа PLIF: моделирование и проверка информационных потоков в программных блоках баз данных с использованием аппарата темпоральной логики действий TLA+TimakovA. A.ТимаковА. А.timakov@mirea.ruRyzhovI. G.РыжовИ. Г.ryzhov.ilgen@gmail.comMIREA – Russian Technological UniversityМИРЭА – Российский технологический универсистетRUDN UniversityРоссийский универсистет дружбы народов150820254NO4 (2025)№4 (2025)839801112025Copyright ©; 2025, Russian Academy of SciencesCopyright ©; 2025, Российская академия наук2025Russian Academy of SciencesРоссийская академия наукhttps://transsyst.ru/0132-3474/article/view/695670

The verification of software properties using formal verification tools is one of the current research directions in the field of information flow control. Security conditions of information flows in software under various information noninterferrence schemes are naturally described by so-called hyper-properties in well-known extensions of linear temporal logic and computation tree logic. In practice, verifying such properties for large projects is a non-trivial task. In this work, the authors translate the idea of dynamic type checking to detect prohibited information flows into the realm of computation verification using model-checking tools. Computations over security labels (safe types) are described by the abstract semantics of information flows. Transitioning from concrete computational semantics to abstract semantics of information flows allows formulating these security properties as state properties. In this case, proven tools in large industrial projects such as TLA+ and TLC can be used for the description and verification of real computer systems.

Проверка свойств программного обеспечения с использованием инструментов формальной верификации является одним из текущих направлений исследований в области контроля информационных потоков. Условия безопасности информационных потоков в программном обеспечении в различных схемах информационного невлияния естественным образом описываются так называемыми гипер-свойствами в известных расширениях линейной темпоральной логики и логики ветвящегося времени. На практике проверка таких свойств для больших проектов является нетривиальной задачей. В работе авторы транслируют идею динамической проверки типов для выявления запрещенных информационных потоков в область проверки вычислений с использованием инструментов проигрывания моделей. Вычисления над метками безопасности (безопасными типами) описываются абстрактной семантикой информационных потоков. Переход от конкретной вычислительной семантики к абстрактной семантике информационных потоков позволяет сформулировать указанные свойства безопасности как свойства состояний, в этом случае для описания и проверки реальных компьютерных систем могут быть использованы зарекомендовавшие себя в крупных промышленных проектах инструменты TLA+ и TLC.

information flowinformation flow controlsecurity policy languageformal verificationmodel checkingtemporal logicинформационный потокуправление информационным потокомязык политики безопасностиформальная верификацияпроверка моделитемпоральная логикаTimakov A.А. Analysis of information flow security using software implementing business logic based on stored database program blocks. Russian Technological Journal. 2024. V. 12. № 2. P. 16–27.Тимаков А.А. PLIF. 2021. GitHub. https://github.com / timimin / plifKozyri E. et al. Expressing Information Flow Properties // Foundations and Trends® in Privacy and Security. 2022. V. 3. № 1. P. 1–102.Hedin D., Sabelfeld A. A Perspective on Information-Flow Control // Software safety and security. 2012. P. 319–347.Balliu M., Schoepe D., Sabelfeld A. We are family: Relating information-flow trackers // Computer Security – ESORICS 2017: 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11–15, 2017, Proceedings, Part I 22. Springer International Publishing. 2017. P. 124–145.Russo A., Sabelfeld A., Li K. Implicit flows in malicious and nonmalicious code // Logics and Languages for Reliability and Security. – IOS Press, 2010. P. 301–322.Jang D. et al. An empirical study of privacy-violating information flows in JavaScript web applications // Proceedings of the 17th ACM conference on Computer and communications security. 2010. P. 270–283.Kang M.G. et al. Dta++: dynamic taint analysis with targeted control-flow propagation // NDSS. 2011.King D. et al. Implicit flows: Can’t live with ‘em, can’t live without ‘em // Information Systems Security: 4th International Conference, ICISS 2008, Hyderabad, India, December 16–20, 2008. Proceedings 4. Springer Berlin Heidelberg, 2008. P. 56–70.Staicu C.A. et al. An empirical study of information flows in real-world javascript // Proceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security. 2019. P. 45–59.Myers C.A., Liskov B. A decentralized model for information flow control // ACM SIGOPS Operating Systems Review. 1997. № 5. P. 129–142.Broberg N., van Delft B., Sands D. Paragon for practical programming with information-flow control // Programming Languages and Systems: 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9–11, 2013. Proceedings 11. Springer International Publishing. 2013. P. 217–232.Pottier F., Simonet V. Information Flow Inference for ML // ACM Transactions on Programming Languages and Systems. 2003. P. 117–158.Volpano D., Irvine C., Smith G. Sound type system for secure flow analysis // Journal of Computer Security. 1996. № 2–3. P. 167–187.Clarkson M.R. et al. Temporal logics for hyperproperties // Principles of Security and Trust: Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13. 2014. Proceedings 3. Springer Berlin Heidelberg. 2014. P. 265–284.Spearritt J. // Thesis for the Degree of Doctor of Engineering Practical. The Applicability of Information Flow to Secure Java Development, 2017.Seifermann S. et al. Detecting violations of access control and information flow policies in data flow diagrams // Journal of Systems and Software. 2022. V. 184. P. 111138.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.Lamport L. Specifying systems: the TLA+ language and tools for hardware and software engineers. 2002.Becker S., Koziolek H., Reussner R. The Palladio component model for model-driven performance prediction // Journal of Systems and Software. 2009. V. 82. № 1. P. 3–22.Dura A., Reichenbach C., Sŏderberg E. JavaDL: automatically incrementalizing Java bug pattern detection // Proceedings of the ACM on Programming Languages. 2021. V. 5. № OOPSLA. P. 1–31.Leavens G.T., Baker A.L., Ruby C. JML: a Java modeling language // Formal Underpinnings of Java Workshop (at OOPSLA’98). 1998. P. 404–420.Harel D., Kozen D., Tiuryn J. Dynamic logic // ACM SIGACT News. 2001. V. 32. № 1. P. 66–69.Ahrendt W. et al. The KeY platform for verification and analysis of Java programs // Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17–18, 2014, Revised Selected Papers 6. Springer International Publishing. 2014. P. 55–71.DeMarco T. Structured analysis and system specification. Software pioneers: contributions to software engineering. Berlin, Heidelberg: Springer Berlin Heidelberg. 2011. P. 529–560.