Model-checking trace-based information flow properties for infinite-state systems

Abstract

We consider the problem of model-checking some of the well-known trace-based information flow properties from the literature for classes of infinite-state system models. We first define some language-theoretic operations that help to characterize language inclusion in terms of these properties. This gives us a reduction of the language inclusion problem for a class of system models, say $F$ , to the model checking problem for $F$ , whenever $F$ is effectively closed under these language-theoretic operations. We apply this result to show that the problem of model-checking any of these properties for One Counter Nets, One-Counter Automata, Basic Parallel Processes, and some properties for deterministic One Counter Automata, is undecidable. We also consider the class of Visibly Pushdown Systems and show that their model-checking problem is undecidable for a couple of properties. For the special case when all confidential events are internal we show that model-checking each of these properties for Visibly Pushdown Systems becomes decidable.

Keywords

Model-checking Petri net information flow security pushdown visibly pushdown deterministic pushdown one-counter

1. Introduction

Information flow properties are a way of specifying security properties of systems that originated in the work of Goguen and Meseguer in the 1980’s [12]. In this framework, a system is modelled as having high-level (or confidential) events as well as low-level (or public) events, and a typical property requires that the high-level events should not “influence” the occurrence of low-level events. In other words, the sequence of low-level events observed from a system execution, should not reveal “too much” information about the high-level events that may have taken place.

A variety of information flow properties have been proposed in the literature, falling broadly under three categories. The original formulation of non-interference by Goguen and Meseguer was state-based in the sense that it spoke about the state of the system after a sequence of events: the state reached by the system after executing a sequence of low and high-level events, must be the same (from the low-level observer’s point of view) as the state reached after executing only the low-level events in the sequence.

Subsequent information flow properties in the literature were trace-based in that they specify a property of the set of traces or executions produced by the system (such properties are termed “hyperproperties” in [6]). For example, the non-inference (NF) property [24,25,31] states that for every trace produced by the system, its projection to low-level events must also be a possible trace of the system. Other well-known properties include separability (SEP) [24], generalized non-interference (GNI) [23], non-deducibility (NDO) [26], forward correctability (FC) [18], generalized non-inference (GNF) [31] and perfect security property (PSP) [31].

Finally there are properties based on the structure of the system model. These properties are termed bisimulation-based information flow properties and are studied by Focardi and Gorrieri in [10].

Fig. 1.

A Petri net model of Alice’s financial transactions, and the induced labelled transition system. (a) Petri net model. (b) Induced labelled transition system.

To illustrate how an information-flow property can express a confidentiality property of a system, consider the following example where we would like to model and reason about the confidentiality of an individual’s financial transactions. Alice periodically receives a unit of salary. She may choose to invest a unit of her money, in which case she eventually gets back double her investment. She could also choose to spend a unit of the money with her. Let us say the events of Alice receiving her salary and her expenditures are publicly visible events, while her investments and returns are not. We could model this system as a Petri net as shown in Fig. 1(a). There are two places (P and Q) and four transitions (labelled “ $sal$ ”, “ $inv$ ”, “ $ret$ ”, and “ $\exp$ ”) in the model. The place P will represent (via the tokens that collect there) the money Alice has with her, while Q will represent the money she has currently invested. The $sal$ event represents Alice receiving her salary and generates one token (representing a unit of money) in place P, while the $\exp$ event represents an expenditure of one unit, and removes a token from place P. Similarly, the event $inv$ moves one token from place P to Q, while the event $ret$ removes one token from place Q and generates two in place P. The Petri net model induces an (infinite-state) labelled transition system (LTS) shown in Fig. 1(b).

We can now ask whether this LTS (with $sal$ and $\exp$ being the public or low events, and $inv$ and $ret$ being private or high events) satisfies the non-inference property: Does every trace of events generated by the system satisfy the property that its projection to low events is also a trace of the system? This system does not satisfy this property since the trace “ $sal \cdot inv \cdot ret \cdot \exp \cdot \exp$ ” is generated by the system, but its projection to public events “ $sal \cdot \exp \cdot \exp$ ” is not generated by the system. Thus, if a public observer who knows the system model observes the low-level trace “ $sal \cdot \exp \cdot \exp$ ”, he can infer that Alice must have made an investment and received returns on it.

A natural question that arises is whether these properties can be “model-checked” for different classes of system models. The problem of model-checking an information flow property P for a class of system models $F$ is the following: given an instance M of the class of models $F$ , does M satisfy P? The question we would like to answer asks whether there is a decision procedure for this problem for a given property P and a class of models $F$ .

The problem of model-checking each of the trace-based properties mentioned above is known to be decidable for finite-state systems [7,30]. The technique in [7] makes use of Mantel’s characterisation of these properties [20,21] in terms of Basic Security Predicates (BSP’s) and essentially reduces the problem to the language-inclusion problem (modulo some closure properties) of the class of models. The model-checking problem for pushdown systems (PDS) was also shown to be undecidable in [7] by showing a reduction from the emptiness problem for Turing machines. For bisimulation-based properties, the model-checking problem is known to be decidable for finite-state systems [3,11]. More recently this problem was shown to be undecidable for pushdown systems, Petri nets and process algebras in [8].

In this paper, we focus on the problem of model-checking the trace-based properties mentioned above for classes of infinite-state system models (like the Petri net model of Fig. 1(a)). We begin by proving a general result that says that the language-inclusion problem for a class of system models reduces to the model-checking problem for each of the trace-based properties for this class of models, provided the class of models is effectively closed under certain corresponding language-theoretic operations. This result can be thought of as a converse direction of the characterisation in [7], thus showing that the problems of language-inclusion and model-checking for a class of systems are closely related.

This general result can be used to show that the model-checking problem for each of the trace-based properties is undecidable for well-known classes of infinite-state systems like Petri nets and Pushdown Systems, by simply checking that (a) the language-inclusion problem is undecidable for them, and (b) that they are closed under the corresponding language-theoretic operations. In fact we apply this technique to classes of system models fairly low in the hierarchy of classes like Basic Parallel Processes (BPP) [5] which can be thought of as communication-free Petri nets, and One-Counter Nets (OCN). This lets us conclude that the model-checking problem (for each of the trace-based properties) is undecidable for these classes, as well as for any super-class of them like One-Counter Automata (OCA) (that extend OCN’s by allowing a zero-check), and Process Rewrite Systems (PRS) [22] (that can be viewed as extending Petri nets with subroutines), apart from Petri nets and Pushdown Systems.

Fig. 2.

Various classes of infinite-state system models, ordered by inclusion of the class of languages they define. The results in this paper imply that model-checking any of the trace-based properties is undecidable for the darkly shaded classes, while model-checking the properties NF and GNF is undecidable for the lightly shaded classes.

For the deterministic versions of some of these classes, like Deterministic Pushdown Systems (DPDS) and Deterministic One-Counter Automata (DOCA), we can apply our generic result only partially. This is because while the language-inclusion problem for these classes is known to be undecidable, they are closed only with respect to one of the required language-theoretic operations. This lets us conclude that the problem of model-checking the properties NF and GNF for these classes is undecidable, while the others remain open.

For the class of Visibly Pushdown Systems (VPS) [1], which are a well-known class of infinite-state systems contained in DPDS, our general result is not useful as the language-inclusion problem for VPS is decidable. Nevertheless we show that model-checking the properties of NF and GNF is undecidable for this class of systems, by showing a reduction from the language-inclusion problem of a PDS in a VPS, which in turn we show to be undecidable. We also consider a restricted problem for VPS where all confidential events are internal. In this case, we can use a similar route to the one for finite-state systems [7] to show that this restricted model-checking problem for VPS is decidable.

The undecidability results in this paper are depicted in Fig. 2 which shows the different classes of infinite-state models we consider, ordered by inclusion of the classes of languages they define. We have also shown the classes BPA representing Basic Process Algebra or Context-Free Processes [22], which can be seen to define the same class of languages as PDS; and Two-Counter Automata (TCA) (or Minsky Machines) that are Turing-complete. The darkly shaded classes all have undecidable model-checking problems for each of the trace-based properties, while the lightly-shaded ones have undecidable model-checking problems for the NF and GNF properties. Our results are summarised in Table 1. The entries “Not Dec”, and “?” stand for “not decidable” and “open” respectively.

Table 1

Summary of decidability results in this paper

Information flow property	System models

	OCN	BPP	DOCA	VPS	VPS (high events internal)
NF	Not Dec	Not Dec	Not Dec	Not Dec	EXPTIME-complete
SEP	Not Dec	Not Dec	?	?	EXPTIME-complete
GNI	Not Dec	Not Dec	?	?	EXPTIME-complete
NDO	Not Dec	Not Dec	?	?	EXPTIME-complete
FC	Not Dec	Not Dec	?	?	EXPTIME-complete
GNF	Not Dec	Not Dec	Not Dec	Not Dec	EXPTIME-complete
PSP	Not Dec	Not Dec	?	?	EXPTIME-complete

The rest of the article is organized as follows. Section 2 recalls the definitions of the different trace-based information flow properties in the literature. Section 3 defines the classes of system models studied in this paper. Section 4 characterises language-inclusion in terms of the satisfaction of trace-based properties. It also derives conditions under which the language inclusion problem for a class of system models reduces to the problem of model-checking trace-based properties for that class. Section 5 applies this result to show that this problem is undecidable for the class of basic parallel processes. Similarly Section 6 shows that the model-checking problem is undecidable for the classes DOCA and OCN. Sections 7 and 8 deal with the decidability results for Visibly Pushdown Systems. We conclude and point to some future directions in Section 9.

2. Trace-based information flow properties

We recall the definitions of some of the well-known trace-based information flow properties. As we are interested in addressing the verification problem in this paper, we only recall the definitions of these properties and point the reader to [21] and [10] for motivation and example applications.

We begin with some preliminary notions. We use $N$ to denote the set of nonnegative integers. By an alphabet we mean a finite set of symbols representing events or actions of a system. For an alphabet Σ we use $Σ^{*}$ to denote the set of finite strings over Σ. The null or empty string is represented by the symbol ϵ. For two strings u and v in $Σ^{*}$ we write $u \cdot v$ , or simply $u v$ , for the concatenation of u followed by v. A language over Σ is just a subset of $Σ^{*}$ . For languages $L_{1}$ and $L_{2}$ over Σ, the concatenation of $L_{1}$ followed by $L_{2}$ , denoted $L_{1} \cdot L_{2}$ is defined to be the language ${u \cdot v | u \in L_{1}, v \in L_{2}}$ . For $a \in Σ$ and $L \subseteq Σ^{*}$ , we sometimes write $a \cdot L$ for the language ${a} \cdot L$ . We will make use of standard notation for regular expressions. The prefix-closure of a language L over Σ, denoted $pref (L)$ , is the set ${u \in Σ^{*} | \exists v \in Σ^{*} : u \cdot v \in L}$ .

Let w be a string over an alphabet Σ, and let $X \subseteq Σ$ . Then $w ↾_{X}$ denotes the projection of w to X, namely the string obtained by deleting all events from w that are not elements of X. For alphabets $Σ_{1}$ and $Σ_{2}$ with $Σ_{1} \cap Σ_{2} = \emptyset$ , and $w_{1} \in Σ_{1}^{*}$ and $w_{2} \in Σ_{2}^{*}$ , we define the shuffle or interleaving of $w_{1}$ and $w_{2}$ , written $w_{1} ‖ w_{2}$ , to be the language over $Σ_{1} \cup Σ_{2}$ given by $\begin{matrix} w_{1} ‖ w_{2} = {w \in {(Σ_{1} \cup Σ_{2})}^{*} | w ↾_{Σ_{1}} = w_{1} and w ↾_{Σ_{2}} = w_{2}} . \end{matrix}$ For languages $L_{1} \subseteq Σ_{1}^{*}$ and $L_{2} \subseteq Σ_{2}^{*}$ with $Σ_{1} \cap Σ_{2} = \emptyset$ , we define $L_{1} ‖ L_{2} = ⋃_{w_{1} \in L_{1}, w_{2} \in L_{2}} w_{1} ‖ w_{2}$ .

Finally, a partitioned alphabet $(Σ, H, L, I, O)$ is a base alphabet Σ, along with a partition of Σ into $H$ (“High”) and $L$ (“Low”) events, and another partition of Σ into $I$ (“Input”) and $O$ (“Output”) events. We write $HI$ for $H \cap I$ and $LI$ for $L \cap I$ .

