Отправить статью по E-mail Описание семантики языка Paralocks в TLA+
- Авторы: Тимаков А.А.1
-
Учреждения:
- МИРЭА – Российский технологический универсистет
- Выпуск: № 1 (2024)
- Страницы: 88-99
- Раздел: ИНФОРМАЦИОННАЯ БЕЗОПАСНОСТЬ
- URL: https://journals.rcsi.science/0132-3474/article/view/259186
- DOI: https://doi.org/10.31857/S0132347424010073
- EDN: https://elibrary.ru/HJYWFT
- ID: 259186
Цитировать
Открытый доступ
Доступ предоставлен
Только для подписчиков
Аннотация
Одним из основных аспектов реализации контроля информационных потоков в программном обеспечении является язык описания политик безопасности или меток. Важно, чтобы такой язык позволял формировать политики безопасности элементов среды вычислений на основе правил управления доступом системного уровня. Соответственно язык должен быть достаточно гибким, поскольку на системном уровне могут использоваться разные механизмы: ролевое, мандатное управление доступом и др. Кроме того, в приложении могут действовать некоторые дополнительные ограничения. Наконец, желательно, чтобы язык позволял естественным образом учитывать возможность деклассификации данных (контролируемого раскрытия) в процессе вычислений. Одним из таких языков является Paralocks. Работа посвящена реализации семантики несколько упрощенной версии этого языка с использованием TLA+. Paralocks является языковой частью разработанной с участием автора платформы анализа информационных потоков в хранимых программных блоках баз данных PLIF. Приводятся доказательства свойств заданного отношения частичного порядка и решетки, построенной на основе множества всех возможных политик безопасности.
Об авторах
А. А. Тимаков
МИРЭА – Российский технологический универсистет
Автор, ответственный за переписку.
Email: timakov@mirea.ru
ORCID iD: 0000-0003-4306-789X
Россия, 119454, Москва, пр. Вернадского, д. 78
Список литературы
- Девянин П.Н. и др. Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы // Тр. Института системного программирования РАН. 2020. Т. 32. № 1. С. 7–26.
- Lamport L. Specifying systems: the TLA+ language and tools for hardware and software engineers. 2002.
- Denning, Dorothy Е. A lattice model of secure information flow // Communications of the ACM. 1976, № 5. Р. 236–243.
- Broberg, Niklas, Sands, David. Paralocks: Role-based information flow control and beyond // Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2010. Р. 431–444.
- Myers, C. Andrew, Liskov, Barbara. A decentralized model for information flow control // ACM SIGOPS Operating Systems Review. 1997. № 5. Р. 129–142.
- Тимаков А.А. PLIF. 2021. GitHub. https://github.com/timimin/plif.
- Blanchette J. C., Bulwahn L., Nipkow T. Automatic proof and disproof in Isabelle/HOL //Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011, Saarbrucken, Germany, October 5–7, 2011. Proceedings 8. Springer Berlin Heidelberg, 2011. Р. 12–27.
- Bonichon R., Delahaye D., Doligez D. Zenon. An extensible automated theorem prover producing checkable proofs //LPAR. 2007. Т. 4790. Р. 151–165.
- Lamport L. How to write a proof //The American mathematical monthly. 1995. Т. 102. № 7. Р. 600–608.
- Kukovec J., Konnov I. Type Inference for TLA in Apalache.
- Broberg N. Thesis for the Degree of Doctor of Engineering Practical, Flexible Programming with Information Flow Control. 2011.
- Кораблин Ю.П. Эквивалентность схем программ на основе алгебраического подхода к заданию семантики языков программирования // Russian Technological Journal. 2022. № 10(1). С. 18–27.
- 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. С. 217–232.
- 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. С. 265–284.
