PLIF PLATFORM: MODELING AND VERIFICATION OF INFORMATION FLOWS IN SOFTWARE DB UNITS USING THE TEMPORAL LOGIC OF ACTIONS TLA+

封面

如何引用文章

全文:

开放存取 开放存取
受限制的访问 ##reader.subscriptionAccessGranted##
受限制的访问 订阅存取

详细

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.

作者简介

A. Timakov

MIREA – Russian Technological University

Email: timakov@mirea.ru
78 Vernadsky Avenue, Moscow 119454

I. Ryzhov

RUDN University

Email: ryzhov.ilgen@gmail.com
6 Miklukho-Maklaya street, Moscow, 117198, Russia

参考

  1. 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.
  2. Тимаков А.А. PLIF. 2021. GitHub. https://github.com / timimin / plif
  3. Kozyri E. et al. Expressing Information Flow Properties // Foundations and Trends® in Privacy and Security. 2022. V. 3. № 1. P. 1–102.
  4. Hedin D., Sabelfeld A. A Perspective on Information-Flow Control // Software safety and security. 2012. P. 319–347.
  5. 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.
  6. 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.
  7. 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.
  8. Kang M.G. et al. Dta++: dynamic taint analysis with targeted control-flow propagation // NDSS. 2011.
  9. 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.
  10. 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.
  11. Myers C.A., Liskov B. A decentralized model for information flow control // ACM SIGOPS Operating Systems Review. 1997. № 5. P. 129–142.
  12. 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.
  13. Pottier F., Simonet V. Information Flow Inference for ML // ACM Transactions on Programming Languages and Systems. 2003. P. 117–158.
  14. Volpano D., Irvine C., Smith G. Sound type system for secure flow analysis // Journal of Computer Security. 1996. № 2–3. P. 167–187.
  15. 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.
  16. Spearritt J. // Thesis for the Degree of Doctor of Engineering Practical. The Applicability of Information Flow to Secure Java Development, 2017.
  17. 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.
  18. 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.
  19. Lamport L. Specifying systems: the TLA+ language and tools for hardware and software engineers. 2002.
  20. 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.
  21. 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.
  22. 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.
  23. Harel D., Kozen D., Tiuryn J. Dynamic logic // ACM SIGACT News. 2001. V. 32. № 1. P. 66–69.
  24. 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.
  25. DeMarco T. Structured analysis and system specification. Software pioneers: contributions to software engineering. Berlin, Heidelberg: Springer Berlin Heidelberg. 2011. P. 529–560.

补充文件

附件文件
动作
1. JATS XML
下载

版权所有 © Russian Academy of Sciences, 2025

Согласие на обработку персональных данных с помощью сервиса «Яндекс.Метрика»

1. Я (далее – «Пользователь» или «Субъект персональных данных»), осуществляя использование сайта https://journals.rcsi.science/ (далее – «Сайт»), подтверждая свою полную дееспособность даю согласие на обработку персональных данных с использованием средств автоматизации Оператору - федеральному государственному бюджетному учреждению «Российский центр научной информации» (РЦНИ), далее – «Оператор», расположенному по адресу: 119991, г. Москва, Ленинский просп., д.32А, со следующими условиями.

2. Категории обрабатываемых данных: файлы «cookies» (куки-файлы). Файлы «cookie» – это небольшой текстовый файл, который веб-сервер может хранить в браузере Пользователя. Данные файлы веб-сервер загружает на устройство Пользователя при посещении им Сайта. При каждом следующем посещении Пользователем Сайта «cookie» файлы отправляются на Сайт Оператора. Данные файлы позволяют Сайту распознавать устройство Пользователя. Содержимое такого файла может как относиться, так и не относиться к персональным данным, в зависимости от того, содержит ли такой файл персональные данные или содержит обезличенные технические данные.

3. Цель обработки персональных данных: анализ пользовательской активности с помощью сервиса «Яндекс.Метрика».

4. Категории субъектов персональных данных: все Пользователи Сайта, которые дали согласие на обработку файлов «cookie».

5. Способы обработки: сбор, запись, систематизация, накопление, хранение, уточнение (обновление, изменение), извлечение, использование, передача (доступ, предоставление), блокирование, удаление, уничтожение персональных данных.

6. Срок обработки и хранения: до получения от Субъекта персональных данных требования о прекращении обработки/отзыва согласия.

7. Способ отзыва: заявление об отзыве в письменном виде путём его направления на адрес электронной почты Оператора: info@rcsi.science или путем письменного обращения по юридическому адресу: 119991, г. Москва, Ленинский просп., д.32А

8. Субъект персональных данных вправе запретить своему оборудованию прием этих данных или ограничить прием этих данных. При отказе от получения таких данных или при ограничении приема данных некоторые функции Сайта могут работать некорректно. Субъект персональных данных обязуется сам настроить свое оборудование таким способом, чтобы оно обеспечивало адекватный его желаниям режим работы и уровень защиты данных файлов «cookie», Оператор не предоставляет технологических и правовых консультаций на темы подобного характера.

9. Порядок уничтожения персональных данных при достижении цели их обработки или при наступлении иных законных оснований определяется Оператором в соответствии с законодательством Российской Федерации.

10. Я согласен/согласна квалифицировать в качестве своей простой электронной подписи под настоящим Согласием и под Политикой обработки персональных данных выполнение мною следующего действия на сайте: https://journals.rcsi.science/ нажатие мною на интерфейсе с текстом: «Сайт использует сервис «Яндекс.Метрика» (который использует файлы «cookie») на элемент с текстом «Принять и продолжить».