- PII
- 10.31857/S0132347424010073-1
- DOI
- 10.31857/S0132347424010073
- Publication type
- Article
- Status
- Published
- Authors
- Volume/ Edition
- Volume / Issue number 1
- Pages
- 88-99
- Abstract
- One of the basic aspects of information flow control in applications is security policy language. Such language should allow to define security policies for evaluation environment elements in coherence with higher level access control rules. So the language is expected to be flexible because there may be different access control paradigms implemented on the system level: mandatory, role-based etc. An application may also have its own specific restrictions. Finally it is also desirable that the language support declassification (controlled release of information) during the computation. One of such languages is Paralocks. The research is devoted to the logical semantics of modified version of Paralocks realized in TLA+. Paralocks represents a language basis for the perspective information flow control platform PLIF which is being developed for the analysis of PL/SQL program blocks with author’s participation. It includes the proofs of the partial order and lattice defined on the set of security policy expressions.
- Keywords
- контроль потока информации язык политики безопасности логическая семантика формальная верификация проверка модели программные модули
- Date of publication
- 15.02.2024
- Year of publication
- 2024
- Number of purchasers
- 0
- Views
- 49
References
- 1. Девянин П.Н. и др. Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы // Тр. Института системного программирования РАН. 2020. Т. 32. № 1. С. 7–26.
- 2. Lamport L. Specifying systems: the TLA+ language and tools for hardware and software engineers. 2002.
- 3. Denning, Dorothy Е. A lattice model of secure information flow // Communications of the ACM. 1976, № 5. Р. 236–243.
- 4. 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.
- 5. Myers, C. Andrew, Liskov, Barbara. A decentralized model for information flow control // ACM SIGOPS Operating Systems Review. 1997. № 5. Р. 129–142.
- 6. Тимаков А.А. PLIF. 2021. GitHub. https://github.com/timimin/plif.
- 7. 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.
- 8. Bonichon R., Delahaye D., Doligez D. Zenon. An extensible automated theorem prover producing checkable proofs //LPAR. 2007. Т. 4790. Р. 151–165.
- 9. Lamport L. How to write a proof //The American mathematical monthly. 1995. Т. 102. № 7. Р. 600–608.
- 10. Kukovec J., Konnov I. Type Inference for TLA in Apalache.
- 11. Broberg N. Thesis for the Degree of Doctor of Engineering Practical, Flexible Programming with Information Flow Control. 2011.
- 12. Кораблин Ю.П. Эквивалентность схем программ на основе алгебраического подхода к заданию семантики языков программирования // Russian Technological Journal. 2022. № 10(1). С. 18–27.
- 13. 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.
- 14. 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.
