Description of Paralocks Language Semantics in TLA+

Abstract

One of the basic aspects of information flow control in applications is a security policy language. This language should allow one to define security policies for evaluation of environment elements in coherence with higher-level access control rules. Hence, the language is expected to be flexible because there may be different access control paradigms (mandatory, role-based, etc.) implemented at the system level. The application may also have its own specific restrictions. Finally, it is also desirable that the language support declassification (controlled release of information) during computations. Paralocks is one of such languages. This research is devoted to the logical semantics of a modified version of Paralocks implemented in TLA+. Paralocks represents a language basis for the PLIF information flow control platform, which is developed with author’s participation for the analysis of PL/SQL program blocks. It includes proofs of the partial order and lattice defined on a set of security policy expressions.