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.

INTRODUCTION

This paper is useful to readers who are familiar with formal security models based on access control and information flow control (IFC), as well as readers who have sufficient knowledge in the field of formal verification and skills in working with related tools. All necessary information can be found in [1–5].

The majority of IFC mechanisms [4, 5] used to describe sets of security policies and abstract semantics of information flows rely on the concept of an algebraic lattice. In this case, proofs of properties of proposed lattices, as well as proofs of correctness of operators for calculating the least upper (greatest lower) bound, are often omitted. Despite the apparent obviousness of assumptions, the absence of such proofs somewhat undermines confidence in implemented mechanisms.

This paper describes the semantics of a simplified version of the Paralocks language for security policy description [4], which forms a language basis for the PLIF information flow control platform [6]. The paper also provides exhaustive explanations for the proofs of properties of a lattice defined on a set of all possible policies.

To check these properties, the following approach was used. At the preliminary stage, the model was run on a small set of initial data using the TLC tool. The absence of contradictions at this stage justified the transition to the second stage: the proof of the properties by using the TLAPS formal logic system. This system allows one to construct proofs hierarchically, which facilitates the use of natural deduction. TLAPS relies on automated theorem proving tools such as Isabelle [7] and Zennon [8]. The described approach provides additional guarantees, which is quite important for formal models. According to some authors [9], up to a third of the proofs published in various studies are incorrect.

In addition, a certain innovation of this research is the use of the Apalache type checking subsystem [10] to prove type invariants for some structures used to describe security policy clauses and policies themselves in TLA+ specifications. This, in turn, enables a reasonable use of some non-obvious assumptions in the proofs.

PARALOCKS SEMANTICS IN TLA+

This paper is useful to readers who are familiar with formal security models based on access control and IFC, as well as readers who have sufficient knowledge in the field of formal verification and skills in working with related tools. All necessary information can be found in the references.

Paralocks is a language for description of security policies, which forms a language basis for the PLIF information flow control platform [4]. The advantages of this language that predetermined its choice were described in our previous paper.

Security policy P_k is defined by a predicate logic formula represented as a conjunction of definite Horn disjuncts: . Here, C_n is a policy clause of form , …, x_m.l₁(⋅) ∧ l₂(⋅) ∧ l₃(⋅)… ⇒ Flow(u), where u is a bound variable or constant that defines the user, Flow(u) is a predicate that indicates the legality of a data flow to u, and are conditions (locks) the fulfillment of which is required for Flow(u) to have TRUE value. Predicates can be parametric or non-parametric.

For instance, the policy clause “A flow to a random user is possible if (a) the guest lock is open (the guest role is set for x) and the lock is open (a specified period of time is expired) or (b) the manager lock is open (the manager role is set for x)" is formally represented as follows: . (t_expire ∧ guest(x) ⇒ Flow(x)) ∧ (manager(x) ⇒ Flow(x))/

To describe policies in the Paralocks.tla specification [6], the following constants are introduced: is a set of valid names for bound variables, U is a set of actors (system users), E₀ is a set of names for non-parametric locks, and E₁ is a set of names for parametric (single-parameter) locks. The well-known scenarios of using Paralocks to encode policies associated with the most popular access control mechanisms (mandatory, role-based, etc.) for software environment elements (variables, function parameters, exceptions, etc.) allow one to confine only to non-parametric and single-parameter locks, as well as make other assumptions to facilitate the description of the corresponding entities in TLA+ specifications. Suppose that the set UU of bound variable names has one element. Suppose also that, if a bound variable appears in one of the locks of some policy clause, then this variable is an argument in the literal of the same clause. In addition, if a bound variable is an argument of for some policy clause, then all parametric locks of this clause also accept this variable as an argument.

The set of possible security policy clauses and the set of policies themselves are defined as follows:

ClausesSet

      {⟨u, ⟨e0, e1⟩⟩ : u ∈ (U ∪ UU),

   e0 ∈ [E0 → SUBSET {NONE}],

   e1 ∈ [E1 → ((SUBSET (U) ∪ SUBSET (UU))

      \{{}}) ∪ {{NONE}}]}

PoliciesSet

    {p ∈ SUBSET ClausesSet :

   ∀ c1 ∈ p : c2 ∈ p :

∧ c1 ≠ c2

∧ ∨(compareClause(c1, c2)

∨ compareClause(c2, c1))}

∪ {{}}

A policy is described by a set of two-dimensional tuples. Each tuple is an individual policy clause. Its first element is a bound variable or constant that defines the user who is allowed to receive an information flow; its second element is a two-dimensional tuple that describes the set of locks that must be open. The elements of this tuple are records, and their fields correspond to the names of the locks defined by model constants; the values of the fields define the sets of actual lock parameters. One policy cannot have two different ordered clauses.

The example described above is written in PLIF specifications as follows:1

{⟨x, ⟨[t_expire ↦ {}], [guest ↦ {x},

  reviewer ↦ {NONE}, manager ↦ {NONE},

  organizer ↦ {NONE}]⟩⟩}⟩],

⟨x, ⟨[t_expire ↦ {NONE}], [guest ↦ {NONE},

  reviewer ↦ {NONE}, manager ↦ {x},

  organizer ↦ {NONE}]⟩⟩}

