Платформа PLIF: моделирование и проверка информационных потоков в программных блоках баз данных с использованием аппарата темпоральной логики действий TLA+

Обложка

Цитировать

Полный текст

Открытый доступ Открытый доступ
Доступ закрыт Доступ предоставлен
Доступ закрыт Только для подписчиков

Аннотация

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

Об авторах

А. А. Тимаков

МИРЭА – Российский технологический универсистет

Email: timakov@mirea.ru
119454 Москва, Проспект Вернадского, д. 78, Россия

И. Г. Рыжов

Российский универсистет дружбы народов

Email: ryzhov.ilgen@gmail.com
117198 Москва, ул. Миклухо-Маклая, д. 6, Россия

Список литературы

  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
Скачать

© Российская академия наук, 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») на элемент с текстом «Принять и продолжить».