{'fraction_non_alphanumeric': 0.03234058103416773, 'fraction_numerical': 0.006532066508313539, 'mean_word_length': 4.602098259979529, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A New Enforcement on Declassification with Reachability Analysis

Language-based information flow security aims to decide whether an action-observable program can unintentionally leak confidential information if it has the authority to access confidential data. Recent concerns about declassification polices have provided many choices for practical intended information release, but more precise enforcement mechanism for these policies is insufficiently studied. In this paper, we propose a security property on the where-dimension of declassification and present an enforcement based on automated verification. The approach automatically transforms the abstract model with a variant of self-composition, and checks the reachability of illegal-flow state of the model after transformation. The self-composition is equipped with a store-match pattern to reduce the state space and to model the equivalence of declassified expressions in the premise of property. The evaluation shows that our approach is more precise than type-based enforcement.


I. INTRODUCTION
Information flow security is concerned with finding new techniques to ensure that the confidential data will not be illegally leaked to the public observation. The topic is popular at both language level and operating system level. Languagebased techniques have been pervasively adopted in the study on information flow security. This is comprehensively surveyed in [1]. Noninterference [2] is commonly known as the baseline property of information flow security. The semanticbased definition of noninterference [3] on batch-job model characterizes a security condition specifying that the system behavior is indistinguishable from a perspective of attacker regardless of the confidential inputs. Noninterference is criticized for the restriction that forbids any flow from high to low. It will influence the usability of system because the deliberate release is pervasive in many situations, e.g. password authentication, online shopping and encryption. Therefore, it is important to specify more relaxed and practical policies for real application scenarios and develop precise enforcement mechanisms for these policies.
The confidentiality aspect of information downgrading, i.e. declassification [4], allows information release with different intentions along four dimensions [5]: what is released, where does the release happen, when the information can be released and who releases it. The security policy we propose is on the where-dimension. On this dimension, there have been several polices, e.g. intransitive noninterference [6], non-disclosure [7], WHERE [8], flow locks [9], and gradual release [10]. Each of them leverages a certain category of type system to enforce the security policy.
In this work, we first use an approach based on automated verification to enforce declassification policy on the wheredimension. As a flow-sensitive and context-sensitive technique, automated verification has been used as an enforcement to noninterference on both imperative languages [11,12] and object-oriented languages [13,14]. In these works declassification is only discussed in [12], where the specific property relaxed noninterference [15] is mostly on the what-dimension.
The approaches based on automated verification usually rely on some form of self-composition [11] that composes the program model with a variable-renamed copy to reduce the security property on original model to a safety property on the model after transformation. In our previous work [14], we have developed a framework that uses reachability analysis to ease the specification of temporal logic formula or the manual assertion encoding partial correctness judgement. The selfcomposition doubles the size of memory store and largely increases the state space of model. When the I/O channels are considered, this effect becomes more serious since each store of channel is modeled explicitly. On the other hand, the security property often requires the equivalence of declassified expressions to be satisfied. Therefore in our enforcement we propose a store-match pattern to 1. avoid duplicating the output channels, and 2. facilitate the self-composition by modeling the equivalence of declassified expressions in the premise of security property. We also evaluated the similarity of the properties and the preciseness of our enforcement mechanism compared with type system.
The main contributions of the paper include: (i) We propose a more relaxed security property enforceable with automated verification on the where-dimension; (ii) We give a flowsensitive and context-sensitive enforcement based on reachability analysis of pushdown system. We show the mechanism is more precise than type-based approaches; (iii) We propose a store-match pattern that can be in common use for automated verifications to reduce the state space of model and the cost of security analysis.
The rest of the paper is organized as follows. In Section II, we introduce the language model and the baseline property.

Fig. 2. Operational Semantics
In Section III, we define the where-security and prove the compliance of property with the prudent principles. Section IV describes the enforcement mechanism. We show the evaluation in Section V and conclude in Section VI.

II. PROGRAM MODEL AND BASELINE PROPERTY
We use a sequential imperative language with I/O channels as the presentation language to illustrate our approach. The syntax is listed in Fig.1. The language is deterministic. The primitive declass stands for declassification that downgrades the confidential data of expression e to be assigned to variable x with a lower security domain. Here x can be considered as a low-level sink of data observable to the attacker. I and O are respectively the set of input and output channels. They are formally defined as a mapping from each channel identifier i to a linear list, e.g. I i resp. O i . The command input(x, I i ) indicates that the input from I i is assigned to x, and the command output(e, O i ) stores the value of expression e into the correct position of O i .
The computation is modeled by the small-step operational semantics in Fig.2. The inductive rules are defined over configurations of the form (µ, I, O, p, q, C). µ : Var → N is a memory store mapping variables to values and C is the command to be executed. p and q are set of indices. p i denotes the index of next element to be input from I i , and q i is the index of location of O i where the next output value will be stored. The elements in p and q are explicitly increased by the computation of inputs and outputs.
The security policy is a tuple (D, , , σ) where (D, ) is a finite security lattice on security domains and is an exceptional downgrading relation of security domains ( ∩ = ∅) statically gathered from the program. Let σ : Var∪I ∪O → D be the mapping from I/O channels and variables to security domains, and let σ(e) ≡ x∈e σ(x) be the least upper bound of the security domains of variables contained in e. When command x := declass (e) in program has σ(x) ≺ σ(e), the declass operation performs a real downgrading from some variable in e and only then an element (σ(e), σ(x)) is contained in the relation , otherwise the operation is identical to an ordinary assignment. We label the transition of declassification with → d in Fig.2. The security policy is different from the MLS policy with exceptions proposed in [6,8,16], where the set of exceptional relations is independent to the declassification operations. In our policy the exceptions are gathered from the declass commands. Our treatment is reasonable since developer should have right to decide the exception when they use the primitive declass explicitly. This is also supported in other work, e.g. [17].
We specify noninterference with the semantic-based PERmodel [3]. Intuitively speaking, it specifies a relation between states of any two correlative runs of program, which is variation in the confidential initial state cannot cause variation in the public final state. In another word, the runs starting from indistinguishable initial states derive indistinguishable final states as well. For the language with I/Os, the indistinguishability relation on memory stores and I/O channels with respect to certain security domain ℓ is defined as below.
For the two observable channels with same security domain, the indistinguishable linear lists should have the same length and identical content. Let I ℓ be the set of input channels with security domain ℓ ′ (ℓ ′ ℓ). If the set I and I ′ have the same domain, e.g. as the inputs of the same program, we can use I ∼ ℓ I ′ to express ∀i.I i ∈ I ℓ ⇒ I i ∼ ℓ I ′ i . The noninterference formalized here takes into consideration the I/O channels and is therefore different from what for batchjob model [1]. It is given as follows.
In this definition, the noninterference property is related to a security domain ℓ 0 . The content of channels with security domain ℓ ′ (ℓ ′ ≻ ℓ 0 ) is unobservable and irrelevant to the property. A more specific way to define noninterference is to require ℓ 0 = D. That means the proposition in Definition 2 has to be satisfied for each security domain in D. We use this definition in the following. Our definition adopts a manner to consider the indistinguishability of the initial and final states but not to characterize the relation in each computation step as did by the bisimulation-based approach [18]. Another use of the security domain of variables is to specify where a valid declassification occurs. This will be discussed below.

III. WHERE-SECURITY AND PRUDENT PRINCIPLES
In this section, we give a security condition to control the legitimate release of confidential information on the wheredimension of security goals. It considers both the code locality where the release occurs and the level locality to which security domain the release is legal. Let ։ represent a (possible empty) sequence of declassification-free transitions. A trace of computations is separated to the declassifications labeled with → d and declassification-free computation sequences. The where-security is formally specified as below.
Intuitively speaking, when the indistinguishable relation on the final states is violated, the contrapositive implies that it is caused by the variation of declassified expressions. This variation is indicated valid by the premise our property. If the leakage of confidential information is caused by a computation other than the primitive declass , it will be captured because without constraining the equality of released expression, the final indistinguishability cannot hold. Our where-security property is more relaxed than WHERE [8,16] which uses strongbisimulation and requires each declassification-free computation step meets the baseline noninterference. We can use explicit final output of public variables to adapt the judgement of µ n+1 ∼ ℓ µ ′ n+1 to the judgement of O n+1 ∼ ℓ O ′ n+1 . Sabelfeld and Sands [5] clarify four basic prudent principles for declassification policies as sanity checks for the new definition: semantic consistency, conservativity, monotonicity of release, and non-occlusion. Our where-security property can be proved to comply with the first three principles. Let P [C] represent a program contains command C. P [C ′ /C] substitutes each occurrence of C in P with C ′ . The principles with respect to the where-security are defined as follows.
Lemma 1 (Semantic Consistency). Suppose C and C ′ are declassification-free commands and semantically equivalent on the same domain of configuration.
Lemma 2 (Conservativity). If program P is where-secure and P contains no declassification, then P satisfies noninterference property. This corollary indicates that the where-security complies with the three prudent principles given by the above lemmas. The proofs of the lemmas are presented in [19]. The nonocclusion principle cannot be formally proved since a proof would require a characterization of secure information flow which is what we want to check against the prudent principles.

IV. ENFORCEMENT
In this section, we provide a new enforcement for the where-security based on reachability analysis of symbolic pushdown system [20]. A pushdown system is a stack-based state transition system whose stack contained in each state can be unbounded. It is a natural model of sequential program with procedures. Symbolic pushdown system is a compact representation of pushdown system encoding the variables and computations symbolically.
The stack symbols denote the flow graph nodes of program. The relation R specifies the variation of abstract variables before and after a single step of symbolic execution directed by the pushdown rules. The operations on R are compactedly implemented with binary decision diagrams (BDDs) [21] in Moped [22] which we use as the back-end verification engine.
The model construction of commands other than I/O operations is similar to the one in our previous work [23]. In the pushdown system, the public channels are represented by global linear lists. In another word, for a security domain ℓ ∈ D, we only model the channels in I ℓ and O ℓ . Take a input command for example, if the source channel is I i , the pushdown rule has a form of IR H for σ(I i ) ≻ ℓ and IR L for σ(I i ) ℓ in Table I, where ⊥ denotes an indefinite value.
OR L γ j ֒→ output entry γ k (tmp ′ = e) ∧ rt(µ, I ℓ , O ℓ , p ℓ , q ℓ , · · · ) ∧ rt 2 (· · · ) output exit ֒→ ǫ rt(µ, On the other hand, if the target channel of output is O i , the pushdown rule has a form of OR H for σ(O i ) ≻ ℓ and OR L for σ(O i ) ℓ in Table I. OR H is just like a transition of skip since the confidential outputs do not influence the public part of subsequent states. The variable tmp stores the value of expression to be outputted or declassified. rt means retainment on value of global variables and on value of local variables in γ j ֒→ γ k . rt 2 for a rule γ j ֒→ f entry γ k denotes retainment on value of local variables of the caller of procedure f. The declassifications are modeled with DR in Table I. The bodies of outputs to different public channel and the bodies of declassifications are vacuous. These absent parts of model will be filled by the self-composition. This treatment is decided by the store-match pattern which we develop to avoid the duplication of public channels and to guide the instrumented computation to fulfil the premise of where-security property.
We follow the principle of reachability analysis for noninterference which we proposed in [14]. The self-composition is evolved into three phases: basic self-composition, auxiliary initial interleaving assignments, and illegal-flow state construction. For simplicity, we use the compact self-composition [23] as basic self-composition. To avoid duplicating the input channels, we reuse the content of public input channels by resetting the indices of p ℓ to 0 at the beginning of the pairing part of model, see RST in Table II. This treatment is safe because from the semantics we know that no computation actually modifies the content of input channels. In order to avoid duplicating the output channels, we propose a storematch pattern of output actions. This is to stuff the model after basic self-composition with the pushdown rules OS and OM in Table II parameterized with the channel identifier i. The OM rules show that when the output to channel O i is computed in the second run, it is compared with the corresponding output stored during the first run. If they are not equal, the symbolic x∈Var ∧rt(µ)}∪DSγ j ∪DMγ j 10. else if r.expr = γj ֒→ γ k then 11.
execution is directed to the illegal-flow state error.
Compared with the noninterference property, the premise of where-security contains equality relations on the declassified expressions, therefore we need some structure to instrument the semantics of abstract model to make sure the computation can proceed only when the equality relations are satisfied. We define another global linear list D. Suppose there are m declassifications respectively at code location γ di (0 ≤ i < m) and a function ρ mapping γ di to i. We give another pattern of store-match that stores the value of expression declassified at γ di to the site D[ρ(γ di )], see DS in Table II. The corresponding match operation has a form of DM in Table II. Note that ξ is the rename function on the stack symbols to generate new flow graph nodes as well as on the variables to generate the companion variables for the pairing part of model. The state idle has only itself as the next state. From the reachability of error we can ensure the violation of where-security without considering the equality relations on the subsequent outputs. The self-composition algorithm is given in Algorithm 1. The LastTrans returns the pushdown rule with respect to the last return command of program. The first rule added to ∆ ′ denotes the initial interleaving assignments from public variables to their companion variables. r.R x∈Var means a relation substituting each variable in Var with the renamed companion variable.
Theorem 1 (Correctness). Let SC(P ℓ ) be the pushdown system w.r.t. security domain ℓ generated by our self-composition on the model of program P . If ∀ℓ ∈ D, the state error of SC(P ℓ ) is unreachable from any initial state, we have P satisfies the where-security.
(The proof is sketched in the technical report [19])

V. EVALUATION
We implement Algorithm 1 as part of the parser of Remopla [24] and use Moped as the black-box back-end engine for the reachability analysis. Here we use experiments to evaluate: 1. whether the property defined by where-security is similar to the existing properties on the where-dimension, e.g. [8,10], and what is the real difference between these properties. 2. the preciseness of the mechanism compared with the type systems on enforcing the respective security properties. 3. whether the store-match pattern can really reduce the state space as well as the cost of verification. The experiments are performed on a laptop with 1.66GHz Intel Core 2 CPU, 1GB RAM and Linux kernel 2.6.27-14-generic. The test cases are chosen from related works, see Table IV.
Firstly, we illustrate that where-security is more relaxed than WHERE [8,16] and gradual release [10]. Lux and Mantel [16] have proposed another two prudent principles: noninterference up-to and persistence. Compared with the four basic principles, the two principles are not generally used for policies on different dimensions. The conformances of the properties with these principles are given in Table III. Similar to the gradual release, the program P1 in Table IV is secure (denoted by ) w.r.t. where-security. This indicates the two properties do not comply with persistence since the reachable command l := h is obviously not secure. On the contrary, WHERE rejects this program. Our where-security does not comply with noninterference up-to because the definition deduces relations on final states but not on the states before declass primitives. A typical example is P0. It is where-secure but judged insecure by WHERE and gradual release. Although different on these special cases, the where-security can characterize a similar property to WHERE and gradual release for the most cases in Then we evaluate the preciseness of our enforcement mechanism. In Table IV τ 1 is the well-typeness of program judged by the type system in Fig.4, [8]. τ 2 is the judgement of the type system given in Fig.3, [10]. RA is the reachability analysis result using our mechanism. means the state error is not reachable. The analysis time T is related to the number of bits of each variable, which we set to 3 and that means each variable in the model has a range of 0∼2 3 -1. Larger number of bits corresponds to the increase on state space of model and the analysis time. On the other hand, the number of bits of variable is meaningful also because if it is too small for the model of insecure program, the illegal path cannot be caught. This causes a false-positive which can be avoided by setting the number of bits of variable sufficiently large. We record the minimum number of bits to avoid falsepositive as N min . The analysis might be time consuming when N min is large. For secure program, the illegal-flow state will be unreachable for any number of bits therefore N min is not recorded. The program filter in Table IV has a more complex policy. From the escape hatch information we have reader network. The model is constructed and transformed on respective security domains. On each security domain different public variables are modeled outputted in the end and state error of transformed model is unreachable. Our enforcement is more precise compared with the type systems that reject some secure programs (P2,P6,P7 for WHERE and P1,P2,P6 for gradual release).
Finally, we evaluate the reduction on the cost of verification provided by the store-match pattern. We compare our mechanism with a model transformation, i.e. Tr in Fig.3, which duplicates the public output channels and constructs the illegal-flow state following the pairing part of model. The test cases containing I/Os are from Fig.4, [26], and named F 1 ∼F 8 in Fig.3. These experiments show that the store-match pattern can give an overall 41.4% reduction on the cost of verification. The number of bits of variable is set to 3 as well.

VI. CONCLUSION
We propose a security property on the where-dimension of declassification. The property is proved complying with the three classical prudent principles. We also give a precise enforcement based on the reachability analysis of pushdown system derived by a variant of self-composition. To immigrate our approach to the properties on other dimensions of declassification, e.g. the delimited release [17] on the what-