Here, , , {guest, reviewer, manager, organizer} ⊆ E₁ and is a special value that indicates that opening the lock is not required (in TLA+, records are functions, and partially defined functions are not supported).

In addition, taking into account the above constraints, the following assumptions hold:

ASSUME U_ASSMU ≠ {} ∧ NONE ∉ U

ASSUME UU_ASSMUU ={“x”}

ASSUME Clause_ASSM2

  ∀ c ∈ ClausesSet :

   (∨ ∧ c [1] ∈ UU

∧ ∀ e1 ∈ E1 : c [2] [2][e1] = UU

∨ ∧ c [1] ∉ UU

∧ ∀ e1 ∈ E1 : c [2] [2][e1] ∩ UU ={})

Explanations for some other assumptions that are defined in Paralocks.tla and used in formal proofs are given below.

The comparison operator is defined on the set of security policy clauses:

compareClause(c1, c2)

∧ substMap3Equality (c1, c2)

∧ ∀ k ∈ E0 : ∨ c1 [2] [1][k] = c2 [2] [1][k]

∨ c2 [2] [1][k] = {}

∧ ∀ ∈ E1 : c1 [2] [2][e] = {NONE}

∨ matchLocks(c1, c2, e)

⊆ c2 [2] [2][e]

Operator compareClause(c1, c2) returns TRUE – clause c2 is at least as strict as clause c1 – if two conditions are met: (a) there is a substitution that reduces the predicate Flow(⋅) of c1 to the form identical to the predicate Flow(⋅) of c2 and, (b) upon applying the corresponding substitution to the locks of c1, the set of locks of c1 is a subset of locks of c2. The logical interpretation of the thus-defined partial order can be found in [4].

The parameter of predicate Flow(⋅) can be a bound variable (element of set UU) or a particular user (element of set U), which is why the fulfillment of the first condition is checked by evaluating the function

substMap3Equality (c1, c2)

         c1 [1] ∈ UU ∨ c1 [1] = c2 [1]

In this notation, the second element of a policy clause is a two-dimensional tuple of records that define required sets of non-parametric and parametric locks. If opening some non-parametric lock is not required, then the corresponding field of the record takes value {NONE}; otherwise, it takes value {}. Thus, the inclusion of the set of non-parametric locks of clause c1 into the set of non-parametric locks of clause c2 actually means

∀ k ∈ E0 : ∨ c1 [2] [1][k] = c2 [2] [1][k]

∨ c2 [2] [1][k] = {}

For single-parameter locks, value {NONE} in the field of the corresponding lock also means that opening the lock is not required. If the lock field contains a non-empty set of elements other than NONE, then the legality of an information flow to the user specified by Flow(⋅) requires opening some instances of this lock (which are determined by a given set of elements). If necessary, function matchLocks(⋅) performs the corresponding substitution to the expressions of the single-parameter locks of c1:

matchLocks(c1, c2, e)

  LET cc1 [2] [2][e]

   IN

       IF c ∩ UU ≠ {}

       THEN (c\UU) ∪ {c2 [1]}

       ELSE c

To compare security policies, function comparePol(⋅) is used. Its definition is trivial:

comparePol(p1, p2)

  ∀ c2 ∈ p2 :

   (∃ c1 ∈ p1 : compareClause(c1, c2))

Below, some explanations of TLAPS expressions use operator instead of and .

The most important semantic rules of Paralocks are those associated with calculating the least upper bound (LUB) and greatest lower bound (GLB) of two security policies. The GLB of two arbitrary security policies and is a maximally strict policy p_GLB such that p_GLBp1 and p_GLBp2. With each policy clause representing an individual possibility of a legal information flow, the following statement obviously holds:

GLB(p1, p2) p1 ∪ p2

The LUB of two arbitrary security policies and is a minimally strict policy such that p1 p_LUB and p2 p_LUB. To calculate it, for all possible pairs such that , and there is a substitution that reduces the Flow(⋅) predicate of clause to the form identical to the Flow(⋅) predicate of clause c2 or, conversely, the Flow(⋅) predicate of c2 to the form identical to the Flow(⋅) predicate of c1, it is required to generate a new policy clause by making the corresponding substitution to the locks of c1 or c2 and, then, uniting the resulting sets of locks of the original clauses:

LUB(p1, p2) {x ∈ {unionCl(c1, c2) :

            c1 ∈ p1, c2 ∈ p2} : x ≠ ⟨⟩}

Here, function unionCl(c1, c2) calculates a new clause of policy based on and if there is the corresponding substitution; otherwise, it returns an empty clause ⟨⟩:

unionCl(c1, c2)

  LET capMap [e0 ∈ E0 ↦

    c1[2][1][e0] ∩ c2[2][1][e0]]

  IN

    IF substMap3Equality(c1, c2)

     THEN ⟨c2 [1], ⟨capMap,

          [e1 ∈ E1 ↦

          IF ∧ NONE ∈ c1[2][2][e1]

            ∧ NONE ∈ c2[2][2][e1]

          THEN {NONE}

          ELSE (matchLocks(c1, c2, e1)

∪ c2[2][2][e1]) \ {NONE}]⟩⟩

     ELSE

     IF substMap3Equality(c2, c1)

     THEN ⟨c1 [1], ⟨capMap,

         [e1 ∈ E1 ↦

         IF ∧ NONE ∈ c1 [2] [2][e1]

           ∧ NONE ∈ c2 [2] [2][e1]

           THEN {NONE}

           ELSE (matchLocks(c2, c1, e1)

                ∪ c1[2][2][e1]) \ {NONE}]⟩⟩

     ELSE ⟨⟩

