Enviar artigo por via de e-mail Description of Paralocks language semantics in TLA+
- Autores: Timakov A.1
-
Afiliações:
- MIREA – Russian Technological University
- Edição: Nº 1 (2024)
- Páginas: 88-99
- Seção: INFORMATION SECURITY
- URL: https://journals.rcsi.science/0132-3474/article/view/259186
- DOI: https://doi.org/10.31857/S0132347424010073
- EDN: https://elibrary.ru/HJYWFT
- ID: 259186
Citar
Acesso aberto
Acesso está concedido
Somente assinantes
Resumo
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.
Sobre autores
A. Timakov
MIREA – Russian Technological University
Autor responsável pela correspondência
Email: timakov@mirea.ru
ORCID ID: 0000-0003-4306-789X
Rússia, Pr. Vernadskogo 78, Moscow, 119454
Bibliografia
- Devyanin P.N. and others. Integration of mandatory and role-based access control and mandatory control in a verified hierarchical security model of LED systems // Proceedings of the Institute of System Programming of the Russian Academy of Sciences. – 2020. – T. 32. – No. 1. – P. 7–26.
- Lamport L. Specifying systems: the TLA+ language and tools for hardware and software engineers. – 2002.
- Denning E.D. A lattice model of secure information flow // Communications of the ACM, 1976, No 5. P. 236–243.
- Broberg N., Sands D. Paralocks: Role-based information flow control and beyond // Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2010. P. 431–444.
- Myers C.A., Liskov B. A decentralized model for information flow control // ACM SIGOPS Operating Systems Review, 1997, No 5. p. 129–142.
- Timakov А.А. 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.Z. 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.
- Korablin Yu.P. Equivalence of program schemes based on the algebraic approach to specifying the semantics of programming languages // Russian Technological Journal, 2022, 10(1), P. 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.
