Description of Paralocks language semantics in TLA+

封面

如何引用文章

全文:

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

详细

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.

作者简介

A. Timakov

MIREA – Russian Technological University

编辑信件的主要联系方式.
Email: timakov@mirea.ru
ORCID iD: 0000-0003-4306-789X
俄罗斯联邦, Pr. Vernadskogo 78, Moscow, 119454

参考

  1. 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.
  2. Lamport L. Specifying systems: the TLA+ language and tools for hardware and software engineers. – 2002.
  3. Denning E.D. A lattice model of secure information flow // Communications of the ACM, 1976, No 5. P. 236–243.
  4. 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.
  5. Myers C.A., Liskov B. A decentralized model for information flow control // ACM SIGOPS Operating Systems Review, 1997, No 5. p. 129–142.
  6. Timakov А.А. 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.Z. 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. 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.
  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.

版权所有 © Russian Academy of Sciences, 2024

##common.cookie##