Local function unites the non-parametric locks of clauses c1 and c2 (the field corresponding to the non-parametric lock takes value {NONE} if no lock is required; otherwise, it takes value {}).

To prove some properties using TLAPS, as noted above, it is convenient to use assumptions. Proving them is sometimes difficult, sometimes even impossible, because TLAPS has a number of limitations. For instance, the system does not fully support sets of tuples. Checking properties by using the model replay mechanism on incomplete datasets does not provide formal guarantees. For type invariants, the problem can be partially solved using the Snowcat type checker, which is part of the Apalache platform [10]. Another assumption used in the proofs is . Its validity is confirmed using Snowcat. It should be noted, however, that the use of this tool generally requires a special markup of specifications:

@: CLAUSE = ⟨U, ⟨E0 → Set(U), E1 → Set(U)⟩⟩;

@: POLICY = Set(CLAUSE);

@type: Set(CLAUSE);

ClausesSet {…}

@type: Set(POLICY);

PoliciesSet {…}

@type: (POLICY, POLICY) ⇒ POLICY;

LUB(p1, p2) {x ∈ {unionCl(c1, c2) :

        c1 ∈ p1, c2 ∈ p2} : x ≠ EC}

ASSUME LUB_PS ∀ p1, p2 ∈ PoliciesSet :

             LUB(p1, p2) ∈ PoliciesSet

Other trivial assumptions described in Paralocks.tla are not considered here.

CHECKING PROPERTIES OF A LATTICE DEFINED ON A SET OF SECURITY POLICIES

Deriving formal proofs for desired properties of algebraic structures described in the Paralocks.tla specification by using the TLAPS logical system is a very time-consuming process. That is why, at the initial stage, the properties were checked on a small dataset by using the tool for evaluating expressions over the constants of the TLA + Toolbox environment and, in some cases, by using the TLC model checking tool. Results of the preliminary stage are not presented in this paper; however, they can be found in files of the project [6]. Let us describe the general form of a proof that function is a partial order on the set of policies .

Reflexivity

It is convenient to divide the check into two cases: the case where the set of clauses of an arbitrary policy is empty and the case where it is not.

THEOREM Reflexitivity

     ∀ p ∈ PoliciesSet : comparePol(p, p)

⟨1⟩ USE DEF comparePol, compareClause,

            substMap3Equality, matchLocks

⟨1⟩1 TAKE pol ∈ PoliciesSet

⟨1⟩2 CASE pol = { }

  …

⟨1⟩3 CASE pol ≠ { }

    …

⟨1⟩4. QED

  BY ⟨1⟩2, ⟨1⟩3

In the first case, it is obvious that

∀c2 ∈ pol : (∃c1 ∈ pol : compareClause(c1, c2)), the proof follows from the definition comparePol(⋅).

In the second case, for arbitrary , it is required to prove that compareClause(c1, c1) is true, or, taking into account the definition of compareClause(⋅):

…

⟨1⟩3.CASE pol ≠ {}

⟨2⟩1 TAKE c1 ∈ pol

        …

⟨2⟩3 substMap3Equality(c1, c1)

       …

⟨2⟩4 ∀ k ∈ E0 : ∨ c1 [2] [1][k] = c1 [2] [1][k]

∨ c1 [2] [1][k] = {}

       …

⟨2⟩5 ∀ e ∈ E1 : ∨ c1 [2] [2][e] = {NONE}

∨ matchLocks(c1, c1, e)

⊆ c1 [2] [2][e]

       …

⟨2⟩6 QED

BY ⟨2⟩3, ⟨2⟩4, ⟨2⟩5

…

The proof of step ⟨2⟩3 is obvious: it follows from the definition of substMap3Equality(⋅) and the fact that c1 [1] = c1 [1] is true. Step ⟨2⟩4 also does not require proof. To prove step ⟨2⟩5, the case where ≠ NONE is of interest.

…

⟨2⟩5 ∀ e ∈ E1 : ∨ c1 [2] [2][e] = {NONE}

∨ matchLocks(c1, c1, e)

⊆ c1 [2] [2][e]

⟨3⟩1 TAKE e ∈ E1

⟨3⟩2 CASE c1 [2] [2][e] = {NONE}

⟨4⟩1 c1 [2] [2][e] = {NONE}

PROOF BY ⟨3⟩2

⟨4⟩2 QED BY ⟨4⟩1

⟨3⟩3 CASE c1 [2] [2][e] ≠ {NONE}

…

⟨3⟩4 QED BY ⟨3⟩2 , ⟨3⟩1, ⟨3⟩3

…

In this case, it is required to prove that matchLocks(c1, c1, e) ⊆ c1 [2] [2][e]. If c1 [2] [2][e] ∩ UU = {}, then the proof follows from the definition of matchLocks(⋅) and the fact that c1 [2] [2][e] ⊆ c1 [2] [2][e] is true:

…

⟨4⟩1 matchLocks(c1, c1, e) ⊆ c1 [2] [2][e]

⟨5⟩1 CASE c1 [2] [2][e] ∩ UU = {}