Definition 1.
Let $(Σ, H, L, I, O)$ be a partitioned alphabet, and let L be a language over Σ. We define below what it means for L to satisfy various trace-based information flow properties.
Non-inference (NF) [ 24 , 25 , 31 ] states that for every trace produced by the system, its projection to low events must also be a possible trace of the system. Thus if a system satisfies the non-inference information flow property, a low-level user who observes the visible behavior of the trace is unable to infer in general, the exact system trace. Formally, L satisfies NF iff $\begin{matrix} \forall τ \in L (τ ↾_{L} \in L) . \end{matrix}$

Separability (SEP) [ 24 ] requires that every possible low-level behavior interleaved with every possible high-level behaviour must be a possible behaviour of a system. Formally, L satisfies SEP iff $\begin{matrix} \forall τ_{1}, τ_{2} \in L ((τ_{1} ↾_{H}) ‖ (τ_{2} ↾_{L}) \subseteq L) . \end{matrix}$

Generalized non-interference (GNI) [ 23 ]: Given a trace τ, modifying it by inserting or deleting high-level input results in a sequence σ, which is not necessarily a valid trace. This is referred to as a perturbation of τ. GNI requires that it must be possible to construct a valid trace $τ^{'}$ from σ by inserting or deleting high-level outputs. This is called a correction to a perturbation. Formally, L satisfies GNI iff $\begin{matrix} \forall τ_{1}, τ_{2}, τ_{3} ((τ_{1} τ_{2} \in L \land τ_{2} ↾_{Σ ∖ HI} = τ_{3} ↾_{Σ ∖ HI}) \Rightarrow \exists τ_{4} (τ_{1} τ_{4} \in L \land τ_{4} ↾_{L \cup HI} = τ_{3} ↾_{L \cup HI})) . \end{matrix}$

Non-deducibility for outputs (NDO) [ 14 ] is similar to SEP, but weaker in that it permits some non-critical information flow from low level to high level. More specifically, the high-level behavior may depend on the input that is provided by low-level users. The possible user inputs are modelled by a set $UI \subseteq I$ . Formally, L satisfies NDO w.r.t. $UI$ iff $\begin{matrix} \forall τ_{1}, τ_{2} \in L ((τ_{1} ↾_{L}) ‖ (τ_{2} ↾_{H \cup (L \cap UI)}) \subseteq L) . \end{matrix}$

Forward correctability (FC) [ 18 ]: FC is a causal or forward correctable version of GNI where corrections can occur only after the perturbation. Formally, L satisfies FC iff $\begin{array}{l} \forall τ_{1}, τ_{2} \forall c \in HI \forall v^{'} \in LI \\ ((τ_{1} v^{'} τ_{2} \in L \land τ_{2} ↾_{HI} = ϵ) \Rightarrow \exists τ_{3} (τ_{1} c v^{'} τ_{3} \in L \land τ_{3} ↾_{L} = τ_{2} ↾_{L} \land τ_{3} ↾_{HI} = ϵ) \land \\ (τ_{1} c v^{'} τ_{2} \in L \land τ_{2} ↾_{HI} = ϵ) \Rightarrow \exists τ_{3} (τ_{1} v^{'} τ_{3} \in L \land τ_{3} ↾_{L} = τ_{2} ↾_{L} \land τ_{3} ↾_{HI} = ϵ)) . \end{array}$

Generalized non-inference (GNF) [ 31 ] is satisfied when for any trace τ, it must be possible to find another trace σ such that the low projections of τ and σ coincide, and σ has no high level inputs. Formally, L satisfies GNF iff $\begin{matrix} \forall τ \in L \exists σ \in L (σ ↾_{HI} = ϵ \land σ ↾_{L} = τ ↾_{L}) . \end{matrix}$

Perfect security property (PSP) [ 31 ]: PSP was proposed to address a limitation of SEP. SEP does not allow low-level users to influence high-level activity. PSP is proposed as the weakest property that does not allow a flow from high-level users to low-level users. L satisfies PSP iff $\begin{array}{l} (\forall τ \in L (τ ↾_{L} \in L)) \land \\ (\forall α, β ((α β \in L \land β ↾_{H} = ϵ) \Rightarrow \forall h \in H (α h \in L \Rightarrow α h β \in L))) . \end{array}$

For the reader interested in the relationship between these different properties, we point to Theorem 4.3.7 in [21], that details the relative strength of each of these properties.
3. System models

In this section we introduce some of the system models we consider and define the model-checking problem for them. We begin with labelled transition systems and some associated notation.

Definition 2.
A labelled transition system (LTS) M is a tuple $(Q, Σ, s, \to)$ where Q is a set of states, Σ is a set of labels, $s \in Q$ is the initial state and $\to \subseteq Q \times (Σ \cup {ϵ}) \times Q$ is a set of labelled transitions.

Let $M = (Q, Σ, s, \to)$ be an LTS. For states $p, q \in Q$ , and $c \in Σ \cup {ϵ}$ , we will sometimes write $p \overset{c}{\to} q$ for $(p, c, q) \in \to$ . For states $p, q \in Q$ and $w \in Σ^{}$ we represent the fact that there is a path from p to q labelled w in M, by $p \overset{w}{\Rightarrow} q$ , and define it as the smallest relation in $Q \times Σ^{} \times Q$ satisfying $p \overset{ϵ}{\Rightarrow} p$ for each $p \in Q$ ; and for each $p, q, r \in Q$ , $u \in Σ^{}$ , and $c \in Σ \cup {ϵ}$ , if $p \overset{u}{\Rightarrow} q$ and $q \overset{c}{\to} r$ then $p \overset{u \cdot c}{\Rightarrow} r$ . We can now define the trace language generated by M, denoted by $L (M)$ , as the set ${w \in Σ^{} | \exists q \in Q : s \overset{w}{\Rightarrow} q} .$ We note that $L (M)$ is always a prefix-closed language.

We say that M is deterministic if for each $p, q, r, t \in Q$ , $c \in Σ \cup {ϵ}$ , and $a \in Σ$ :

$p \overset{c}{\to} q$ and $p \overset{c}{\to} r$ implies $q = r$ ; and

$p \overset{a}{\to} q$ and $r \overset{ϵ}{\to} t$ implies $p \neq r$ .

We say that a formalism $F$ represents a class of system models if each of its instances N has a trace semantics in terms of an LTS $M_{N}$ (that is $L (N)$ is defined to be $L (M_{N})$ ).
Definition 3.
A one-counter automaton (OCA) (see [28]) consists of a finite-state control and a counter capable of storing an unbounded non-negative integer. Formally, a OCA N is a tuple $(Q, Σ, s, δ, δ_{0})$ where Q is a finite set of control states, Σ a finite alphabet of actions, s the starting control state, δ a transition relation of the form $δ \subseteq Q \times (Σ \cup {ϵ}) \times {- 1, 0, 1} \times Q$ , and $δ_{0}$ a “zero-test” transition relation of the form $δ_{0} \subseteq Q \times (Σ \cup {ϵ}) \times {0, 1} \times Q$ .

Let $N = (Q, Σ, s, δ, δ_{0})$ be a OCA. A configuration of N is a pair in $Q \times N$ , representing a control state and a valuation to the counter. The OCA N induces an LTS $M_{N} = (Q \times N, Σ, (s, 0), \to)$ , where the transition relation → is defined as follows: for every $p, q \in Q$ , $m, m^{'} \in N$ and $a \in Σ \cup {ϵ}$ , we have: $\begin{matrix} (p, m) \overset{a}{\to} (q, m^{'}) iff either (p, a, (m^{'} - m), q) \in δ, or m = 0 and (p, a, m^{'}, q) \in δ_{0} . \end{matrix}$

A OCA is called a one-counter net (OCN) if $δ_{0} = \emptyset$ , i.e., if the automaton cannot test if the counter is equal to 0. It is called a deterministic OCA, or DOCA, if the induced LTS is deterministic.

We now introduce the system model Basic Parallel Processes (BPP’s) (see [22]).
Definition 4.
Let $Const$ be a set of process constants. The class of process expressions over $Const$ is given by $\begin{matrix} E : : = ϵ ∣ X ∣ E ‖ E, \end{matrix}$ where ‘ϵ’ is the empty process, X ranges over $Const$ , and ‖ stands for parallel composition.

A Basic Parallel Process (BPP) N over a set of process constants $Const$ is a tuple $(P, Σ, Δ)$ where P is the initial process expression, Σ is an alphabet and Δ is a finite set of rules of the form $X \overset{c}{⟶} E$ where $X \in Const$ , $c \in Σ \cup {ϵ}$ and E is a process expression over $Const$ .

A BPP $N = (P, Σ, Δ)$ over $Const$ determines an LTS $M_{N} = (Q, Σ, P, \to)$ where the states in Q are process expressions over $Const$ and the transition → is the least relation satisfying the following structural operational semantics (SOS) rules: $\begin{matrix} \begin{matrix} \frac{(X \overset{c}{\to} E) \in Δ}{X \overset{c}{⟶} E} \frac{E \overset{c}{⟶} E^{'}}{E ‖ F \overset{c}{\to} E^{'} ‖ F} \frac{F \overset{c}{⟶} F^{'}}{E ‖ F \overset{c}{\to} E ‖ F^{'}} \end{matrix} \end{matrix}$ where $c \in Σ \cup {ϵ}$ .

Finally, we turn to pushdown systems and their variants. A pushdown system (PDS) (see [19]) is a structure $P = (Q, Σ, Γ, s, δ, ⊥)$ , where Q is a finite set of states, Σ is the input alphabet, Γ is the stack alphabet which contains a designated bottom-of-stack symbol ⊥, s is the start state, and δ a finite subset of $(Q \times (Σ \cup {ϵ}) \times Γ) \times (Q \times Γ^{})$ the transition relation. A transition of the form $((p, a, X), (q, B_{1} \dots B_{k}))$ , which we will sometimes write $(p, a, X) \to (q, B_{1} \dots B_{k})$ for clarity, with $k ⩾ 0$ , represents the following move of the PDS: in state p, on input a, and top of stack X, it can move to state q, pop X off the stack, and push in symbols $B_{k}$ , $B_{k - 1}$ , to $B_{1}$ (in that order) on the stack.

A pushdown system P above induces an LTS $M_{P}$ whose states are elements of $Q \times Γ^{}$ (called the configurations of P), the start state is $(s, ⊥)$ , and the transition relation is given by: $\begin{matrix} (p, X \cdot γ) \overset{c}{\to} (q, B_{1} \dots B_{k} \cdot γ) with X \in Γ and γ \in Γ^{}, \end{matrix}$ provided there exists a transition of the form $((p, c, X), (q, B_{1} \dots B_{k}))$ in δ.

A pushdown automaton* (PDA) is a pushdown system along with a set of final states $F \subseteq Q$ . The language accepted by a PDA P, denoted $L (P)$ , is the set of strings $w \in Σ^{}$ , for which there is a run on w in the induced LTS to an “accepting” configuration where the control state is in F.

A visibly pushdown system* [1] is a pushdown system where the alphabet Σ is partitioned into a call alphabet $Σ_{c}$ , a return alphabet $Σ_{r}$ and an internal alphabet $Σ_{int}$ , with the restriction that the system does a push operation on reading a character from the call alphabet, a pop operation on reading a character from the return alphabet, and does not modify the stack on reading a character from the internal alphabet. A more formal definition follows.
Definition 5.
A visibly pushdown system (VPS) is a tuple $V = (Q, Σ_{c}, Σ_{r}, Σ_{int}, Γ, s, δ, ⊥)$ where Q is a finite set of states, $Σ_{c}$ is a finite call alphabet, $Σ_{r}$ is a finite return alphabet, $Σ_{int}$ is a finite internal alphabet, Γ is a finite stack alphabet that contains a special bottom-of-stack symbol ⊥, $s \in Q$ is the initial state and $δ \subseteq (Q \times Σ_{c} \times Q \times (Γ ∖ {⊥})) \cup (Q \times Σ_{r} \times Γ \times Q) \cup (Q \times Σ_{int} \times Q)$ .

A VPS V induces an LTS $M_{V}$ defined in a similar way to that of a pushdown system. A transition $(q, a, q^{'}, A)$ where $a \in Σ_{c}$ and $A \neq ⊥$ , is called a push-transition and denotes that on reading a, A is pushed onto the stack and the control changes from state q to $q^{'}$ . Similarly, $(q, a, A, q^{'})$ where $a \in Σ_{r}$ is called a pop-transition and denotes that on reading input a with A on the top of the stack, the top of the stack is popped and the control state changes from q to $q^{'}$ ; the only exception being that if A is the bottom of stack symbol ⊥, then it is not popped. A transition $(q, a, q^{'})$ where $a \in Σ_{int}$ is called an internal-transition and denotes that on reading a there is no change to the stack and the control changes from state q to $q^{'}$ . In Section 8.1 we give a detailed example of a VPS that models a program with procedure calls.

The classes OCA, DOCA, OCN, DOCN, PDS and VPS all represent classes of system models. Given two classes of system models $F_{1}$ and $F_{2}$ , we say that $F_{2}$ is effectively as expressive as $F_{1}$ , if there is a computable map σ from $F_{1}$ to $F_{2}$ such that for any instance M of $F_{1}$ , $L (σ (M)) = L (M)$ .

We now define the model-checking problem for classes of system models.
Definition 6.
The problem of model-checking a trace-based information flow property θ for a class of system models $F$ , denoted by ${MC}_{F} (θ)$ , is the following: given an instance M of $F$ over an alphabet Σ and a partitioned alphabet $\tilde{Σ}$ based on Σ, does $L (M)$ satisfy θ with respect to $\tilde{Σ}$ ?

As usual, the language inclusion problem for a class of system models $F$ , denoted by ${LI}_{F}$ , is as follows: given two instances $M_{1}$ and $M_{2}$ of $F$ over an alphabet Σ, is $L (M_{1}) \subseteq L (M_{2})$ ?
4. Reducing language inclusion to model-checking

In this section we give sufficient conditions under which the problem of language inclusion for a class of system models reduces to the model-checking problem for that class. We begin with a characterization of language inclusion in terms of satisfaction of the trace-based information flow properties. For this purpose we first define some language-theoretic operations.

Definition 7.
Let $L_{1}$ , $L_{2}$ be languages over an alphabet Σ. Let k and v be distinct symbols outside Σ. We define the binary operations ${op}_{1}^{k}$ , ${op}_{2}^{k}$ , ${op}_{3}^{k}$ , ${op}_{4}^{k, v}$ , and ${op}_{5}^{k, v}$ on languages, as follows:
${op}_{1}^{k} (L_{1}, L_{2}) = (k \cdot L_{1}) \cup L_{2}$ .

${op}_{2}^{k} (L_{1}, L_{2}) = (k \cdot L_{1}) \cup (L_{2} ‖ k^{})$ .

${op}_{3}^{k} (L_{1}, L_{2}) = (k \cdot L_{1}) \cup L_{2} \cup (k \cdot L_{2})$ .

${op}_{4}^{k, v} (L_{1}, L_{2}) = (v \cdot L_{1}) \cup ((v \cdot L_{2}) ‖ k^{})$ .

${op}_{5}^{k, v} (L_{1}, L_{2}) = (k \cdot L_{1}) \cup ((L_{2} \cup {v}) ‖ k^{})$ .
We note that ${op}_{5}^{k, v} (L_{1}, L_{2})$ is similar to ${op}_{2}^{k} (L_{1}, L_{2})$ except that it also contains strings of the form $v ‖ k^{}$ .

For an alphabet Σ and distinct symbols k and v outside Σ, we define the partitioned alphabets $\begin{array}{l} {\tilde{Σ}}_{1} = (Σ \cup {k}, {k}, Σ, {k}, Σ), \\ {\tilde{Σ}}_{2} = (Σ \cup {k, v}, {k}, Σ \cup {v}, {k, v}, Σ), \\ {\tilde{Σ}}_{3} = (Σ \cup {k, v}, {k}, Σ \cup {v}, {k}, Σ \cup {v}) . \end{array}$ These alphabets are depicted in Fig. 3.

Fig. 3.
Partitioned alphabets ${\tilde{Σ}}_{1}$ , ${\tilde{Σ}}_{2}$ and ${\tilde{Σ}}_{3}$ .
Theorem 1.
Let $L_{1}$ and $L_{2}$ be two languages over an alphabet Σ. Then
$L_{1} \subseteq L_{2}$ iff ${op}_{1}^{k} (L_{1}, L_{2})$ satisfies NF over ${\tilde{Σ}}_{1}$ .

$L_{1} \subseteq L_{2}$ iff ${op}_{5}^{k, v} (L_{1}, L_{2})$ satisfies SEP over ${\tilde{Σ}}_{3}$ .

$L_{1} \subseteq L_{2}$ iff ${op}_{2}^{k} (L_{1}, L_{2})$ satisfies GNI over ${\tilde{Σ}}_{1}$ .

$L_{1} \subseteq L_{2}$ iff ${op}_{5}^{k, v} (L_{1}, L_{2})$ satisfies NDO (w.r.t. any $UI$ ) over ${\tilde{Σ}}_{3}$ .

$L_{1} \subseteq L_{2}$ iff ${op}_{4}^{k, v} (L_{1}, L_{2})$ satisfies FC over ${\tilde{Σ}}_{2}$ .

$L_{1} \subseteq L_{2}$ iff ${op}_{1}^{k} (L_{1}, L_{2})$ satisfies GNF over ${\tilde{Σ}}_{1}$ .

$L_{1} \subseteq L_{2}$ iff ${op}_{3}^{k} (L_{1}, L_{2})$ satisfies PSP over ${\tilde{Σ}}_{1}$ .

Proof.

Let $L = {op}_{1}^{k} (L_{1}, L_{2}) = (k \cdot L_{1}) \cup L_{2}$ . (⇒:) Suppose $L_{1} \subseteq L_{2}$ . Let $w \in L$ . If $w \in L_{2}$ , then $w = w ↾_{L}$ , as there are no $HI$ events in $L_{2}$ , and hence $w ↾_{L} \in L$ . If $w \notin L_{2}$ , then it is of the form $k \cdot w^{'}$ for some $w^{'} \in L_{1}$ . Since $L_{1} \subseteq L_{2}$ , we have $w ↾_{L} = w^{'} \in L_{2}$ , and hence $w ↾_{L} \in L$ . Thus L satisfies NF over ${\tilde{Σ}}_{1}$ .

(⇐:) Suppose $L_{1} ⊈ L_{2}$ . Then there exists some $w \in L_{1}$ such that $w \notin L_{2}$ . Consider the string $k w \in L$ . We have $k w ↾_{L} = w$ which is not in L. Hence L does not satisfy NF with respect to ${\tilde{Σ}}_{1}$ .

Let $L = {op}_{5}^{k, v} (L_{1}, L_{2}) = (k \cdot L_{1}) \cup ((L_{2} \cup {v}) ‖ k^{})$ . (⇒:) Suppose $L_{1} \subseteq L_{2}$ . Consider $τ_{1}, τ_{2} \in L$ . We proceed case by case:
Case: $τ_{1}, τ_{2} \in k \cdot L_{1}$ . Then $τ_{1} ↾_{H} = k$ and $τ_{2} ↾_{L} = w$ for some $w \in L_{1}$ . Hence $(τ_{1} ↾_{H}) ‖ (τ_{2} ↾_{L}) = k ‖ w$ which is contained in $L_{2} ‖ k^{}$ since w is also in $L_{2}$ .

Case: $τ_{1}, τ_{2} \in (L_{2} \cup {v}) ‖ k^{}$ . Then $τ_{1} ↾_{H} \in k^{}$ and $τ_{2} ↾_{L} = v$ or $τ_{2} ↾_{L} = w$ for some $w \in L_{2}$ . Hence $(τ_{1} ↾_{H}) ‖ (τ_{2} ↾_{L}) \subseteq k^{} ‖ {v, w}$ which is contained in $(L_{2} \cup {v}) ‖ k^{}$ since w is also in $L_{2}$ .

Case: $τ_{1} \in k \cdot L_{1}$ and $τ_{2} \in (L_{2} \cup {v}) ‖ k^{}$ . Then $τ_{1} ↾_{H} = k$ and $τ_{2} ↾_{L} = v$ or $τ_{2} ↾_{L} = w$ for some $w \in L_{2}$ . Hence $(τ_{1} ↾_{H}) ‖ (τ_{2} ↾_{L}) \subseteq k ‖ {v, w}$ which is contained in $(L_{2} \cup {v}) ‖ k^{}$ .

Case: $τ_{1} \in (L_{2} \cup {v}) ‖ k^{}$ and $τ_{2} \in k \cdot L_{1}$ . Then $τ_{1} ↾_{H} \in k^{}$ and $τ_{2} ↾_{L} = w$ for some $w \in L_{1}$ . Hence $(τ_{1} ↾_{H}) ‖ (τ_{2} ↾_{L}) \subseteq k^{} ‖ w$ which is contained in $(L_{2} \cup {v}) ‖ k^{}$ since w is also in $L_{2}$ .
This proves that L satisfies SEP over ${\tilde{Σ}}_{3}$ .

(⇐:) Suppose $L_{1} ⊈ L_{2}$ . Then there exists some $w \in L_{1}$ such that $w \notin L_{2}$ . Consider the strings $v k k$ and $k w$ in L. Then $(v k k ↾_{H}) ‖ (k w ↾_{L}) = k k ‖ w$ contains the string $w k k$ which is not in L. Thus L does not satisfy SEP over ${\tilde{Σ}}_{3}$ .

For the partitioned alphabet ${\tilde{Σ}}_{1}$ (note that $HO = \emptyset$ and $HI = {k}$ ), GNI may be simplified to the following property. $\begin{matrix} \forall τ_{1}, τ_{2}, τ_{3} ((τ_{1} τ_{2} \in L \land τ_{2} ↾_{Σ} = τ_{3} ↾_{Σ}) \Rightarrow τ_{1} τ_{3} \in L) . \end{matrix}$ Let $L = {op}_{2}^{k} (L_{1}, L_{2}) = (k \cdot L_{1}) \cup (L_{2} ‖ k^{})$ . (⇒:) Suppose $L_{1} \subseteq L_{2}$ . Let $τ_{1} τ_{2} \in L$ .
Case $τ_{1} τ_{2} \in k \cdot L_{1}$ . Then $τ_{1} τ_{2} = k w_{1}$ for some $w_{1} \in L_{1}$ . In this case for any $τ_{3} \in τ_{2} ‖ k^{}$ , we have $τ_{1} τ_{3} \in w_{1} ‖ k^{}$ which is contained in $L_{2} ‖ k^{}$ since $w_{1} \in L_{1} \subseteq L_{2}$ .

Case $τ_{1} τ_{2} \in L_{2} ‖ k^{}$ . Then $τ_{1} τ_{2} \in w_{2} ‖ k^{}$ for some $w_{2} \in L_{2}$ . In this case for any $τ_{3} \in τ_{2} ‖ k^{}$ , we have $τ_{1} τ_{3} \in w_{2} ‖ k^{}$ which is contained in $L_{2} ‖ k^{}$ .
Hence L satisfies GNI over ${\tilde{Σ}}_{1}$ .

(⇐:) Suppose $L_{1} ⊈ L_{2}$ . Then there exists some $w \in L_{1}$ such that $w \notin L_{2}$ . Consider the strings $τ_{1} = k$ , $τ_{2} = w$ , and $τ_{3} = w k$ . Then $τ_{1} τ_{2} \in L$ , but $τ_{1} τ_{3} = k w k$ which does not belong to L. Hence L does not satisfy GNI over ${\tilde{Σ}}_{1}$ .

Let $UI$ be a subset of $I$ . As $L \cap I = \emptyset$ in ${\tilde{Σ}}_{3}$ , we have $L \cap UI = \emptyset$ . Hence over the partitioned alphabet ${\tilde{Σ}}_{3}$ , NDO (w.r.t. any $UI$ ) is equivalent to the SEP, and the claim follows from the one for SEP.

The property FC is vacuously satisfied when $LI = \emptyset$ . Hence we use the partitioned alphabet ${\tilde{Σ}}_{2}$ where $LI \neq \emptyset$ . Let $L = {op}_{4}^{k, v} (L_{1}, L_{2}) = (v \cdot L_{1}) \cup ((v \cdot L_{2}) ‖ k^{})$ .

(⇒:) Suppose $L_{1} \subseteq L_{2}$ . Then clearly $v \cdot L_{1} \subseteq (v \cdot L_{2}) ‖ k^{}$ , and we have $L = (v \cdot L_{2}) ‖ k^{}$ . Hence it is enough to prove that $(v \cdot L_{2}) ‖ k^{}$ independently satisfies FC. Consider a string $τ_{1} v τ_{2}$ in $(v \cdot L_{2}) ‖ k^{}$ with no k-events in $τ_{2}$ and $v \in LI$ . Then clearly $τ_{1} k v τ_{2}$ is also in $(v \cdot L_{2}) ‖ k^{}$ . Now consider a string $τ_{1} k v τ_{2}$ in $(v \cdot L_{2}) ‖ k^{}$ . Once again, we clearly have $τ_{1} v τ_{2}$ in $(v \cdot L_{2}) ‖ k^{}$ . Hence L satisfies FC over ${\tilde{Σ}}_{2}$ .

(⇐:) Suppose $L_{1} ⊈ L_{2}$ . Then there exists a string w in $L_{1}$ and not in $L_{2}$ . Consider the string $v w$ in L. If L were to satisfy FC, we must have $k v w$ also in L. But clearly, $k v w$ does not belong to $v \cdot L_{1}$ nor $(v \cdot L_{2}) ‖ k^{}$ . Hence $k v w \notin L$ . Consequently L does not satisfy FC over ${\tilde{Σ}}_{2}$ .

The property GNF is the same as NF when $HO = \emptyset$ . Hence the arguments in the proof of NF holds here as well.

Let $L = {op}_{3}^{k} (L_{1}, L_{2}) = (k \cdot L_{1}) \cup L_{2} \cup (k \cdot L_{2})$ .

(⇒:) Suppose $L_{1} \subseteq L_{2}$ . Consider a string $τ \in L$ . It is easy to see that $τ ↾_{L} \in L$ . Now consider α, β in ${(Σ \cup {k, v})}^{}$ and $h \in H$ such that $α β \in L$ , $β ↾_{H} = ϵ$ , and $α h \in L$ . This can only happen when $h = k$ and $α = ϵ$ . This implies that $β \in L_{2}$ . Now $α h β = k β$ which belongs to $k \cdot L_{2}$ which is contained in L. Hence L satisfies PSP with respect to ${\tilde{Σ}}_{1}$ .

(⇐:) Suppose $L_{1} ⊈ L_{2}$ . Then there exists some $τ \in L_{1} ∖ L_{2}$ . Consider the string $k τ \in L$ . We have $k τ ↾_{L} = τ$ , and clearly $τ \notin L$ . Hence L does not satisfy PSP over ${\tilde{Σ}}_{1}$ . □

The following theorem gives sufficient conditions for a class of system models under which the problem of language inclusion reduces to the problem of model-checking a particular trace-based property for that class. We use the notation $L I_{F} ⪯ M C_{F} (θ)$ to denote that the language inclusion problem for a class of system models $F$ reduces to the problem of model-checking property θ for $F$ . We say a class of system models $F$ is effectively closed* under the language-theoretic operation ${op}_{1}$ if and only if given two instances $M_{1}$ , $M_{2}$ of $F$ over an alphabet Σ and given $k \notin Σ$ there is an algorithm to construct an instance M of $F$ such that $L (M) = {op}_{1}^{k} (L (M_{1}), L (M_{2}))$ . Closure with respect to the other operations is defined similarly.
Theorem 2.
Let $F$ be a class of system models. Then
$L I_{F} ⪯ M C_{F} (NF)$ provided $F$ is effectively closed under ${op}_{1}$ .

$L I_{F} ⪯ M C_{F} (SEP)$ provided $F$ is effectively closed under ${op}_{5}$ .

$L I_{F} ⪯ M C_{F} (GNI)$ provided $F$ is effectively closed under ${op}_{2}$ .

$L I_{F} ⪯ M C_{F} (NDO)$ provided $F$ is effectively closed under ${op}_{5}$ .

$L I_{F} ⪯ M C_{F} (FC)$ provided $F$ is effectively closed under ${op}_{4}$ .

$L I_{F} ⪯ M C_{F} (GNF)$ provided $F$ is effectively closed under ${op}_{1}$ .

$L I_{F} ⪯ M C_{F} (PSP)$ provided $F$ is effectively closed under ${op}_{3}$ .

Proof.
Consider part (a) of the theorem. Let $M_{1}$ and $M_{2}$ be two instances of $F$ over an alphabet Σ. Suppose $F$ is effectively closed under ${op}_{1}$ . Let k be a distinct symbol outside Σ. Then we can construct an instance M of $F$ over the alphabet $Σ \cup {k}$ , such that $L (M) = {op}_{1}^{k} (L (M_{1}), L (M_{2}))$ . Now from Theorem 1, we have that $L (M_{1}) \subseteq L (M_{2})$ if and only if $L (M)$ satisfies NF over ${\tilde{Σ}}_{1}$ . Hence $L I_{F} ⪯ M C_{F} (NF)$ .

The proofs for parts (b) to (g) follow similarly. □

The following proposition is immediate:
Proposition 1.
Let $F_{1}$ and $F_{2}$ be two classes of system models. If $F_{2}$ is effectively as expressive as $F_{1}$ then ${MC}_{F_{1}} (θ)$ reduces to ${MC}_{F_{2}} (θ)$ for any information flow security property θ of Definition 1 .
Corollary 1.
If the problem of model-checking a system model $F$ for an information flow property θ of Definition 1 is undecidable, then the problem of model-checking any more-expressive system model $F^{'}$ than $F$ (i.e., $F \subseteq F^{'}$ ) for θ is also undecidable.
5. Model-checking basic parallel processes

We now apply the results of the previous section to show that the problem of model-checking each of the trace-based properties of Definition 1 for BPP’s is undecidable. The language inclusion problem for BPP’s is known to be undecidable [15]. Using Theorem 2, it is sufficient to show that BPP’s are effectively closed under the operations ${op}_{1}$ through ${op}_{5}$ .

For the rest of the section, we fix the BPP’s $N_{1} = (P_{1}, Σ, Δ_{1})$ over ${Const}_{1}$ and $N_{2} = (P_{2}, Σ, Δ_{2})$ over ${Const}_{2}$ such that ${Const}_{1} \cap {Const}_{2} = \emptyset$ . Let k and v be distinct symbols outside of Σ.

We now construct a BPP N from $N_{1}$ and $N_{2}$ such that $L (N) = {op}_{1}^{k} (L (N_{1}), L (N_{2}))$ . Let $N = (P, Σ \cup {k}, Δ)$ over ${Const}_{1} \cup {Const}_{2} \cup {P}$ where $P \notin {Const}_{1} \cup {Const}_{2}$ , and Δ contains the rules of $Δ_{1}$ , $Δ_{2}$ and the rules $P \overset{k}{\to} P_{1}$ and $P \overset{ϵ}{\to} P_{2}$ . Figure 4(a) depicts the induced LTS of the constructed BPP N. From the construction, it is straight-forward to see that $L (N) = {op}_{1}^{k} (L (N_{1}), L (N_{2}))$ .

Fig. 4.

Closure of BPP under operations ${op}_{1}$ and ${op}_{2}$ . (a) Induced LTS of N for ${op}_{1}$ . (b) Induced LTS of $N^{'}$ for ${op}_{2}$ .

We now construct a BPP $N^{'}$ from $N_{1}$ and $N_{2}$ such that $L (N^{'}) = {op}_{2}^{k} (L (N_{1}), L (N_{2}))$ . Let $N^{'} = (P, Σ \cup {k}, Δ)$ over ${Const}_{1} \cup {Const}_{2} \cup {P}$ where ${P} \cap ({Const}_{1} \cup {Const}_{2}) = \emptyset$ and Δ is defined as follows. $\begin{matrix} Δ = Δ_{1} \cup Δ_{2} \cup \{\begin{matrix} P \overset{k}{\to} P_{1}, \\ P \overset{ϵ}{\to} P_{2}, \\ X \overset{k}{\to} X & for every X \in {Const}_{2} \end{matrix}\} . \end{matrix}$

Figure 4(b) shows the induced LTS of the constructed BPP $N^{'}$ partially. It is easy to see that $L (N^{'}) = {op}_{2}^{k} (L (N_{1}), L (N_{2}))$ .

We now construct a BPP $N^{″}$ from $N_{1}$ and $N_{2}$ such that $L (N^{″}) = {op}_{3}^{k} (L (N_{1}), L (N_{2}))$ . Let $N^{″} = (P, Σ \cup {k}, Δ)$ over ${Const}_{1} \cup {Const}_{2} \cup {P}$ where $P \notin {Const}_{1} \cup {Const}_{2}$ and Δ is defined as follows. $\begin{matrix} Δ = Δ_{1} \cup Δ_{2} \cup \{\begin{matrix} P \overset{k}{\to} P_{1}, \\ P \overset{k}{\to} P_{2}, \\ P \overset{ϵ}{\to} P_{2} \end{matrix}\} . \end{matrix}$

Figure 5(a) shows the induced LTS of the constructed BPP $N^{″}$ . It is easy to see that $L (N^{″}) = {op}_{3}^{k} (L (N_{1}), L (N_{2}))$ .

We now construct a BPP $N^{‴}$ from $N_{1}$ and $N_{2}$ such that $L (N^{‴}) = {op}_{4}^{k, v} (L (N_{1}), L (N_{2}))$ . Let $N^{‴} = (P, Σ \cup {k, v}, Δ)$ over ${Const}_{1} \cup {Const}_{2} \cup {P, P^{'}}$ where ${P, P^{'}} \cap ({Const}_{1} \cup {Const}_{2}) = \emptyset$ and Δ is defined as follows. $\begin{matrix} Δ = Δ_{1} \cup Δ_{2} \cup \{\begin{matrix} P \overset{v}{\to} P_{1}, \\ P \overset{ϵ}{\to} P^{'}, \\ P^{'} \overset{v}{\to} P_{2}, \\ X \overset{k}{\to} X & for every X \in {Const}_{2} \cup {P^{'}} \end{matrix}\} . \end{matrix}$

Fig. 5.

Closure of BPP under operations ${op}_{3}$ and ${op}_{4}$ . (a) Induced LTS of $N^{″}$ for ${op}_{3}^{k}$ . (b) Induced LTS of $N^{‴}$ for ${op}_{4}^{k, v}$ .

Figure 5(b) depicts the induced LTS of the constructed BPP $N^{‴}$ . Note that the last rule enables us to have arbitrary number of k’s at arbitrary positions in the strings from the language $v \cdot L (N_{2})$ . Clearly, $L (N^{‴}) = {op}_{4}^{k, v} (L (N_{1}), L (N_{2}))$ .

The construction for ${op}_{5}^{k, v} (L (N_{1}), L (N_{2}))$ is very similar to that of ${op}_{2}$ and we skip the details.

Now from Theorem 2, it follows that:

Theorem 3.

The problem of model-checking any of the trace-based properties of Definition 1 for BPP’s is undecidable.

As a BPP can be viewed as a Petri net where every transition has exactly one input place and every arc has weight 1, from Corollary 1, we have:

Theorem 4.

The problem of model-checking any of the trace-based properties of Definition 1 for Petri nets is undecidable.

6. Model-checking one-counter nets/automata

In this section we apply Theorem 2 to the model-checking problem for deterministic one-counter automata (DOCA’s) and one-counter nets (OCN’s). We then extend these results to the problem of model-checking pushdown systems.

The language inclusion problem for OCN is shown to undecidable in [16]. We now show that the OCN class of models is closed under the operations ${op}_{1}$ through ${op}_{5}$ . Let Σ be an alphabet and let k and v be distinct symbols outside Σ. Let $N_{1}$ and $N_{2}$ be two OCN’s over Σ, with start states $s_{1}$ and $s_{2}$ respectively.

Consider the operation ${op}_{1}$ . We construct a OCN N from $N_{1}$ and $N_{2}$ by adding a new transition from $s_{2}$ to $s_{1}$ on k without modifying the counter, i.e., $(s_{2}, k, 0, s_{1})$ . Without loss of generality assume that the start state $s_{2}$ has no incoming transitions. The state $s_{2}$ is the starting state in N. Now it is easy to see that $L (N) = {op}_{1}^{k} (L (N_{1}), L (N_{2}))$ .

Next we consider the operation ${op}_{2}$ . We construct a OCN N from $N_{1}$ and $N_{2}$ by adding a new start state s, and transitions $(s, k, 0, s_{1})$ , $(s, ϵ, 0, s_{2})$ . We also add the transitions $(q, k, 0, q)$ for each state q in $N_{2}$ . The OCN N clearly accepts ${op}_{2}^{k} (L (N_{1}), L (N_{2}))$ .

Consider the language-theoretic operation ${op}_{3}$ . We construct a OCA N from $N_{1}$ and $N_{2}$ as follows. Introduce a new start state s and transitions $(s, k, 0, s_{1})$ , $(s, k, 0, s_{2})$ and $(s, ϵ, 0, s_{2})$ . Retain all the transitions from $N_{1}$ and $N_{2}$ in N. Now it is easy to see that $L (N) = {op}_{3}^{k} (L (N_{1}), L (N_{2}))$ .

Finally, we consider the language-theoretic operation ${op}_{4}$ . We construct a OCN N from $N_{1}$ and $N_{2}$ as follows. Introduce a new start state s and states $s_{1}^{'}$ and $s_{2}^{'}$ , and transitions $(s, ϵ, 0, s_{1}^{'})$ , $(s_{1}^{'}, v, 0, s_{1})$ , $(s, ϵ, 0, s_{2}^{'})$ , $(s_{2}^{'}, k, 0, s_{2}^{'})$ and $(s_{2}^{'}, v, 0, s_{2})$ . For all the states in $N_{2}$ , introduce a self loop on k without modifying the counter, i.e., if q is a state in $N_{2}$ , then add the transition $(q, k, 0, q)$ . Retain all the transitions from $N_{1}$ and $N_{2}$ in N. Now it is easy to see that $L (N) = {op}_{4}^{k, v} (L (N_{1}), L (N_{2}))$ .

The construction for ${op}_{5}$ is very similar to that of ${op}_{2}$ and we skip the details. Hence, using Theorem 2 we have:

Theorem 5.
The problem of model-checking any of the trace-based properties of Definition 1 for the class OCN is undecidable.

Since OCN is a syntactic subclass of OCA which in turn is a subclass of pushdown systems (PDS), from Corollary 1, we have:
Theorem 6.
The problem of model-checking any of the trace-based properties of Definition 1 for one-counter automata (OCA) and pushdown systems (PDS) is undecidable.

Finally, we consider some deterministic subclasses of pushdown systems. It is known that the language inclusion problem for deterministic one-counter automata (DOCA) is undecidable [29] (see also [28]). We note that the construction for ${op}_{1}$ shown above holds even for DOCA’s. This means that the class DOCA is closed under the operation ${op}_{1}$ . From Theorem 2 we then have:
Theorem 7.
The problem of model-checking the properties NF and GNF for deterministic one-counter automata (DOCA) is undecidable.

Since DOCA is an effective subclass of deterministic pushdown systems (DPDS), we have that
Corollary 2.
The problem of model-checking the properties NF and GNF for deterministic pushdown systems (DPDS) is undecidable.

Unfortunately, the decidability of the model-checking problems for the other properties for DOCA and DPDS remains open. We note that Theorem 2 is of little help in establishing undecidability in this case, since both DOCA and DPDS are not closed under the operations ${op}_{2}$ through ${op}_{5}$ . This can be seen by considering the language $L_{1} = pref ({a^{l} b^{m} c^{n} d | l \neq m})$ and $L_{2} = pref ({a^{l} b^{m} c^{n} d | m \neq n})$ , over the alphabet ${a, b, c, d}$ , which are both expressible as DOCA’s (and hence also DPDS’s). Note that $\begin{matrix} \overline{{op}_{2}^{k} (L_{1}, L_{2})} \cap k a^{} b^{} c^{*} d = {k a^{n} b^{n} c^{n} d | n ⩾ 0} . \end{matrix}$ Hence, if ${op}_{2} (L_{1}, L_{2})$ were expressible by a DOCA or DPDS, then since the class DPDS is closed under complementation and intersection with regular languages, we would have that the language ${k a^{n} b^{n} c^{n} d | n ⩾ 0}$ is expressible by a DPDS. But this is not possible, since the language is not even context-free. A similar argument can be used to show that the classes are not closed under the operations ${op}_{3}$ , ${op}_{4}$ and ${op}_{5}$ .
7. Model-checking visibly pushdown systems

We now study the model-checking problem for visibly pushdown systems. We show that this problem is undecidable in general for non-inference and generalized non-inference. We also show that a restricted problem of model-checking any of the properties in Definition 1, for visibly pushdown systems in which all the high events are internal, is decidable. In this section we focus on the undecidability result.

We note that the language inclusion problem for visibly pushdown automata (when the two VPA’s are over the same partitioned alphabet) is decidable [1], and hence we cannot directly make use of Theorem 2 for this class of system models. Instead, we will prove and make use of the fact that the problem of language inclusion of a PDS with respect to a VPS (i.e., whether the language of a given PDS P is contained in the language of a given VPS V) is undecidable. More precisely we show the following:

Theorem 8.
The problem of language inclusion of an ϵ-free PDS with respect to a VPS is co-r.e. hard.

We prove this theorem in three steps:

We reduce the complement of the halting problem of a Turing machine ( $\neg HP$ ) to the problem of checking the emptiness of the intersection of a PDA with a VPA (see Lemma 1).

We reduce the problem of checking the emptiness of the intersection of a PDA with a VPA to the problem of language inclusion of a PDA with respect to a VPA (see Lemma 2).

We reduce the problem of language inclusion of a PDA with respect to a VPA to the problem of language inclusion of an ϵ-free PDS with respect to a VPS (see Lemma 3).

We now describe these steps in detail. We recall that a Turing machine M is of the form $\begin{matrix} (Q, Σ_{M}, Γ_{M}, ⊢, ♭, δ, s, t, r), \end{matrix}$ where Q is a finite set of states, $Σ_{M}$ is a finite input alphabet, $Γ_{M}$ is a finite tape alphabet containing $Σ_{M}$ , $⊢ \in Γ_{M} ∖ Σ_{M}$ is the left end-marker, $♭ \in Γ_{M} ∖ Σ_{M}$ is the blank symbol, $δ : (Q \times Γ_{M}) \to (Q \times Γ_{M} \times {L, R})$ is the transition function, $s \in Q$ is the start state, and $t, r \in Q$ are respectively the accept and reject states which are assumed to be sink states. A configuration c of M at any instant is defined as a triple $(q, z, n)$ where $q \in Q$ is a state, z is a string describing the “non-blank” part of the tape contents, and n is a non-negative integer representing the position of the head of the Turing machine. The initial configuration of M on input x is $(s, ⊢ x, 0)$ , and the next configuration relation ⇝ is defined as follows: We have $(p, y a w, n) ⇝ (q, y b w, n + 1)$ , if $δ (p, a) = (q, b, R)$ and $| y | = n$ . Similarly $(p, y a w, n) ⇝ (q, y b w, n - 1)$ , when $δ (p, a) = (q, b, L)$ and $| y | = n$ . A configuration of M is halting if the control state is either t or r.

The halting problem for Turing machines is represented by the language $HP$ comprising (a suitable encoding of) a Turing machine M and its input x such that M reaches a halting configuration on input x. As is well-known, the problem $HP$ is undecidable and its complement $\neg HP$ is co-r.e. complete.

We now show a reduction from $\neg HP$ to the problem of emptiness of the intersection of a PDA and a VPA. The reduction follows the general idea of representing valid computations of a Turing machine as strings (see for example [19]), and is similar to the reduction one would use for showing undecidability of the emptiness of the intersection of the languages accepted by two given PDA’s. We represent a configuration of M as a finite string c over the alphabet $Δ_{M} = Γ_{M} \times (Q \cup {-})$ . For example the initial configuration of M on input $a a b a$ would be represented as the string $\begin{matrix} \overset{⊢}{s} \overset{a}{-} \overset{a}{-} \overset{b}{-} \overset{a}{-}, \end{matrix}$ where we write an element $(a, q)$ of Δ vertically stacked as ‘ $\begin{matrix} \overset{a}{q} \end{matrix}$ ’.

We now represent a computation of M on an input x as a sequence of configurations $c_{i}$ separated by a # symbol. More precisely, let $Δ_{M}^{'} = Γ_{M}^{'} \times (Q \cup {-})$ , where $Γ_{M}^{'} = {a^{'} | a \in Γ}$ , be a “primed” version of $Δ_{M}$ . Let $c^{'}$ denote the representation of a configuration c in the primed alphabet $Δ_{M}^{'}$ . Let $y^{R}$ denote the reverse of a string y. Then we represent the valid computations of M on x as a string over of the form: $\begin{matrix} c_{1}^{'} # c_{2}^{R} # c_{3}^{'} # c_{4}^{R} # \dots # c_{2 n}^{R}, \end{matrix}$ over the alphabet $Δ = Δ_{M} \cup Δ_{M}^{'} \cup {#}$ , satisfying the conditions that
$c_{1}$ is the initial configuration of M on x,

$c_{i} ⇝ c_{i + 1}$ , for each $i : 1 ⩽ i < 2 n$ ,

and $c_{2 n}$ is a halting configuration of M.
Such a string is depicted in Fig. 6. Let us call the collection of such strings over the alphabet Δ, the language ${Valcomps}_{M, x}$ . It is clear that M halts on x iff ${Valcomps}_{M, x}$ is non-empty.

Fig. 6.
Representing a computation of M on x.

Let ${Valcomps}_{M, x}^{odd}$ be a version of ${Valcomps}_{M, x}$ in which only the odd-numbered configurations and their successors are checked for consecution (i.e. $c_{2 i - 1} ⇝ c_{2 i}$ for each $i ⩽ n$ ). Similarly, let ${Valcomps}_{M, x}^{even}$ be the version in which only the even-numbered configurations and their successors are checked for consecution (i.e. $c_{2 i} ⇝ c_{2 i + 1}$ for each $i < n$ ). Then it is clear that ${Valcomps}_{M, x} = {Valcomps}_{M, x}^{odd} \cap {Valcomps}_{M, x}^{even}$ .

We can now construct a PDA $P_{M, x}$ that accepts precisely ${Valcomps}_{M, x}^{odd}$ . The well-formedness of each configuration, that $c_{1}$ is the start configuration, and that $c_{2 n}$ is a halting configuration – can all be checked by a finite-state automaton. The main thing that remains to be checked is the consecution of the odd-numbered configurations with their successors. A PDA can do this by simply pushing each odd-numbered configuration symbol-by-symbol on the stack, and then reading the succeeding configuration (which is conveniently reversed) to make sure it “agrees” with the corresponding symbols of the previous configuration, in accordance with the transition function of the Turing machine M. This is standard and we skip the details. If the PDA detects any violation of the consecution it rejects the string; if it finds no violations till the end of the string, it accepts. In a similar way we can construct a VPA $V_{M, x}$ that accepts precisely ${Valcomps}_{M, x}^{even}$ . Note that the primed alphabet helps here, as we can declare the call alphabet of the VPA to be $Δ_{M}$ , the return alphabet to be $Δ_{M}^{'}$ , and the internal alphabet to be ${#}$ .

Thus, given an instance M, x of the problem $\neg HP$ , we can (algorithmically) construct the PDA $P_{M, x}$ and VPA $V_{M, x}$ above. Since it is true that M does not halt on x iff $L (P_{M, x}) \cap L (V_{M, x}) = \emptyset$ , we can conclude:
Lemma 1.
The problem $\neg HP$ reduces to the problem of emptiness of the intersection of the languages accepted by a PDA and a VPA.

The second step is easy:
Lemma 2.
The problem of emptiness of the intersection of the languages accepted by a PDA and a VPA, reduces to the problem of language inclusion of a PDA with respect to a VPA.
Proof.
Let P and V be a PDA and a VPA respectively. As VPA’s are effectively closed under complementation, we can construct a VPA accepting $\overline{L (V)}$ . Now since $L (P) \cap L (V) = \emptyset$ if and only if $L (P) \subseteq \overline{L (V)}$ , the reduction follows. □

The final step is shown by the following lemma.
Lemma 3.
The problem of language inclusion of a PDA with respect to a VPA reduces to the problem of language inclusion of an ϵ-free PDS with respect to a VPS.
Proof.
Let P and V be the given PDA and VPA respectively, over an alphabet Σ. Let d be a symbol outside Σ. Then we will construct a PDS $P^{'}$ and a VPS $V^{'}$ over the alphabet $Σ \cup {d}$ which accept the languages $pref (L (P) \cdot {d})$ and $pref (L (V) \cdot {d})$ respectively. If we can do this, we are done, as it is easy to check that $L (P) \subseteq L (V)$ iff $L (P^{'}) \subseteq L (V^{'})$ .

We now focus on the construction of the PDS $P^{'}$ . Without loss of generality we can assume that the given PDA P has no ϵ-transitions. This is because it follows from Greibach’s normal form for context-free grammars [13] that a PDA can be converted to an equivalent ϵ-free PDA. We can now modify P to accept $L (P) \cdot {d}$ by adding a new state t, which will be the only accepting state, and adding transitions $((p, d), (t, X, X))$ for each final state p of P and stack symbol X. Let the resulting ϵ-free PDA be $P^{″} = (Q, Σ \cup {d}, Γ, s, δ, ⊥, F)$ .

We now describe how to construct a PDS $P^{'}$ that accepts the prefix-closure of $P^{″}$ . The idea is to detect when we are about to enter a “bad” configuration from which $P^{″}$ cannot reach an accepting configuration no matter what remaining input it reads. This can be done by making use of the pushdown reachability algorithm [4,9] (see also [27]), which gives us a deterministic finite-state automaton (DFA) that accepts precisely the bad configurations of a pushdown system. This DFA can be run (by $P^{'}$ ) on the stack contents to keep track of when it is about to get into a bad configuration.

More precisely, let $A = (Q_{A}, s_{A}, δ_{A}, F_{A})$ be a DFA accepting precisely the bad configurations of $P^{″}$ . Without loss of generality we assume A accepts the reverse of the configurations, so that it accepts strings of the form $Γ^{} \cdot Q$ . We define $P^{'}$ to be the PDS $(Q, Σ \cup {d}, Γ \times Q_{A} \times Q_{A}, s, δ^{'}, (⊥, q_{A}, s_{A}))$ , where $q_{A} = δ_{A} (s_{a}, ⊥)$ , and $δ^{'}$ is defined as follows. Let us consider a push transition in $P^{″}$ . For ease of presentation, let us assume it pushes two symbols and is of the form $(p, a, X) \to (q, Y Z)$ . Then for each $p_{A}, q_{A}, r_{A}, t_{A} \in Q_{A}$ , such that $δ_{A} (p_{A}, Y) = r_{A}$ , $δ_{A} (r_{A}, Z) = t_{A}$ , and $δ_{A} (t_{A}, q) \notin F_{A}$ , we add the transition $\begin{matrix} (p, a, (X, q_{A}, p_{A})) \to (q, (Z, t_{A}, r_{A}) (Y, r_{A}, p_{A})) \end{matrix}$ in $δ^{'}$ . Similarly, if $(p, a, X) \to (q, ϵ)$ is a pop transition in δ, then for each $p_{A}, q_{A} \in Q_{A}$ with $δ_{A} (p_{A}, q) \notin F_{A}$ , we add the transition $\begin{matrix} (p, a, (X, q_{A}, p_{A})) \to (q, ϵ) \end{matrix}$ in $δ^{'}$ . Thus, we are essentially keeping track of the state of A if it were to have read the current stack contents. We also need to keep track of the state of A if it had read the stack without the current top of stack. This helps us when we have to pop the top of stack and also lets $P^{'}$ detect when to disallow a transition that takes it to a bad configuration.

It is not difficult to see that $L (P^{'}) = pref (L (P^{″}))$ . In a similar way we can construct a VPS $V^{'}$ from V that accepts $pref (L (V) \cdot {d})$ . This completes the proof of the lemma. □

With this, we have completed the chain of reductions to prove Theorem 8. We remark here that the theorem and its proof also hold if we replace the PDS in the statement of the theorem by an ϵ-free DPDS.

Returning now to the problem of model-checking the NF and GNF properties for VPS’s, we show that the language inclusion problem of an ϵ-free PDS with respect to a VPS reduces to the model-checking problems $M C_{VPS} (NF)$ and $M C_{VPS} (GNF)$ .

Let $P = (Q_{P}, Σ, Γ_{P}, s_{P}, δ_{P}, ⊥_{P})$ be an ϵ-free PDS and $V = (Q_{V}, Σ_{c}, Σ_{r}, Σ_{int}, Γ_{V}, s_{V}, δ_{V}, ⊥_{V})$ be a VPS. We assume without loss of generality that $⊥_{P} = ⊥_{V} = ⊥$ . The aim is essentially to construct a VPS accepting $(k \cdot L (P)) \cup L (V)$ , and then to use an argument similar to Theorem 2. However constructing such a VPS is problematic due to the potential mismatch between the way the PDS P and the VPS V use their stacks on each input alphabet. Instead we construct a VPS $V^{'}$ over an alphabet $Σ \cup {k, k_{c}, k_{r}}$ , where k, $k_{c}$ , and $k_{r}$ are new symbols outside Σ, such that $L (V^{'}) = (k \cdot L (V_{P})) \cup L (V)$ where $V_{P}$ is a VPS constructed from P such that $L (V_{P}) ↾_{Σ} = L (P)$ . The call alphabet of $V^{'}$ is $Σ_{c} \cup {k_{c}}$ , the return alphabet is $Σ_{r} \cup {k_{r}}$ , and internal alphabet is $Σ_{int} \cup {k}$ . The VPS $V^{'}$ is depicted in Fig. 7.

The main step in the construction of $V^{'}$ is the component $V_{P}$ . The aim of $V_{P}$ is to simulate the moves of P. However due to the regimen imposed by the call/return alphabet $V_{P}$ may temporarily be out of step with P. In such a case, it will make use of the new input symbols to perform compensating actions that bring it back in step with P.

Fig. 7.
Constructed VPS $V^{'}$ .

We now describe the construction of $V^{'}$ . Let l be the maximum length of string pushed onto the stack in a single transition of $δ_{P}$ , and let $Γ_{l}$ denote all strings over Γ of length at most l. The components of $V^{'}$ are as follows:

The states of $V^{'}$ are $(Q_{P} \times Γ) \cup (Q_{P} \times Γ_{l} \times Γ_{l}) \cup Q_{V}$ . A state of the form $(q, X)$ will represent the fact that the simulation of a move of P is complete and it is in state q with top of stack X. A state of the form $(q, γ_{1}, γ_{2})$ will represent the fact that P is in state q, but we have to immediately perform some compensating actions by popping $γ_{1}$ from the stack and pushing $γ_{2}$ on the stack.

The call alphabet is $Σ_{c} \cup {k_{c}}$ , the return alphabet is $Σ_{r} \cup {k_{r}}$ , and the internal alphabet is $Σ_{int} \cup {k}$ .

The stack alphabet is $Γ_{V} \cup Γ_{P} \cup {D}$ , where D is a new stack symbol not in $Γ_{P} \cup Γ_{V}$ .

The start state is $s_{V}$ . We assume without loss of generality that $s_{V}$ has no incoming transitions in V.

The initial stack symbol is ⊥.

The transition relation δ comprises the transitions of V (i.e., $δ_{V}$ ), $(s_{V}, k, (s_{P}, ⊥))$ and the following transitions of the component $V_{P}$ .

For each transition $((p, a, X), (q, γ))$ in $δ_{P}$ , we add the following transitions based on whether a is a call, return, or internal action.
Case $a \in Σ_{c}$ : we add the push transition $((p, X), a, (q, D X, γ), D)$ in δ.

Case $a \in Σ_{int}$ : we add the internal transition $((p, X), a, (q, X, γ))$ in δ.

Case $a \in Σ_{r}$ : we add the pop transition $((p, X), a, X, (q, ϵ, γ))$ in δ.
In addition we add the following transitions to δ: $\begin{array}{l} ((q, X \cdot γ, γ^{'}), X, k_{r}, (q, γ, γ^{'})) for each X \in Γ, γ, γ^{'} \in Γ^{}, \\ ((q, ϵ, γ^{'} \cdot X Y), k_{c}, (q, ϵ, γ^{'} \cdot X), Y) for each X, Y \in Γ, γ^{'} \in Γ^{}, \\ ((q, ϵ, X), k_{c}, (q, X), X) for each X \in Γ, \\ ((q, ϵ, ϵ), k_{r}, X, (q, ϵ, X)) for each X \in Γ . \end{array}$

It is not difficult to argue that $V^{'}$ accepts the language $(k \cdot L (V_{P})) \cup L (V)$ with $L (V_{P}) ↾_{Σ} = L (P)$ .

Table 2
Partitioned alphabet ${\tilde{Σ}}_{3}$

$I$ $O$

$H$ ${k, k_{c}, k_{r}}$ ∅

$L$ ∅ Σ

Let ${\tilde{Σ}}_{3}$ be the partitioned alphabet $({k, k_{c}, k_{r}}, \emptyset, \emptyset, Σ)$ , as shown in Table 2.
Lemma 4.
Let P, V, and* $V^{'}$ be as described above. Then $L (P) \subseteq L (V)$ iff $L (V^{'})$ satisfies NF over ${\tilde{Σ}}_{3}$ .
Proof.
(⇒:) Suppose $L (P) \subseteq L (V)$ . Consider a string w in $L (V^{'})$ . Recall that by construction we have $L (V^{'}) = k \cdot L (V_{P}) \cup L (V)$ and $L (V_{P}) ↾_{Σ} = L (P)$ . Now if $w \in L (V)$ , then $w ↾_{L} = w$ which belongs to $L (V^{'})$ . If $w \in k \cdot L (V_{P})$ , then we know that $w ↾_{L} = w ↾_{Σ} \in L (P)$ . As $L (P) \subseteq L (V)$ , we have $w ↾_{L} \in L (V)$ and hence also that $w ↾_{L} \in L (V^{'})$ . This proves that $L (V^{'})$ satisfies NF.

(⇐:) Suppose $L (P) ⊈ L (V)$ . Then there exists some $w \in L (P) ∖ L (V)$ . Hence there exists a string of the form $k \cdot w^{'}$ in $L (V^{'})$ (more precisely $k \cdot L (V_{P})$ ) with $w^{'} ↾_{Σ} = w$ . Since w is not in $L (V)$ and also clearly not in $k \cdot L (V_{P})$ , we have $(k \cdot w^{'}) ↾_{L} \notin L (V^{'})$ . Hence $L (V^{'})$ does not satisfy NF. □

We have thus shown a reduction from the problem of language inclusion of a PDS with respect to a VPS to the problem of model-checking NF for a VPS. As the property GNF is the same as NF when $HO = \emptyset$ , the same reduction also works for the problem of model-checking GNF for VPS’s. Hence we have:
Theorem 9.
The problems of model-checking the properties NF and GNF for visibly pushdown systems are co-r.e. hard.

Since visibly pushdown systems are a strict subclass of deterministic pushdown systems, this gives us an alternative proof for the undecidability (in fact co-r.e. hardness) of the problem of model-checking NF and GNF for deterministic pushdown systems. We note that the problems of model-checking VPS’s (and DPDS’s) for other properties are still open.
8. Model-checking visibly pushdown systems – A decidable restriction

	$I$	$O$
$H$	${k, k_{c}, k_{r}}$	∅
$L$	∅	Σ

We now show that the restricted problem of model-checking visibly pushdown systems when all high events are internal is decidable for each of the properties of Definition 1.

8.1. A motivating example

We begin by motivating why this result is useful in a practical setting. Consider a system implemented as a C-like program with procedures, as shown in Fig. 8(a). The program has a global variable key representing a secret key it is updating, and makes calls to a recursive procedure foo to compute an intermediate value.

Fig. 8.

Modelling a program with procedures as a VPS. (a) Program P. (b) VPS model of P. (c) Stacks after calls to foo in line 3 and 10 respectively.

This program can be modelled as a VPS in a natural way, as shown in Fig. 8(b). The alphabet of actions is essentially the statement numbers of the original program, though some statements are split into several steps. For instance the statement 3 in the original program is split into actions $\overline{3a}$ , $\overline{3b}$ , $\overline{3c}$ , $\underline{3d}$ , and 3e in the VPS, to model the steps involved in a procedure call. These steps represent (a) +pushing local variables on the stack, (b) pushing the return address, (c) pushing the argument to the called procedure, and finally (d) restoring the value of local variables from the stack, and (e) carrying out the assignment of the returned value. We use the convention that a “push” alphabet (i.e. in $Σ_{c}$ ) is decorated with an “overline”, as in $\overline{3a}$ , a “pop” alphabet is decorated with an “underline”, as in $\underline{3d}$ , and an internal action, like 3e, is undecorated.

The control state of the VPS comprises a vector of the form $⟨ stepno, key, a, x, res, retval ⟩$ , representing the step number (or action name), the value of the variables key, a, x, and res, and finally the value last returned from a procedure call. We assume that the variables store integers of bounded size, and are intitialized to 0 at the time of declaration. For example, after the call to procedure foo(3) returns in main, the control state of our VPS would be $⟨ 4, 0, 6, 3, 6, 6 ⟩$ .

The transitions of the VPS are given in psuedo-code in Fig. 8(b). The step “push a” for example, is enabled whenever the step number in the control state equals “3a”, and it pushes the value of a stored in the current control state, onto the stack, and goes to a new control state in which step number is “3b”, with other components remaining unchanged. Similarly, the step “pop x” in step number 5, represents a transition that pops the top of the stack, stores it in the component x of the control state, and goes to step number 6.

Figure 8(c) shows the snapshots of the stack after the calls to foo in line 3 and line 10 in the original program, respectively.

Consider now a scenario concerning the security of this program P. Let us say a low-level observer has access to a covert channel that lets him detect accesses to the system stack, thereby allowing him to observe all the push and pop actions of the program while it is executing. However, he is not able to detect internal actions of the system, like accesses to the key variable which may be register-allocated. Suppose we are interested in whether the system, in this security setting, satisfies an information flow property like “it is not possible for the observer to conclude, by observing only the low-level actions of the system, that the key variable was changed”. Such a property can be phrased as one of the information flow properties of Definition 1, like non-inference (see [7]). We further note that the system model is a VPS that satisfies the assumption that all confidential events are internal actions. Hence, the result of this section (Theorem 10) gives us a way to algorithmically answer such questions.

8.2. Decision procedure

We now describe our decision procedure for model-checking the trace-based properties for this restricted class of VPS’s. We essentially make use of a characterization in our earlier work [7] (which in turn factors through Mantel’s characterization of trace-based properties in terms of what he called “Basic Security Predicates” [20]) which says that the model-checking problem for a class of system models $F$ reduces to the language-inclusion problem for that class provided the class $F$ is closed under certain language-theoretic operations. We note that the language inclusion problem for VPA’s is decidable, and hence to obtain the decidability result we seek, it suffices to show that the class of VPA’s are closed under these language-theoretic operations. We emphasize that these closure properties hold under the restriction that all confidential events are part of the alphabet of internal actions of the VPA.

In the sequel we will recall the definitions of the requisite operations, and the characterization of [7], before going on to show the closure properties of VPA’s.

In the definition below we will make use of some terminology. Let Σ be an alphabet. A view w.r.t. Σ is a partition $V = (V, N, C)$ of Σ into visible events V, confidential events C, and neither visible nor confidential events N, from a particular user’s point of view. A marked language M over Σ is a language over the alphabet $Σ \cup {♮}$ , where ‘♮’ is a special “mark” symbol different from those in Σ, and each string in M contains exactly one occurrence of ♮. A marked language over Σ is thus a subset of $Σ^{*} ♮ Σ^{*}$ .

Definition 8 ([7]).

Let $V = (V, N, C)$ be a view of an alphabet Σ. Let L be a language over Σ and M a marked language over Σ.

Let $X \subseteq Σ$ . The projection of the language L to X, written $L ↾_{X}$ , is defined to be ${τ ↾_{X} | τ \in L}$ .

$l - del (L) = {α β | c \in C, β ↾_{C} = ϵ, and α c β \in L} .$ This operation $l - del$ corresponds to the deletion of the last confidential event in a string.

$l - ins (L) = {α c β | c \in C, β ↾_{C} = ϵ, and α β \in L}$ . This $l - ins$ corresponds to the insertion of a confidential event in strings of L, only at a position after which no confidential events occur.

Let $X \subseteq Σ$ . Then ${l - ins - adm}^{X} (L)$ is defined to be the set $\begin{matrix} {α c β | c \in C, α β \in L, β ↾_{C} = ϵ, and \exists γ c \in L : γ ↾_{X} = α ↾_{X}} . \end{matrix}$ Operation $l - ins - adm$ (w.r.t. X) corresponds to insertion of “X-admissible” confidential events in strings of L. The insertion of a C-event is X-admissible after a prefix α in a string τ iff there exists another string $γ c \in L$ with γ projected to X being the same as α projected to X.

$l - del - mark (L) = {α ♮ β | c \in C, α c β \in L, and β ↾_{C} = ϵ}$ . The operation $l - del - mark$ corresponds to the “marked” deletion of the last confidential event. More precisely, this operation replaces the last C-event in every string of L by the special mark symbol ♮.

$l - ins - mark (L) = {α c ♮ β | c \in C, α β \in L, β ↾_{C} = ϵ}$ . The operation $l - ins - mark$ corresponds to the “marked” insertion of a confidential event. It is similar to the operation $l - ins$ , but additionally introduces a mark ♮ after the newly inserted C-event.

Let $X \subseteq Σ$ . Then we define ${l - ins - adm - mark}^{X} (L)$ to be the set $\begin{matrix} {α c ♮ β | c \in C, α β \in L, β ↾_{C} = ϵ, and \exists γ c \in L : γ ↾_{X} = α ↾_{X}} . \end{matrix}$ Operation $l - ins - adm - mark$ (w.r.t. X) corresponds to the marked insertion of X-admissible events. This operation is similar to $l - ins - adm$ , but a mark ♮ is introduced after the newly inserted X-admissible event.

$mark (L) = {α ♮ β | α β \in L}$ . Thus operation $mark$ corresponds to the insertion of a mark at an arbitrary position in strings of L.

Let $X \subseteq Σ$ . Then the marked projection of the marked language M to X, written $M ↾_{X}^{m}$ , is defined as $\begin{matrix} M ↾_{X}^{m} = {α ♮ β^{'} | α ♮ β \in M and β^{'} = β ↾_{X}} . \end{matrix}$ Thus marked projection operates on a marked language M and is similar to projection, but leaves every string intact up to the mark and projects the suffix after the mark to X.

Let $C^{'} \subseteq C$ and $V^{'} \subseteq V$ . Then ${l - del - con - mark}_{C^{'}, V^{'}} (L)$ is defined to be the set $\begin{matrix} {α v ♮ β | c \in C^{'}, v \in V^{'}, α c v β \in L and β ↾_{C} = ϵ} . \end{matrix}$ Thus the operation $l - del - con - mark$ (w.r.t. $C^{'}$ and $V^{'}$ ) corresponds to marked deletion in the “context” of an event in $V^{'}$ . This operation deletes the last confidential event c in a string and inserts a mark, provided c belongs to $C^{'}$ and is immediately followed by a $V^{'}$ -event in the string. For convenience we place the mark after the $V^{'}$ -event.

Let $C^{'} \subseteq C$ and $V^{'} \subseteq V$ . Then ${l - ins - con - mark}_{C^{'}, V^{'}} (L)$ is defined to be the set $\begin{matrix} {α c v ♮ β | c \in C^{'}, v \in V^{'}, α v β \in L, and β ↾_{C} = ϵ} . \end{matrix}$ Operation $l - ins - con - mark$ (w.r.t. $C^{'}$ and $V^{'}$ ) thus corresponds to marked insertion of $C^{'}$ -events in the “context” of a $V^{'}$ event, in the sense above.

Let $X \subseteq Σ$ , $C^{'} \subseteq C$ and $V^{'} \subseteq V$ . Then ${l - ins - adm - con - mark}_{C^{'}, V^{'}}^{X} (L)$ is defined to be the set $\begin{matrix} {α c v ♮ β | c \in C^{'}, v \in V^{'}, α v β \in L, β ↾_{C} = ϵ, and \exists γ c \in L, γ ↾_{X} = α ↾_{X}} . \end{matrix}$ The operation $l - ins - adm - con - mark$ (w.r.t. X, $C^{'}$ and $V^{'}$ ) corresponds to the marked insertion of X-admissible $C^{'}$ -events in the context of a $V^{'}$ event. It is similar to $l - ins - con - mark$ but allows only the insertion of X-admissible $C^{'}$ -events.

Let $N^{'} \subseteq N$ and $V^{'} \subseteq V$ . Then ${erase - con - mark}_{N^{'}, V^{'}} (L)$ is defined to be the set $\begin{matrix} {α v ♮ β | v \in V^{'}, and \exists δ \in {(N^{'})}^{*} : α δ v β \in L} . \end{matrix}$ The operation $erase - con - mark$ (w.r.t. $N^{'}$ and $V^{'}$ ) corresponds to the marked erasure of $N^{'}$ -events in the context of $V^{'}$ -events. More precisely, ${erase - con - mark}_{N^{'}, V^{'}} (L)$ contains all strings obtained from a string in L by the erasure of a consecutive sequence of zero or more $N^{'}$ events which end before a $V^{'}$ event v. The mark symbol is inserted after the event v in the string.

From [7,20], we have the following relation between information flow properties and the language-theoretic operations of Definition 8 established.

Lemma 5 ([7,20]).

Let $\tilde{Σ} = (Σ, H, L, I, O)$ be a partitioned alphabet. Let L be a language over Σ. Then:

L satisfies the property NF over $\tilde{Σ}$ iff $L ↾_{L} \subseteq L$ .

L satisfies property SEP over $\tilde{Σ}$ iff ${l - ins - adm - mark}^{C} (L) ↾_{Σ}^{m} \subseteq mark (L) ↾_{Σ}^{m}$ and $l - del - mark (L) ↾_{Σ}^{m} \subseteq mark (L) ↾_{Σ}^{m}$ .

L satisfies property GNI over $\tilde{Σ}$ iff $l - ins - mark (L) ↾_{L \cup HI}^{m} \subseteq mark (L) ↾_{L \cup HI}^{m}$ and $l - del - mark (L) ↾_{L \cup HI}^{m} \subseteq mark (L) ↾_{L \cup HI}^{m}$ .

Given a set $UI \subseteq I$ , L satisfies property NDO w.r.t. $UI$ over $\tilde{Σ}$ iff ${l - ins - adm - mark}^{UI} ↾_{Σ}^{m} \subseteq mark (L) ↾_{Σ}^{m}$ and $l - del - mark (L) ↾_{Σ}^{m} \subseteq mark (L) ↾_{Σ}^{m}$ .

L satisfies property FC over $\tilde{Σ}$ iff $l - ins - mark (L) ↾_{L \cup HI}^{m} \subseteq mark (L) ↾_{L \cup HI}^{m}$ , $l - del - mark (L) ↾_{L \cup HI}^{m} \subseteq mark (L) ↾_{L \cup HI}^{m}$ , ${l - ins - con - mark}_{HI, LI} (L) ↾_{L \cup HI}^{m} \subseteq {erase - con - mark}_{\emptyset, LI} (L) ↾_{L \cup HI}^{m}$ and $l - del - con - {mark}_{HI, LI} (L) ↾_{L \cup HI}^{m} \subseteq {erase - con - mark}_{\emptyset, LI} (L) ↾_{L \cup HI}^{m}$ .

L satisfies the property GNF over $\tilde{Σ}$ iff $L ↾_{L} \subseteq L ↾_{L \cup HI}$ .

L satisfies property PSP over $\tilde{Σ}$ iff ${l - ins - adm - mark}^{Σ} (L) ↾_{Σ}^{m} \subseteq mark (L) ↾_{Σ}^{m}$ and $l - del - mark (L) ↾_{Σ}^{m} \subseteq mark (L) ↾_{Σ}^{m}$ .

Lemma 6.
Let Σ be an alphabet, and let $V = (V, N, C)$ be a view of Σ. Let $\hat{Σ} = (Σ_{c}, Σ_{r}, Σ_{int})$ be a call-return partitioning of Σ, such that $C \cup N \subseteq Σ_{int}$ . Then the class of VPA’s over the alphabet $\hat{Σ}$ is closed under the operations of Definition 8 w.r.t. the view $V$ .
Proof.
In [7] we gave effective constructions for these operations for the class of finite-state systems. Deletion and insertion of internal events in a VPS behave the same way as finite-state systems as they do not influence the stack. Thus the constructions for many of the operations – $l - del$ , $l - ins$ , $l - del - mark$ , $l - ins - mark$ , mark, $l - del - con - mark$ , $l - ins - con - mark$ , $erase - con - mark$ – for finite-state systems carry over to VPS’s as well. We give the effective constructions for operations projection (when $X \supseteq Σ_{c} \cup Σ_{r}$ ) and $l - ins - adm$ below. The constructions for rest of the operations – $l - ins - adm - mark$ , marked projection (when $X \supseteq Σ_{c} \cup Σ_{r}$ ) and $l - ins - adm - con - mark$ – follow from these.
Projection: Let L be a language over an alphabet Σ, accepted by a VPA $A = (Q, Σ_{c}, Σ_{r}, Σ_{int}, Γ, s, δ, ⊥, F)$ , and let $X \supseteq Σ_{c} \cup Σ_{r}$ . Then we construct the VPA $A^{'}$ accepting $L ↾_{X}$ by simply replacing transitions in $A$ of the form $(p, a, q)$ , with $a \notin X$ , by ϵ-transitions $(p, ϵ, q)$ . Note that $A^{'}$ is a VPA with internal ϵ-transitions and can be converted to an equivalent standard VPA (i.e., without ϵ-transitions) as follows. We group internal ϵ-transitions in $δ_{ϵ}$ , i.e. $(p, q) \in δ_{ϵ}$ if and only if $(p, ϵ, q) \in δ$ . Let $δ_{ϵ}^{}$ denote the reflexive and transitive closure of $δ_{ϵ}$ . If there is a transition of the form $(p, a, q, γ)$ in $A^{'}$ with $a \neq ϵ$ , then we add the transition $(p^{'}, a, q^{'}, γ)$ to $B$ for every $p^{'}$ , $q^{'}$ such that $(p^{'}, p) \in δ_{ϵ}^{}$ and $(q, q^{'}) \in δ_{ϵ}^{}$ . Now it is easy to see that $L (B) = L (A^{'}) = L ↾_{X}$ .

$l - ins - adm$ : Let $X \subseteq Σ$ such that $X \supseteq Σ_{c} \cup Σ_{r}$ . Let L be a language over Σ accepted by a VPA $A = (Q, Σ_{c}, Σ_{r}, Σ_{int}, Γ, s, δ, ⊥, F)$ .

We construct $A^{'}$ for ${l - ins - adm}^{X} (L)$ as follows. We have two components in $A^{'}$ . The first component is the product of two copies of $A$ where the second copy non-deterministically keeps track of a state of $A$ that is reachable by a word that is X-equivalent to the current word being read (i.e. their projections to X are equal) by replacing the non-X transitions with ϵ (and further ϵ’s are eliminated as described in the case of the projection operation). We have a transition labelled c, with $c \in C$ , from a state $(p, q)$ in the first component to p in the second copy, provided from q it is possible to take a c-labelled transition and reach a final state. Once in the second component, we allow only non-C transitions and retain the original final states. The construction is depicted in Fig. 9.

More formally, we define $A^{'}$ as follows. The first component is the product of $A$ with $B$ where $B$ is the VPA obtained from $A$ by replacing the labels of all transitions not in X by ϵ. Note that from our assumption, we only have internal ϵ-transitions in $B$ . We eliminate these ϵ-transitions from $B$ as described in the case of the projection operation. Let $δ_{B}$ denote the transition relation of $B$ . We define $A^{'} = ((Q \times Q) \cup Q, Σ_{c}, Σ_{r}, Σ_{int}, Γ \times (Γ \cup {⋆}), δ^{'}, (s, s), F)$ where $⋆ \notin Γ$ and $δ^{'}$ is defined as follows. $\begin{matrix} \begin{matrix} ((p, q), a, (p^{'}, q^{'})) \in δ^{'} & iff a \in (X \cap Σ_{int}) \land (p, a, p^{'}) \in δ \land (q, a, q^{'}) \in δ_{B}, \\ ((p, q), a, (p^{'}, q^{'}), (A_{1}, A_{2})) \in δ^{'} & iff a \in (X \cap Σ_{c}) \land (p, a, p^{'}, A_{1}) \in δ \land (q, a, q^{'}, A_{2}) \in δ_{B}, \\ ((p, q), a, (A_{1}, A_{2}), (p^{'}, q^{'})) \in δ^{'} & iff a \in (X \cap Σ_{r}) \land (p, a, A_{1}, p^{'}) \in δ \land (q, a, A_{2}, q^{'}) \in δ_{B}, \\ ((p, q), a, (p^{'}, q)) \in δ^{'} & iff a \notin X \land (p, a, p^{'}) \in δ, \\ ((p, q), c, p) \in δ^{'} & iff c \in C \land \exists q^{'} \in F (q, c, q^{'}) \in δ_{B}, \\ (p, a, q) \in δ^{'} & iff a \notin C \land (p, a, q) \in δ, \\ (p, a, q, (A, ⋆)) \in δ^{'} & iff (p, a, q, A) \in δ, \\ (p, a, (A_{1}, A_{2}), q) \in δ^{'} & iff (p, a, A_{1}, q) \in δ \land A_{2} \in Γ . □ \end{matrix} \end{matrix}$
Fig. 9.
Construction of VPA $A^{'}$ for ${l - ins - adm}^{X} (L)$ .

We can now state and prove the main result of this section: Theorem 10.
The restricted problem of model-checking visibly pushdown systems for any of the trace-based properties of Definition* 1 , when all the high events are internal, is EXPTIME-complete.
Proof.
Let V be a VPS over a call-return alphabet $\hat{Σ} = (Σ_{c}, Σ_{r}, Σ_{int})$ , and let P be one of the properties of Definition 1 w.r.t. a partitioning $\tilde{Σ} = (Σ, H, L, I, O)$ of Σ, with $H \subseteq Σ_{int}$ . Then, by Lemma 5, V satisfies P w.r.t. $\tilde{Σ}$ iff ${op}_{1}^{'} (L (V)) \subseteq {op}_{2}^{'} (L (V))$ , where ${op}_{1}^{'}$ and ${op}_{2}^{'}$ are some operations (or composition of operations) of Definition 8. By Lemma 6, we can construct VPA’s $A_{1}$ and $A_{2}$ such that $L (A_{1}) = {op}_{1}^{'} (L (V))$ and $L (A_{2}) = {op}_{2}^{'} (L (V))$ . Both $A_{1}$ and $A_{2}$ can be seen to have at most polynomially many states as V. The language inclusion problem for VPA’s over the same call-return partitioned alphabet is decidable in EXPTIME [1]. Thus we can check whether $L (A_{1}) \subseteq L (A_{2})$ in exponential time in the size of V. This shows that the model-checking problem for property P is in EXPTIME.

To show the EXPTIME-hardness part, we reduce the language inclusion problem for VPA’s to the problem of model-checking VPS’s in which all the high events are internal for each of the trace-based properties. Using arguments similar to those in the proof of Lemma 3, we reduce the language inclusion problem for VPA’s to the language inclusion problem for VPS’s. Then Theorem 2, applied for VPS’s, provides us with a reduction from the language inclusion problem to the problem of model-checking VPS’s, provided VPS’s are effectively closed under the operations ${op}_{1}$ through ${op}_{5}$ of Definition 7. By following the same steps we used to show effective closure under these operations for one counter nets in Section 6, we obtain effective closure under these operations for visibly pushdown systems as well. Note that the added transitions in these constructions for one counter nets never increment/decrement the counter. This corresponds to introducing internal transitions in a VPS and thus these constructions prove closure of VPS’s with respect to the operations ${op}_{1}$ through ${op}_{5}$ . Also in each of these constructions we have all the high events ( $H = {k}$ ) to be internal. It is easy to see that these constructions are polynomial in the size of the given VPA.

Putting these reductions together, we obtain a polynomial-time reduction from the language inclusion problem for VPA’s to the restricted problem of model-checking each of the trace-based properties for VPS’s when all the high events are internal. This completes the proof of EXPTIME-hardness. □

9. Conclusion

In this paper we have studied the problem of model-checking some of the well-known trace-based information flow properties for infinite-state system models. In earlier work [7] showing decidability of checking these properties for finite-state systems, we had reduced the problem of model-checking these properties for a class of system models, say $F$ , to the language inclusion problem for $F$ , provided the class $F$ is effectively closed under some operations. In this work we have essentially shown a converse reduction: we show that the language inclusion problem for $F$ reduces to the problem of model-checking these properties for $F$ , provided $F$ is effectively closed under some (different) language-theoretic operations. Thus it is evident that the problem of language inclusion and the problem of checking these properties are closely related.

As part of future work, we aim to resolve the open questions mentioned in Table 1. It would also be interesting to apply Theorem 2 to other classes of system models. The language inclusion problem for many models is studied extensively in [2]. This problem is known to be undecidable for many sub-classes of context-free languages – linear, unambiguous, sequential, simple deterministic, real-time strict deterministic, super-deterministic and $LL (k)$ . We would like to study the model-checking problem for these classes as well. An interesting class of models that merits further investigation is deterministic one-counter nets (DOCN) for which some decidability results have been recently shown [17]. While these results would seem to imply that model-checking the NF property for this class is decidable, it would be interesting to explore decision procedures for the remaining properties.

References

Alur and

Madhusudan , Visibly pushdown languages, in: Proceedings of the 36th ACM Symposium on Theory of Computing, 2004, pp. 202–211.

P.R.J.

Asveld and

Nijholt , The inclusion problem for some subclasses of context-free languages, Theoretical Computer Science 230(1–2) (1999), 247–256.

Bossi ,

Focardi ,

Piazza and

Rossi , A proof system for information flow security, in: Logic Based Program Synthesis and Transformation, Springer, 2003, pp. 199–218.

J.R.

Büchi , Regular canonical systems, Archiv Math. Logik und Grundlagenforschung 6 (1964), 91–111.

Christensen , Decidability and decomposition in process algebras, PhD thesis, Edinburgh University, 1993.

M.R.

Clarkson and

F.B.

Schneider , Hyperproperties, Journal of Computer Security 18(6) (2010), 1157–1210.

D’Souza ,

Holla ,

K.R.

Raghavendra and

Sprick , Model-checking trace-based information flow properties, Journal of Computer Security 19(1) (2011), 101–138.

D’Souza and

K.R.

Raghavendra , Model-checking bisimulation-based information flow properties for infinite state systems, in: Proceedings of 17th European Symposium on Research in Computer Security (ESORICS), Pisa, Italy, September 10–12, 2012, pp. 591–608.

Esparza ,

Hansel ,

Rossmanith and

Schwoon , Efficient algorithms for model checking pushdown systems, in: Proceedings of 12th Conference on Computer Aided Verification (CAV), Chicago, IL, USA, July 15–19, 2000, pp. 232–247.

10.

Focardi and

Gorrieri , A classification of security properties for process algebras, Journal of Computer Security 3(1) (1995), 5–33.

11.

Focardi and

Gorrieri , The compositional security checker: A tool for the verification of information flow security properties, IEEE Transactions on Software Engineering 23(9) (1997), 550–571.

12.

J.A.

Goguen and

Meseguer , Security policies and security models, in: Proceedings of IEEE Symposium on Security and Privacy, 1982, pp. 11–20.

13.

S.A.

Greibach , A new normal-form theorem for context-free phrase structure grammars, J. ACM 12(1) (1965), 42–52.

14.

J.D.

Guttman and

M.E.

Nadel , What needs securing, in: Proceedings of Computer Security Foundations Workshop, 1988, pp. 34–57.

15.

Hirshfeld , Petri nets and the equivalence problem, in: Proceedings of 7th Workshop on Computer Science Logic (CSL), Swansea, UK, September 13–17, 1993, pp. 165–174.

16.

Hofman ,

Mayr and

Totzke , Decidability of weak simulation on one-counter nets, in: Proceedings of 28th ACM/IEEE Symposium on Logic in Computer Science, New Orleans, LA, USA, June 25–28, 2013, pp. 203–212.

17.

Hofman and

Totzke , Trace inclusion for one-counter nets revisited, 2014, available at: arXiv:1404.5157.

18.

D.M.

Johnson and

F.J.

Thayer , Security and the composition of machines, in: Proceedings of Computer Security Foundations Workshop, Franconia, NH, USA, 1988, pp. 72–89.

19.

Kozen , Automata and Computability, Springer-Verlag, New York, 1997.

20.

Mantel , Possibilistic definitions of security – An assembly kit, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, July 3–5, 2000, pp. 185–199.

21.

Mantel , A uniform framework for the formal specification and verification of information flow security, PhD thesis, Universität des Saarlandes, 2003.

22.

Mayr , Process rewrite systems, Inf. Comput. 156(1–2) (2000), 264–286.

23.

McCullough , Specifications for multilevel security and a hookup property, in: Proceedings of IEEE Symposium Security and Privacy, 1987, pp. 161–166.

24.

McLean , A general theory of composition for trace sets closed under selective interleaving functions, in: Proceedings of IEEE Symposium on Research in Security and Privacy, IEEE Computer Society Press, 1994, pp. 79–93.

25.

O’Halloran , A calculus of information flow, in: Proceedings of the European Symposium on Research in Computer Security, 1990, pp. 147–159.

26.

Sutherland , A model of information, in: Proceedings of the 9th National Computer Security Conference, 1986, pp. 175–183.

27.

Thomas , Finite automata and the analysis of infinite transition systems, in: Modern Applications of Automata Theory, 2012, pp. 495–528.

28.

Totzke , Inclusion problems for one-counter systems, PhD thesis, University of Edinburgh, 2014.

29.

L.G.

Valiant , Decision procedures for families of deterministic pushdown automata, Technical report, Coventry, UK, 1973.

30.

van der Meyden and

Zhang , Algorithmic verification of noninterference properties, Electronic Notes in Theoretical Computer Science 168 (2007), 61–75.

31.

Zakinthinos and

E.S.

Lee , A general theory of security properties, in: Proceedings of IEEE Symposium on Security and Privacy, IEEE Computer Society, Washington, DC, USA, 1997, pp. 94–102.