⟨6⟩1 c1 [2] [2][e] ⊆ c1 [2] [2][e]

PROOF OBVIOUS

⟨6⟩2 QED BY ⟨5⟩1, ⟨6⟩1 DEF matchLocks

…

In the case where c1 [2] [2][e] ∩ UU ≠ {}, the proof is straightforward:

…

⟨4⟩1 matchLocks(c1, c1, e) ⊆ c1 [2] [2][e]

⟨5⟩1 CASE c1 [2] [2][e] ∩ UU = {}

…

⟨5⟩2 CASE c1 [2] [2][e] ∩ UU ≠ {}

⟨6⟩1 c1 ∈ ClausesSet

PROOF BY ONLY DEF PoliciesSet

⟨6⟩2 {c1 [1]} = UU

PROOF BY ⟨5⟩2, ⟨6⟩1,

Clause_ASSM2, UU_ASSM

⟨6⟩3 QED BY ⟨5⟩2, ⟨6⟩2

…

Transitivity

This property is formulated as a theorem in TLAPS:

THEOREM Transitivity

∀ p1, p2, p3 ∈ PoliciesSet :

∧ comparePol(p1, p2)

∧ comparePol(p2, p3)

⇒ comparePol(p1, p3)

…

By selecting , , and from PoliciesSet and assuming that comparePol(p1, p2) ∧ comparePol(p2, p3), it is required to prove that ∀c3 ∈ p3 : (∃c1 ∈ p1 : compareClause(c1, c3)):2

…

⟨1⟩ USE DEF comparePol, compareClause,

substMap3Equality, matchLocks

⟨1⟩1 TAKE p1 ∈ PoliciesSet, p2 ∈ PoliciesSet,

p3 ∈ PoliciesSet

⟨1⟩3 HAVE ∧ comparePol(p1, p2)

∧ comparePol(p2, p3)

⟨1⟩4 ∀ c3 ∈ p3 : (∃ c1 ∈ p1 :

compareClause(c1, c3))

…

⟨1⟩5 QED BY ⟨1⟩4

Obviously, for any , there are and such that .∧ Then, to prove the theorem, it is sufficient to select the corresponding c1, c2, and c3 and prove that , or, taking into account the definition of substMap3Equality(⋅):

…

⟨2⟩1 TAKE c3 ∈ p3

⟨2⟩2 PICK c2 ∈ p2 : compareClause(c2, c3)

    PROOF BY ⟨1⟩3

⟨2⟩3 PICK c1 ∈ p1 : compareClause(c1, c2)

    PROOF BY ⟨1⟩3

⟨2⟩4 c1 [1] ∈ UU ∨ c1 [1] = c3 [1]

    PROOF BY ⟨2⟩3, ⟨2⟩2

⟨2⟩5 ∀ k ∈ E0 : ∨ c1 [2] [1][k] = c3 [2] [1][k]

∨ c3 [2] [1][k] = {}

    PROOF BY ⟨2⟩3, ⟨2⟩2

⟨2⟩6 ∀ k ∈ E1 : ∨ c1 [2] [2][e] = {NONE}

∨ matchLocks(c1, c3, e)

⊆ c3 [2] [2][e]

…

⟨2⟩7 QED BY ⟨2⟩4, ⟨2⟩5, ⟨2⟩6

…

The proofs of steps ⟨2⟩4 and ⟨2⟩5 follow from the proofs of ⟨2⟩2 and ⟨2⟩3, as well as from the definitions of and . To prove step ⟨2⟩6, the case where c1 [2] [2][e] ≠ NONE is of interest:

…

⟨2⟩6 ∀ e ∈ E1 : ∨ c1 [2] [2][e] = {NONE}

∨ matchLocks(c1, c3, e)

⊆ c3 [2] [2][e]

⟨3⟩1 TAKE e ∈ E1

⟨3⟩2 CASE c1 [2] [2][e] = {NONE}

PROOF BY ⟨3⟩2

⟨3⟩3 CASE c1 [2] [2][e] ≠ {NONE}

…

⟨3⟩4 QED BY ⟨3⟩1, ⟨3⟩2, ⟨3⟩2

…

In this case, it is required to prove that matchLocks(c1, c3, e) ⊆ c3 [2] [2][e]. For c1 [2] [2][e] ∩ UU ≠ {}, the proof can be obtained as follows:

…

⟨4⟩2 CASE c1 [2] [2][e] ∩ UU ≠ {}

⟨5⟩1 ((c1 [2] [2][e] \ UU) ∪ {c2 [1]}) ⊆ c2 [2] [2][e]

PROOF BY ⟨4⟩2, ⟨3⟩3, ⟨2⟩3

⟨5⟩2 ((c1 [2] [2][e] \ UU) ∪ {c3 [1]})

⊆ ((c2 [2] [2][e] \ UU) ∪ {c3 [1]})

PROOF BY ⟨5⟩1

⟨5⟩3 c2 ∈ ClausesSet

PROOF BY ONLY PoliciesSet

⟨5⟩4 c2 [1] ≠ NONE

PROOF BY ⟨5⟩3, U_ASSM,

UU_ASSM, Clause_ASSM3

⟨5⟩5 c2 [2] [2][e] ≠ {NONE}

PROOF BY ⟨5⟩4, ⟨5⟩1

⟨5⟩6 QED BY ⟨5⟩5, ⟨5⟩2, ⟨2⟩2, ⟨2⟩3

⟨4⟩3 CASE c1 [2] [2][e] ∩ UU = {}

…

⟨4⟩4 QED BY ⟨4⟩3, ⟨4⟩2

…

In the case where c1 [2] [2][e] ∩ UU = {}, the proof is similar.

Antisymmetry

The antisymmetry property of the partial order on the set of security policies PoliciesSet can be expressed as follows:

THEOREM Antisymmetry

               ∀ p1, p2 ∈ PoliciesSet :

                 ∧ comparePol(p1, p2)

                 ∧ comparePol (p2, p1) ⇒ p1 = p2

The general scheme of the proof is self-explanatory:

…

⟨1⟩ USE DEF comparePol, compareClause,

       substMap3Equality, matchLocks

⟨1⟩1 TAKE p1 ∈ PoliciesSet, p2 ∈ PoliciesSet

⟨1⟩2 HAVE ∧ comparePol(p1, p2) ∧ comparePol(p2, p1)

⟨1⟩4 p1 = p2

⟨2⟩1 ∀ c2 ∈ p2 : ∃c1 ∈ p1 : c2 = c1

⟨2⟩2 ∀ c1 ∈ p1 : ∃c2 ∈ p2 : c1 = c2

…

⟨2⟩5 QED BY ⟨2⟩1, ⟨2⟩2

⟨1⟩5 QED BY ⟨1⟩4

The proofs of steps ⟨2⟩1 and ⟨2⟩2 are obviously identical.

Let us now consider the structure of a proof for step ⟨2⟩1. As noted above, a security policy clause c consists of three components: the predicate – (which is represented by a predicate parameter), the set of non-parametric locks, and the set of parametric locks (which are represented as records whose fields correspond to names of locks, while field values correspond to their parameters). Thus, the proof reduces to checking the equivalence of the corresponding elements:

…

⟨2⟩1 ∀ c2 ∈ p2 : ∃c1 ∈ p1 : c2 = c1

  …

       ⟨3⟩7 c1 [1] = c2 [1]

        …

         ⟨3⟩8 c1 [2] [1] = c2 [2] [1]

           …

         ⟨3⟩9 c1 [2] [2] = c2 [2] [2]

           …

         ⟨3⟩10 QED BY ⟨3⟩7, ⟨3⟩8, ⟨3⟩9

                 DEF PoliciesSet, ClausesSet

…

At the initial stage, we take arbitrary from and select such from and from that and . Let us prove that :

…

⟨3⟩1 TAKE c2 ∈ p2

⟨3⟩3 PICK c1 ∈ p1 : compareClause(c1, c2)

      PROOF BY ⟨1⟩2

⟨3⟩4 PICK c3 ∈ p2 : compareClause(c3, c1)

      PROOF BY ⟨1⟩2

      …

⟨3⟩6 c3 = c2

…

Since the security policy expression cannot contain two different clauses and such that or , to prove step ⟨3⟩6, it is sufficient to prove that :

…

 ⟨3⟩5 compareClause(c3, c2)

      …

⟨3⟩6 c3 = c2

     PROOF BY ⟨3⟩5 DEF PoliciesSet

…

The fact that the first two conjuncts of expression compareClause(c3, c2) are true follows directly from the proofs of steps ⟨3⟩3 and ⟨3⟩4 ( ∧ ), definition of compareClause(⋅), and assumption Clause_ASSM4 that ∈ for any c that belongs to ClausesSet:

…

⟨3⟩5 compareClause(c3, c2)

⟨4⟩1 c3 [1] ∈ UU ∨ c3 [1] = c2 [1]

PROOF BY ⟨3⟩3, ⟨3⟩4

⟨4⟩2 ∀ e ∈ E0 :

∧ ∨ c2 [2] [1][e] = c3 [2] [1][e]

∨ c2 [2] [1][e] = {}

PROOF BY ⟨3⟩3, ⟨3⟩4, Clause_ASSM4

⟨4⟩3 ∀ e ∈ E1 : ∨ c3 [2] [2][e] = {NONE}

∨ matchLocks(c3, c2, e)

⊆ c2 [2] [2][e]

…

⟨4⟩4 QED BY ⟨4⟩1, ⟨4⟩2, ⟨4⟩3

…

To prove that the last condition of expression compareClause(c3, c2) holds, we need to consider three cases:

…

⟨4⟩3 ∀ e ∈ E1 : ∨ c3 [2] [2][e] = {NONE}

∨ matchLocks(c3, c2, e)

⊆ c2 [2] [2][e]

⟨5⟩1 TAKE e ∈ E1

⟨5⟩2 CASE c3 [2] [2][e] = {NONE}

PROOF BY ⟨5⟩2

⟨5⟩3 CASE c3 [2] [2][e] ∩ UU = {}

∧ c3 [2] [2][e] ≠ {NONE}

…

⟨5⟩4 CASE c3 [2] [2][e] ∩ UU ≠ {}

∧ c3 [2] [2][e] ≠ {NONE}

…

⟨5⟩5 QED BY ⟨5⟩2, ⟨5⟩3, ⟨5⟩4

DEF matchLocks

…

The proof of step ⟨5⟩2 is trivial. Complete proofs of steps ⟨5⟩3 and ⟨5⟩4 are not presented to save room. Let us only note that they are based on the fact that ∧ , as well as on the assumptions and .

Based on the definitions of compareClause(⋅) and substMap3Equality(⋅), the assumption that the set of admissible bound variables consists of one element (), and proofs of steps ⟨3⟩3, ⟨3⟩4, and ⟨3⟩6, we have (c3 [1] = x ∨ c3 [1] = c1 [1]) ∧ (c1 [1] = x ∨ c1 [1] = c2 [1]) ∧ . This proves step ⟨3⟩7, i.e., . The proof of step ⟨3⟩8 – = is also trivial.

…

⟨3⟩7 c1 [1] = c2 [1]

      PROOF BY ⟨3⟩3, ⟨3⟩4, ⟨3⟩6, UU_ASSM

⟨3⟩8 c1 [2] [1] = c2 [2] [1]

     ⟨4⟩1 ∀ e0 ∈ E0 : c1 [2] [1][e0] = c2 [2] [1][e0]

           PROOF BY ⟨3⟩3, ⟨3⟩4, ⟨3⟩6

      ⟨4⟩2 QED BY ⟨4⟩1, Clause_ASSM4

                           DEF PoliciesSet

…

It remains to prove step ⟨3⟩9: . For this purpose, it is sufficient to select an arbitrary value from and prove that c1 [2] [2][e1] = c2 [2] [1][e1]. The general structure of the proof for this step is as follows:

…

⟨3⟩9:

⟨4⟩1 SUFFICES ASSUME NEW e1 ∈ E1

        PROVE c1 [2] [2][e1] = c2 [2] [1][e1]

        PROOF BY Clause_ASSM1

                 DEF PoliciesSet

⟨4⟩2 CASE c2 [2] [2][e1] = {NONE}

…

⟨4⟩3 CASE ∧ c2 [2] [2][e1] ∩ UU = {}

∧ c2 [2] [2][e1] ≠ {NONE}

…

⟨4⟩4 CASE ∧ c2 [2] [2][e1] ∩ UU ≠ {}

∧ c2 [2] [2][e1] ≠ {NONE}

…

⟨4⟩5 QED BY ⟨4⟩2, ⟨4⟩3, ⟨4⟩4

…

If , then, based on the fact that , definitions of compareClause(⋅) and matchLocks(⋅), and assumptions about representation of parametric locks in security policy clauses, admissible set of bound variables, and admissible set of actors, we have

…

⟨4⟩2 CASE c2 [2] [2][e1] = {NONE}

⟨5⟩1 ∨ c1 [2] [2][e1] = {NONE}

∨ (c1 [2] [2][e1] \ UU)

∪ {c2 [1]} ⊆ {NONE}

∨ (c1 [2] [2][e1] ⊆ {NONE}

PROOF BY ⟨3⟩3, ⟨4⟩2, Clause_ASSM1

           DEF

⟨5⟩2 c1 ∈ ClausesSet ∧ c2 ∈ ClausesSet

PROOF BY DEF PoliciesSet

⟨5⟩2 QED BY ⟨4⟩2, ⟨5⟩1, ⟨5⟩2,

Clause_ASSM3, Clause_ASSM1,

U_ASSM, UU_ASSM

…

Then, the proof of case ⟨4⟩2 is trivial. For brevity, below we only present the general structure of proofs for steps ⟨4⟩3 and ⟨4⟩4, for which the key steps are ⟨3⟩3, ⟨3⟩4, and ⟨3⟩6.

…

⟨4⟩3 CASE ∧ c2 [2] [2][e1] ∩ UU = {}

∧ c2 [2] [2][e1] ≠ {NONE}

⟨5⟩1 ∨ (c1 [2] [2][e1] \ UU) ∪ {c2 [1]}

⊆ c2 [2] [2][e1]

∨ c1 [2] [2][e1] ⊆ c2 [2] [2][e1]

…

⟨5⟩2 CASE c1 [2] [2][e1] ⊆ c2 [2] [2][e1]

…

⟨5⟩3 CASE (c1 [2] [2][e1] \ UU)

∪ {c2 [1]} ⊆ c2 [2] [2][e1]

…

⟨5⟩4 QED BY ⟨5⟩1, ⟨5⟩2, ⟨5⟩3

⟨4⟩4 CASE ∧ c2 [2] [2][e1] ∩ UU ≠ {}

∧ c2 [2] [2][e1] ≠ {NONE}

…

⟨5⟩9 c2 [2] [2][e1] ⊆ c1 [2] [2][e1]

…

⟨5⟩10 c1 [2] [2][e1] ⊆ c2 [2] [2][e1]

…

⟨5⟩11 QED BY ⟨5⟩9, ⟨5⟩10, UU_ASSM

…

The complete proof of the transitivity property for the relation comparePol(⋅) defined on PoliciesSet can be found in [6].

Lattice

Let us assume that the previously defined function is indeed a function for finding the least upper bound of two security policies and formulate as a theorem the statement that PoliciesSet with the partial order comparePol(⋅) defined on it is an algebraic lattice:

THEOREM ParalocksLattice

     ∀ p1, p2 ∈ PoliciesSet :

∧ comparePol(p1, LUB(p1, p2))

∧ comparePol (p2, LUB(p1, p2))

∧ ∀ y ∈ PoliciesSet :

∧ comparePol(p1, y)

∧ comparePol(p2, y)

⇒ comparePol(LUB(p1, p2), y)

It should be noted that, even on small datasets (two parametric locks, one non-parametric lock, one particular user in , and one bound variable in ), we failed to prove the theorem using the tool for evaluating expressions over TLA = Toolbox environment constants. At the preliminary stage, we had to use the TLC simulation tool. The following variables were chosen: Policies2Set is the set of all possible pairs of policies from PoliciesSet and is the current pair of policies. Function LUB(p1, p2) returned the least upper bound (if any) for a pair of policies and .

With a hierarchical proof being rather cumbersome, we confine ourselves only to its general structure. The steps of the proof are obvious:

⟨1⟩1 TAKE p1, p2 ∈ PoliciesSet

⟨1⟩2 LUB(p1, p2) ∈ PoliciesSet

      PROOF BY LUB_PS

⟨1⟩3 PICK l ∈ PoliciesSet : l = LUB(p1, p2)

      PROOF BY ⟨1⟩2

⟨1⟩4 ∀ l1 ∈ l :

           ∧ ∃ c1 ∈ p1 : compareClause(c1, l1)

           ∧ ∃ c2 ∈ p2 : compareClause(c2, l1)

⟨1⟩5 ∀ y ∈ PoliciesSet :

           comparePol(p1, y) ∧ comparePol(p2, y)

                                           ⇒ comparePol(l, y)

⟨1⟩6 QED BY ⟨1⟩3, ⟨1⟩4, ⟨1⟩5 DEF comparePol

The proof of step ⟨1⟩4 is based on the fact that any clause of policy is a result of applying some substitution to the locks of clause or with subsequent union of the locks of these clauses: unionCl(c1. c2), where and . For the general proof of step ⟨1⟩5, it is required to select an arbitrary policy y ∈ PoliciesSet and arbitrary clause and then prove that ∃c1, c2, l1 : c1 ∈ p1 ∧ c2 ∈ p2 ∧ l1 ∈ l ∧ :

…

⟨1⟩5 ∀ y ∈ PoliciesSet :

  comparePol(p1, y) ∧ comparePol(p2, y)

            ⇒ comparePol(l, y)

⟨2⟩1 TAKE y ∈ PoliciesSet

⟨2⟩2 SUFFICES ∀ y1 ∈ y :

     (∧ ∃ c1 ∈ p1 : compareClause(c1, y1)

       ∧ ∃ c2 ∈ p2 : compareClause(c2, y2)) ⇒

          ∃ l1 ∈ l : compareClause(l1, y1)

         PROOF BY ⟨1⟩3 DEF comparePol

⟨2⟩3 TAKE y1 ∈ y

⟨2⟩4 HAVE ∧ ∃ c1 ∈ p1 : compareClause(c1, y1)

         ∧ ∃ c2 ∈ p2 : compareClause(c2, y1)

⟨2⟩5 PICK c1 ∈ p1 : compareClause(c1, y1)

       PROOF BY ⟨2⟩4

⟨2⟩6 PICK c2 ∈ p2 : compareClause(c2, y1)

       PROOF BY ⟨2⟩4

…

Then, it is required to generate some clause u = and prove that (a) belongs to policy l = and (b) . Condition (b) requires decomposition into three subconditions in accordance with the definition of compareClause(⋅):

…

⟨2⟩9 PICK u : u = unionCl(c1, c2)

     PROOF OBVIOUS

…

⟨2⟩13 u ∈ l

     PROOF BY …

…

⟨2⟩16 u[1] ∈ UU ∨ u[1] = y1 [1]

     PROOF BY …

…

⟨2⟩24 ∀ k ∈ E0 : ∨ u[2] [1][k] = y1 [2] [1][k]

                        ∨ y1 [2] [1] [k] = {}

     PROOF BY

⟨2⟩25 ∀ e ∈ E1 :

∨ u[2] [2][e] = {NONE}

∨ matchLocks(u, y1, e) ⊆ y1 [2] [2][e]

⟨3⟩1 TAKE e ∈ E1

⟨3⟩2 CASE u[2] [2][e] = {NONE}

PROOF BY ⟨3⟩2

⟨3⟩3 CASE ∧ u[2] [2][e] ≠ {NONE}

                        ∧ u[2] [2][e] ∩ UU = {}

…

⟨3⟩4 CASE ∧ u[2] [2][e] ≠ {NONE}

∧ u[2] [2][e] ∩ UU ≠ {}

…

⟨3⟩5 QED BY ⟨3⟩2, ⟨3⟩3, ⟨3⟩4

⟨2⟩26 QED BY ⟨2⟩16, ⟨2⟩13, ⟨2⟩24, ⟨2⟩25

DEF compareClause, substMap3Equality

…

Here, the proof of step ⟨2⟩25 is the most time-consuming one and requires consideration of three cases. In general, the formal derivation of proofs for each of them is carried out in the same manner as the derivation of proofs for the similar steps in the statements considered above: the sequential verification of expressions for function compareClause(⋅), which are responsible for comparing parametric locks of security policy clauses, based on a certain number of reasonable assumptions.

CONCLUSIONS

Information flow control is one of the intensively developed directions in the theory of programming languages [12]. This paper continues a series of publications devoted to the technology (developed with author’s participation) for information flow control in enterprise-level automated information systems. Unlike well-known similar technologies that are based on methods of static and dynamic code analysis and require programmers to solve additional non-trivial problems associated with source code labeling and interpretation of code analysis results, the developed technology allows one to strictly separate the process of coding from checking the correctness of code logic, taking into account the specifics of a problem domain and adopted security policy.

This research is also of independent interest, since it offers a variant of description of Paralocks policies used in Java (Paragon project [11, 13]) in the TLA+ language, which is often used to model software applications and check their properties. Thus, the research takes a step towards creating an IFC platform based on methods of formal verification and model checking.

The idea of checking the security of information flows based on formal verification methods has previously been put forward and received certain recognition [14]. However, this paper presents only theoretical studies without relation to any particular programming language; the alphabet of security policies here is represented by a simple two-level lattice , .

Deriving the proofs for the formal properties of the lattice of expressions that constitute the alphabet of security policies is an important aspect in developing the IFC mechanism.

The proposed scenario of using the TLAPS formal logic system can be of practical interest. As noted above, many cumbersome proofs published in the literature contain incorrect statements. The human factor is responsible for the simplest errors. For instance, based on an established (given) fact of the form “P(x) holds for ∀x ∈ X,” the step “take x ∈ X for which P(x) holds” is often taken. This step is incorrect because it requires checking the additional condition “X is not empty.” Another example is the incorrect use of the facts of form x1 = if e1 then x2 else x3 and to prove some statement . In this case, the missing condition is ; its check can pose a challenge.

The use of tools such as TLAPS certainly requires additional time for translating proofs into TLA+ formulas. However, it provides stronger guarantees of the correctness of the results.

ACKNOWLEDGMENTS

The author expresses his gratitude to Jure Kukovec (Institute of Information Systems Engineering, Vienna, https://informatics.tuwien.ac.at/orgs/e194), one of the developers of the Apalache tool [10] designed to check TLA+ specifications based on symbolic execution, for his important recommendations on the optimization of individual functions and operators that form the TLA+ semantics of the adopted version of Paralocks. Even though, at this stage, it was not possible to fully adapt PLIF specifications to Apalache, the author believes that further efforts in this direction are promising and will be continued.

FUNDING

This work was supported by ongoing institutional funding. No additional grants to carry out or direct this particular research were obtained.

CONFLICT OF INTEREST

The author declares that he has no conflicts of interest.

1

To interpret traces that lead to errors, PLIF uses a simplified notation:

2

The proof is based on the definitions of functions comparePol(·), , , and .

Translated by Yu. Kornienko

Publisher’s Note.

Pleiades Publishing remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

REFERENCES

1 Devyanin, P.N., et al., Integration of mandatory and role-based access control and mandatory integrity control in a verified hierarchical model of operating system security, Tr. Inst. Sist. Program. Ross. Akad. Nauk (Proc. Inst. Syst. Program. Russ. Acad. Sci.), 2020, vol. 32, no. 1, pp. 7–26.

2 Lamport, L., Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002.

3 Denning, D.E., A lattice model of secure information flow, Commun. ACM, 1976, no. 5, pp. 236–243.

4 Broberg, N. and Sands, D., Paralocks: Role-based information flow control and beyond, Conf. Rec. Annu. ACM Symp. Principles of Programming Languages, 2010, pp. 431–444.

5 Myers, A.C. and Liskov, B., A decentralized model for information flow control, ACM SIGOPS Oper. Syst. Rev., 1997, no. 5, pp. 129–142.

6 Timakov, A.A., PLIF, 2021. https://github.com/timimin/plif.

7 Blanchette, J.C., Bulwahn, L., and Nipkow, T., Automatic proof and disproof in Isabelle/HOL, Proc. 8th Int. Symp. Frontiers of Combining Systems (FroCoS), Saarbrucken, Germany, 2011, pp. 12–27.

8 Bonichon, R.; Delahaye, D.; Doligez, D. Zenon: An extensible automated theorem prover producing checkable proofs. LPAR; 2007; 4790, pp. 151-165.

9 Lamport, L. How to write a proof. Am. Math. Mon.; 1995; 102, pp. 600-608.MathSciNet ID: 1349872[DOI: https://dx.doi.org/10.1080/00029890.1995.12004627]

10 Kukovec, J. and Konnov, I., Type inference for TLA in Apalache.

11 Broberg, N., Practical flexible programming with information flow control, Thesis for the Degree of Doctor of Engineering, 2011.

12 Korablin, Yu.P. Equivalence of program schemes based on an algebraic approach to specifying the semantics of programming languages. Russ. Technol. J.; 2022; 10, pp. 18-27. [DOI: https://dx.doi.org/10.32362/2500-316X-2022-10-1-18-27]

13 Broberg, N., van Delft, B., and Sands, D., Paragon for practical programming with information-flow control, Proc. 11th Asian Symp. Programming Languages and Systems (APLAS), Melbourne, 2013, pp. 217–232.

14 Clarkson, M.R. et al., Temporal logics for hyperproperties, Proc. 3rd Int. Conf. Principles of Security and Trust (POST), as part of Eur. Jt. Conf. Theory and Practice of Software (ETAPS), Grenoble, France, 2014, pp. 265–284.