Christophe Demattei
email: demattei@iurc.montp.inserm.fr

Nicolas Molinari

Jean-Pierre Daures

SPATCLUS: an R Package for Arbitrarily Shaped Multiple Spatial Cluster Detection for Case Event Data

Keywords: Spatial cluster detection test, Expected distance computation, Regression model, Dynamic programming algorithm, Numerical approximations

This paper describes an R package, named SPATCLUS, that implements a method recently proposed for spatial cluster detection of case event data. This method is based on a data transformation. This transformation is achieved by the definition of a trajectory which allows to attribute to each point a selection order and the distance to its nearest neighbour. The nearest point is searched among the points which have not yet been selected in the trajectory. Due to the trajectory effects, the distance is weighted by the expected distance under the uniform distribution hypothesis. Potential clusters are located by using multiple structural change models and a dynamic programming algorithm. The double maximum test allows to select the best model. The significativity of potential clusters is determined by Monte Carlo simulations. This method makes it possible the detection of multiple clusters of any shape.

Introduction

A spatial cluster is an aggregate of points in IR p (p > 1) that are grouped together in space with an abnormally high incidence, which has a low probability to have occured by chance alone. Clusters of events are often reported to health agencies and an examination of the data is sometimes required for establishing an etiologic link between exposure and cluster existence. Location and detection of spatial cluster affects severals fields such as agronomy, medicine and social sciences.

Tests for spatial clustering have received substantial attention in the literature. A large number of tests have been proposed by different scientists in the different fields mentioned above. They can be classified according to their purpose. Tests for global clustering [START_REF] Ripley | Modelling spatial patterns[END_REF][START_REF] Whittemore | A test to detect clusters of disease[END_REF][START_REF] Cuzick | Spatial clustering for inhomogeneous populations[END_REF][START_REF] Besag | The detection of clusters in rare diseases[END_REF][START_REF] Tango | A test for spatial disease clustering adjusted for multiple testing[END_REF] are used to analyse the overall clustering tendency of disease incidence in the study area. The cluster location is unknown. Cluster detection tests [START_REF] Turnbull | Monitoring for clusters of disease: application to leukemia incidence in upstate New York[END_REF][START_REF] Kulldorff | A spatial scan statistic[END_REF] are concerned with local clusters. Potential clusters are located and their significance is tested. At last, focused tests [START_REF] Cuzick | Spatial clustering for inhomogeneous populations[END_REF][START_REF] Besag | The detection of clusters in rare diseases[END_REF][START_REF] Diggle | Case-control isotonic regression for investigation of elevation in risk around a point source[END_REF] are used when a pre-specified focus is supposed to be linked to disease incidence. This paper describes the implementation in R langage of a new method of detection and inference for multiple spatial clusters [START_REF] Dematteï | Arbitrarily Shaped Multiple Spatial Cluster Detection for Case Event Data[END_REF]. This method deals with precise events within IR 2 , such as spatial coordinates for the occurrence of disease cases or the geographical positions of individuals. The approach, based on transformation of the data set and a regression model, is an extension of the method presented in Molinari et al. [START_REF] Molinari | Multiple temporal cluster detection[END_REF] for multiple temporal clusters. This new test belongs to the class of detection tests for case event data.

The following section briefly describes the method implemented in the SPATCLUS package. It begins with data tranformation by determining a trajectory and the weighted distances. The ordered weighted distances are then used in the cluster location and detection stages. In the third section, we present a decription of the SPAT-CLUS package. Data input, optional parameters, output and result vizualization are detailed, main algorithms are presented and explained. The use of the exportation module in SatScan [START_REF] Kulldorff | Information Managements Services, Inc. SaTScan v5.1: Software for the spatial and space-time scan statistics[END_REF] format is also detailed. In the fourth section, we apply the method to both simulated and real data. The paper is concluded by a discussion.

Methods

The goal of the method is to test the null hypothesis which corresponds to a uniform distribution of the events. We only present here essential background. A detailed presentation of the method is given in Dematteï et al. [START_REF] Dematteï | Arbitrarily Shaped Multiple Spatial Cluster Detection for Case Event Data[END_REF].

Data transformation

Let n be the number of events occuring in A, a bounded set of IR 2 or IR 3 . The spatial coordinates of those n events are i.i.d random variables denoted X 1 , . . . , X n .

The data transformation consists first in the determination of a trajectory constructed from initial data x 1 , . . . , x n , where x k is a realization of X k . An order variable, that can be seen as an order of selection for the points in the trajectory, is constructed using a recursive algorithm initiated from the first order point x (1) which is arbitrarily chosen (see [START_REF] Dematteï | Arbitrarily Shaped Multiple Spatial Cluster Detection for Case Event Data[END_REF] for a discussion about the choice of the first point). Then, let x (k) be the point with selection order k. Given x (1) , . . . , x (k) , the point x (k+1) is the nearest point from x (k) among the n -k points not yet selected. A trajectory that links successively each point to the next order point is thus defined. The algorithm used to determine the trajectory is presented in Table 1.

We can now define the distance variable D k = d(X (k) , X (k+1) ) from one point to its nearest neighbour.

d k = d(x (k) , x (k+1)
) is a realization of D k . This distance has to be weighted both to correct high distances due to the elimination process of pre-selected points and to adjust for a potential inhomogeneity in the underlying population density. The weighted distance d w k is defined as the ratio between the distance d k and its expectation under H 0 , the uniform distribution hypothesis. Dematteï et al. [START_REF] Dematteï | Arbitrarily Shaped Multiple Spatial Cluster Detection for Case Event Data[END_REF] have shown that the expected distance can be written [START_REF] Ripley | Modelling spatial patterns[END_REF] in which f (x) is the underlying density from which the n points are sampled independantly, S(x, r) is the sphere centered in x with radius r, and

E H 0 D k /X (1) = x (1) , . . . , X (k) = x (k) = a 0   1 - A k-1 S(x (k) ,r) f (x)dx A k-1 f (x)dx   n-k dr,
A k = A k i=1 S(x (i) , d i ) with the convention A 0 = A.
The numerical integration of a 0 in Equation ( 1) is achieved by using the trapezoidal rule. Moreover, the underlying population Z, constituted by N individuals {z i : i = 1, . . . , N}, allows to estimate the density integrals A k-1 and A k-1 S(x (k) ,r) . For any set B ⊂ A, B f (x)dx can be approximated by #{i/z i ∈ B}/N. This integral approximation allows to adjust the computation of d w k for inhomogeneous population. This adjustment is important since, with rare diseases, a large study area is necessary to examine data for evidence of spatial clustering. Hence, due to a natural inhomogeneity, the density of population at risk is not constant over the study area.

Cluster location and detection

Cluster bounds can now be determined from transformed data (k, d w k ) k=1,...,T in which T = n -1. For this purpose we consider the weighted distance regression on the selection order k. To determine the presence of m breaks (denoted by T 1 , . . . , T m ), the regression function taken into consideration is:

f (t) = m+1 j=1 d [T j-1 +1;T j ] × I [T j-1 +1;T j ] (t) (2)
with the convention T 0 = 0 and T m+1 = T . The notation

d [T j-1 +1;T j ] indicates the mean of d w t for t in [T j-1 + 1; T j ].
The minimum percentage of points between two breaks is a parameter which have to be taken into account. Let ǫ ∈ [0; 1] be this parameterµ. Then, the set of possible partitions is

∆ ǫ = {(T 1 , . . . , T m ) ; ∀i = 1, . . . , m + 1, card ([T i-1 + 1; T i ]) ≥ |T ǫ|}.
Breaks (cluster bounds) are estimated by ( T1 , . . . , Tm ) = argmin

(T 1 ,...,Tm)∈∆ǫ T t=1 (d w t -f (t)) 2 , (3)
and are computed efficiently using a dynamic algorithm programming presented in section 3.5.

The double maximum test proposed by Bai and Perron [START_REF] Bai | Estimating and testing linear models with multiple structural changes[END_REF] is used to select the best model. This test allows to test the the null hypothesis of no break against an unknown number of breaks given a certain upper bound M. Once the best model is selected, a p-value is computed for each portion between two breaks by a Monte Carlo procedure.

Package description

In this section, the content of the package is presented and the algorithms for the data transformation and the break location are emphasized. A flow chart describing this package is presented in Figure 1. The package implements essentially the method described in the previous section and its main function is clus( ). Because the spatial scan statistic [START_REF] Kulldorff | A spatial scan statistic[END_REF] is a reference method, the package contains also an exportation module in the SatScan format [START_REF] Kulldorff | Information Managements Services, Inc. SaTScan v5.1: Software for the spatial and space-time scan statistics[END_REF].

[Fig. 1 about here.]

User interface

Once R has started up, a window called "R Console" appears. Within this window, the user types his commands and R displays the results of the required computations. Each command must be written at the right side of the ">" symbol. The result of a command can be stored in a R object by using the "< -" assignement operator. All the functions are called in the same way. For example the command resclus < -clus(data = data ex, pop = pop ex, limx = c(0, 1), limy = c(0, 1))

will analyze the case coordinate data set data ex with the population coordinate data set pop ex. The study area is here defined to be the unit square. The results of this analysis will be store in a R list object called resclus.

In order to be able to use the SPATCLUS package, the user has to type the command > library(spatclus)

which will load the package.

Data input

In 2D, the clus( ) function has 4 essential arguments that have to be specified:

data: Data frame with 2 colums giving coordinates of cases. pop: Matrix with 2 columns giving coordinates of underlying population individuals. This matrix is called grille in the R programs. limx: 2 element vector containing the study area bounds of the X-axis. limy: 2 element vector containing the study area bounds of the Y-axis.

In 3D, the user also has to specified the parameter limz, a 2 element vector containing the study area bounds of the Z-axis.

Optional parameters

The clus( ) function also has several optional arguments that affect the different stage of the method. Default values (DF) are given for these parameters:

• Data input: dataincyn (DF="n"): "y" means that cases are already included in the underlying population. "n" means appends that they are not and appends data to pop . rndm (DF=NaN): Vector that identifies the rows containing cases coordinates in the grid (only if datainc="y"). for Poisson model, 3 for both models. export (DF="n"): If method = 2 or method = 3, and if export = "y", the data will be exported in "repexport" directory in SatScan software format. repexport (no DF): If export = "y", defines the directory in which data will be exported in SatScan software format.

Data transformation algorithm

In this section, the algorithm used for the determination of the trajectory and the distance weighting is presented. The corresponding methodology is described in section 2.1.

In the algorithm given in Table 1 and written in pseudocode, data = {x 1 , . . . , x n } is the set of the n case locations and pop = {u 1 , . . . , u N } is the set of the N individual locations that belongs to the underlying population. The trajectory is initialized by chosing x (1) in the data set, and we consider it as given in the algorithm. This choice is debated in [START_REF] Dematteï | Arbitrarily Shaped Multiple Spatial Cluster Detection for Case Event Data[END_REF]. For a better comprehension, we chose to use a set language rather than a matrix language.

[Table 1 about here.] Some explanations are necessary for a complete understanding of the correspondance between quantities used in this algorithm and those used in Equation (1). In the k th iteration of the global "counting" loop:

• after the IF block, pop represents A k-1 and #pop is used to approximate the quantity N × A k-1 f (x)dx, • in the nested "counting" loop, rpop represents A k-1 S(x (k) , r) and #rpop is used to approximate the quantity

N × A k-1 S(x (k) ,r) f (x)dx,
• the nested "counting" loop allows to compute the quantity pas × S -1 2 that represents an estimation of

a 0   1 - A k-1 S(x (k) ,r) f (x)dx A k-1 f (x)dx   n-k dr using the trapezoidal rule,
• the last step is to store the coordinates x (k) of the k th case of the trajectory along with its associated weighted distance d w k .

Break location using a dynamic programming algorithm

Consider the regression of the ordered series of the weighted distances {d w k : k = 1, . . . , n-1} on the selection order k. The regression function is given in Equation [START_REF] Whittemore | A test to detect clusters of disease[END_REF]. In order to determine the break locations for the m-break model in Equation ( 3), we used the dynamic programming approach proposed by Bai and Perron [START_REF] Bai | Computation and analysis of multiple structural change models[END_REF] that permits to reduce considerably the computing time. The algorithm given in Table 2, separated in two parts, is a translation in pseudocode langage of this method.

The ǫ parameter and the optimal partition ( T1 , . . . , Tm ) are defined in section 2.2.

[Table 2

about here.]

This algorithm gives a complete description of the way to compute the break locations. In the first part, the sum of squared residuals denoted by ssr i,j are computed only for segments [i; j] that are necessary in the m-break determination. In the second part, the optimal partition is obtained by solving the recursive problem S r,j = min rh≤i≤j-h [S r-1,i + ssr i+1,j ] in which S r,j denotes the sum of squared residuals associated with the optimal partition containing r breaks using the first j observations.

Data output and plotting

The output of the clus( ) function is a list of objects that contains: res: A result matrix giving, for each point ordered by its rank in the trajectory, its distance to the nearest neighbourg, the expentancy of this distance, and its weighted distance. pop: A matrix with 2 or 3 columns (depending on wether 2D or 3D data) giving coordinates of underlying population data points. bc: A list of vectors of size 1 to M. The k th element of the list gives the estimated breaks for the model with k breaks. stat: A list of non corrected statistic values (F ), corrected statistic value (wdm), threshold value for the WDM statistic (wdms), significativity (signif ) and the number of breaks that maximizes the WDM statistic (kmax). kulld.p: A vector giving the results of the spatial scan method with the Poisson model. lambda is the value of the spatial scan test statistic, loglambda is its logarithm, cx and cy are the coordinates of the circle center and rayon is its radius. kulld.b: A vector giving the results of the spatial scan method with the Bernouilli model. lambda is the value of the spatial scan test statistic, loglambda is its logarithm, cx and cy are the coordinates of the circle center and rayon is its radius.

This list of objects can be used as argument in both plotting functions. The function plotreg( ) displays the selection order in the X-axis, the weighted distance in the Y-axis and draws the regression function with k breaks. The function plotclus( ) displays the point cloud and located cluster(s) with the k-break model. k is generally equal to the value of the stat$kmax.

Exportation module in SatScan format

In this module, the cluster location by the spatial scan statistic [START_REF] Kulldorff | A spatial scan statistic[END_REF] is implemented, but p-value is not provided. For a full analysis with this method, including cluster detection via Monte Carlo replications, one can use the SatScan software [START_REF] Kulldorff | Information Managements Services, Inc. SaTScan v5.1: Software for the spatial and space-time scan statistics[END_REF] freely available. The SPATCLUS package allows user to export the data in a format directly usable by this software. For this purpose, one can use the following parameter values: method = 3 methk = 1 or 2 (Bernouilli or Poisson model) export = "y" repexport = "dir". dir denotes the directory path in which the data will be exported in SatScan format.

Sample runs

In order to illustrate the flexibility of the method, we simulated two 200-points samples. The first sample contains two simulated potential clusters with different shapes (a parallelogram and a "L"-shaped polygon) with a density inside about 6 times higher than outside. The second sample contains four simulated potential clusters: the same than previously plus two squares. A uniform 3000-point grid was attributed to each sample in order to represent the underlying population.

We analysed those samples with M = 8 as maximum number of breaks and ǫ = 0.1 as minimum number of points between two breaks. The critical value corresponding to these parameter values is 10.7. For the 2-cluster sample, the 4-break (2-cluster) model was selected and the W D max statistic value was 24.2. For the 4-cluster sample, the 8-break (4-cluster) model was selected and the W D max statistic value was 38.9. The no-cluster hypothesis was rejected is both samples and the model with 4 breaks (respectively 8 breaks) was selected. All the clusters were significant.

The regression plot and the cluster location result are presented for both samples in Figure 2.

The spatial scan statistic [START_REF] Kulldorff | A spatial scan statistic[END_REF] was applied on the two samples. The exportation module was used to put data into the right format and analyze them with the SatScan software [START_REF] Kulldorff | Information Managements Services, Inc. SaTScan v5.1: Software for the spatial and space-time scan statistics[END_REF]. In both cases, the most likely cluster (represented by a cercle in Figure 2) was significant.

[Fig. 2 about here.]

fMRI application

A way of applying this method to functional Magnetic Resonance Imaging (fMRI) data is proposed. fMRI is a technique for determining which parts of the brain are activated under different type of experimental conditions. The standard statistical method in analysing fMRI data is based on Statistical Parametric Mapping (SPM) [START_REF] Frackowiak | Imaging neuroscience -Theorie and analysis[END_REF].

The aim of the application of the cluster detection method to fMRI data is to locate clusters which correspond to brain regions simultaneoulsy activated for most subjects. The process consists first in determining activation peaks for each subject by the standard SPM method. Then the peaks of all the subjects are grouped together, which forms a 3D data set. Finally, the cluster detection method is applied to this data set in order to locate and detect clusters of activation peaks.

A word fluency task was given to 11 right-handed women within a classical fMRI block design with 5 control conditions (counting task) and 5 activity conditions (word fluency task) alternately. During the activation conditions, subjects had to produce silently as many words as possible beginning with a orally presented letter. The control condition consisted in counting forward from one, at a rate of about one a second.

The SPM method has been applied to each subject in order to detect significant hot spots (activation peaks) at an individual level. Each subject presents an average of 32 peaks. Then, those 354 peaks has been merged together and analysed with our method in order to determine, at a group level, which cerebral zones are activated for most of the subjects. The model with 8 breaks (4 potential clusters) was selected and the W D max statistic value was 25.2, higher than the critical value. One of the 4 potential cluster was not significant, while the others were significant clusters (p ≤ 0.05).

Hence, three hot spot clusters have been detected, two located in the frontal lobe and the other in the occipital lobe, each containing between 36 and 39 peaks. Those activated brain regions are represented in the Figure 3. Except for one atypical subject presenting only one peak in one of the three clusters, all the others present between 2 and 5 hot spots in each cluster. Those three clusters correspond to brain regions simultaneoulsy activated for most subjects.

Moreover, the spatial scan statistic [START_REF] Kulldorff | A spatial scan statistic[END_REF] was applied to this 3D data set. The maximum spatial cluster size was initially set to 50% of population at risk (default value of SatScan). With this value, the most likely cluster groups together 261 cases among the 354 total number of cases, more than half of cases. Finally, we set this value to 30%. The most likely cluster is a sphere with centre at (9, -5, -53) and radius 54.65. This significant cluster groups together 151 cases and is shown in Figure 3 by a transparent white sphere. Here, we can see that the spatial scan statistic fails: this approach detects a very large cluster which is not interpretable.

[Fig. 3 about here.]

5 Hardware and software specifications

The implemention and sample runs of this package was conducted on a 2GHz PC computer under the MandrakeLinux 9.2 distribution using the R software version 1.9.0 (CRAN, the "Comprehensive R Archive Network"). However, R runs in any OS platform (MAC, UNIX, Windows) and can be obtained freely via the different CRAN mirrors. All the mirrors URLS are available via the CRAN link on the R homepage at http : //www.r -project.org/. Hence, the SPATCLUS package can be installed in any platform.

Online availability

The SPATCLUS package (link "Télécharger l'outil") and the package documentation (link "Voir la notice d'information") are available over the web via the "Thèmes de recherche" tab on the IURC biostatistical laboratory website at following URL http : //www.iurc.montp.inserm.f r/biostat/. The package downloadable file is a ".tar.gz" archive that can be easily installed on the R software using the command "R CMD INSTALL spatclus" from source on UNIX, or "Rcmd INSTALL spatclus" on Windows. Further informations on R packages installation can be found in the "R Installation and Administration" manual available on the R homepage.

Discussion

This paper describes an R package that implements a new spatial cluster detection method. This description and the package documentation are complementary to help users to apply the method both easily and correctly, or for example to conduct valuable power comparisons between different methods.

The main difficulties in the implementation of the method are the distance weighting and the break location. The first algorithm presented allows to enlighten the numerical computation of the distance expectation in the weighting process. The second algorithm is a detailed version of the dynamic programming algorithm presented by Bai and Perron. This method allows to compute the break estimates using at most least-squares operations of order O(T 2 ) for any number of breaks m. This means that it is only marginally longer to obtain the optimal partition with 8 breaks as it is with 2 breaks.

The method implemented in the SPATCLUS package has the advantage of being very flexible. Firstly, it can be used to detect and locate several clusters, with no need to adjust for the multiple testing problem. Secondly, since the method does not need the definition of a predefined shape for potential clusters, the clusters detected can be of any shape. Moreover, since case event data are used, the method is free from map partition. Finally, a potential inhomogeneity in the underlying population distribution is taken into account through the weighting process.

List of

  • Trajectory: start (DF=1): Indicates the rank of the first trajectory point in term of distance from the area edges. 1 means that the first point of the trajectory is the nearest from the edge. • Cluster location and detection: m (DF=5): Maximum number of breaks. eps (DF=0.2): Minimum size of cluster (ratio of the total number of cases). • Spatial scan statistic location and module of exportation in SatScan format: method (DF=1): 1 for multiple break clusters, 2 for spatial scan statistic location, 3 for the 2 methods. methk (DF=3): In the spatial scan statistic location, 1 for Bernoulli model, 2

Figures 1 Flow chart describing the package. 16 2

 12 Results for the 2-and 4-cluster models on simulated data . (a) and (c): Results of the regression of distance on the order respectively for the 2 and 4-cluster model. (b) and (d): Representation of the clusters located respectively by the 2 and 4-cluster model. Points located in the clusters are round points surrounded by a grey disc. Simulated cluster areas are represented in dotted lines. The most likely cluster located by the spatial scan statistic is represented by a cercle. 17

3

  3D representation of fMRI activation peaks (protocol described in Section 4.2). At the top: right-hand side view of the brain from the front. At the bottom: right-hand side view of the brain from the back. Each peak is represented by a little black cube. A line joins two peaks that are successive in the trajectory. Points included in a significant cluster are represented by a sphere or a big black cube. The most likely cluster detected by the spatial scan statistic is represented by a transparent white sphere. 18

Fig. 1 .

 1 Fig. 1. Flow chart describing the package.

Fig. 3 .

 3 Fig. 3. 3D representation of fMRI activation peaks (protocol described in Section 4.2). At the top: right-hand side view of the brain from the front. At the bottom: right-hand side view of the brain from the back. Each peak is represented by a little black cube. A line joins two peaks that are successive in the trajectory. Points included in a significant cluster are represented by a sphere or a big black cube. The most likely cluster detected by the spatial scan statistic is represented by a transparent white sphere.

FOR k = 1 to n - 1 IF k > 1 2 x 1 T ← n - 1 h 1 T1ENDFORIF m > 1 FOR r = 1 to m - 1 FOR

 11211111 THEN pop ← pop {u/d x (k-1) , u ≤ d x (k-1) , x (k) } ENDIF a k ← max u∈pop d x (k) , u SET S to 0 FOR r = 0 to a k by pas SET rpop to pop rpop ← rpop {u/d x (k) , u > r} S ← S + 1 -#rpop #pop n-k ENDFOR E[d k ] ← pas × S -1 (k+1) ← argmin x∈data d x (k) , x d k ← d x (k) , x (k+1) d w k ← d k E[d k ] data ← data {x (k) } PRINT x (k) , ← |T ǫ| FOR i = 1 to T FOR j = 1 to T IF j -i ≥ h -← argmin h≤j≤T -h [ssr 1,j + ssr j+1,T ] ENDIF FOR j = h to T S 0,j ← ssr 1,j j = (r + 1)h to T -(m -r)h S r,j ← min rh≤i≤j-h [S r-1,i + ssr i+1,j ] b r,j ← argmin rh≤i≤j-h [S r-1,i + ssr i+1,j ] ENDFOR ENDFOR S m,T ← min mh≤j≤T -h [S m-1,j ] Tm ← argmin mh≤j≤T -h [S m-1,j ] FOR k = m -1 to 1 Tk ← b k, Tk+1PRINT Tk ENDFOR ENDIF

Table 1

 1 Data transformation algorithm READ data, pop, pas, x[START_REF] Ripley | Modelling spatial patterns[END_REF]


Jaber Karimpour
email: karimpour@tabrizu.ac.ir

Ayaz Isazadeh
email: isazadeh@tabrizu.ac.ir

Ali A Noroozi
email: noroozi@tabrizu.ac.ir

Verifying Observational Determinism

Keywords: Secure information flow, Observational determinism, Verification, Bisimulation

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

To perform an effective security analysis of a given program, program model, security policy and attacker (observer) model should be defined precisely [START_REF] Balliu | Logics for information flow security: from specification to verification[END_REF]. In secure information flow analysis, the program model can be represented as a state machine, which produces a set of executions and is considered public knowledge. In this model, program variables are classified into different security levels. A nave classification is to label some variables as L, meaning low security, public information; and other variables as H, meaning high security, private information. The goal of a security policy is to prevent information in H from flowing to L and being leaked [START_REF] Smith | Principles of secure information flow analysis[END_REF], [START_REF] Sabelfeld | Language-based information-flow security[END_REF]. Other classifications of program variables are possible via a lattice of security levels [START_REF] Denning | A lattice model of secure information flow[END_REF]. In this case, the security policy should ensure that information flows only upwards in the lattice.

The security policy is a property that needs to be satisfied by the program model. The attacker is assumed to be able to observe program executions. Confidentiality policies are of major concern in security policies. These policies are connected to the ability of an attacker to distinguish two program executions that differ only in their confidential inputs. Noninterference is a confidentiality policy that stipulates an observer able to see only low security data (low observer) learns nothing about high security inputs by watching low security outputs [START_REF] Zdancewic | Observational determinism for concurrent program security[END_REF]. Observational determinism is another confidentiality policy which is a generalized notion of noninterference for concurrent programs. Inspired by earlier work by McLean [START_REF] Mclean | Proving noninterference and functional correctness using traces[END_REF] and Roscoe [START_REF] Roscoe | CSP and determinism in security modelling[END_REF], Zdancevic and Myers [START_REF] Zdancewic | Observational determinism for concurrent program security[END_REF] proposed observational determinism which requires the program to produce indistinguishable traces to avoid information leaks. Thus, a program satisfying this condition appears deterministic to a low observer who is able to observe low variables and unable to distinguish states which differ only in high variables. As stated by Huisman et al. [START_REF] Huisman | A temporal logic characterisation of observational de-terminism[END_REF] "concurrent programs are often used in a context where intermediate states can be observed." That's why Zdancevic and Myers require determinism on all the states of a trace, instead of final states. Observational determinism is a widely accepted security property for concurrent programs. Observational deterministic programs are immune to refinement attacks [START_REF] Zdancewic | Observational determinism for concurrent program security[END_REF], because observational determinism is preserved under refinement [START_REF] Clarkson | Temporal Logics for Hyperproperties[END_REF].

This paper concentrates on the problem of verifying observational determinism for concurrent programs. We define observational determinism in terms of stutter equivalence on all low variables. Our contributions include (1) a theorem showing that verifying secure information flow can be reduced to equivalence checking in the quotient system and (2) a sound model checking approach for verifying secure information flow in concurrent programs. In fact, our approach is the first that uses quotient space to reduce the state space and check for secure information flow simultaneously. We illustrate the progress made by the verification of a small example program. It is expected that these contributions constitute a significant step towards more widely applicable secure information flow analysis.

The remainder of the paper is organized as follows. In section 2, preliminaries are explained. In section 3, observational determinism is formally defined and section 4 discusses how to verify it. In section 5, some related work is discussed. Finally, Section 6 concludes, and discusses future work.

Preliminaries

In this section, at first we introduce the program model considered throughout the paper. Then, some preliminary concepts about bisimulation are discussed. Most of these preliminaries are taken from [START_REF] Baier | Principles of model checking[END_REF].

Definition 1 (Kripke structure). A Kripke structure KS is a tuple (S, →, I, AP, La) where S is a set of states, →⊆ S × S is a transition relation, I ⊆ S is a set of initial states, AP is the set of atomic propositions, and La : S → 2 AP is a labeling function. Here, atomic propositions are possible values of the low variables. KS is called finite if S and AP are finite. The set of successors of a state s is defined as P ost(s) = {s ∈ S|s → s }. A state s is called terminal if P ost(s) = ∅. For a Kripke structure modelling a sequential program, terminal states represent the termination of the program.

Definition 2 (Execution or Path).

A finite path fragment π of KS is a finite state sequence s 0 s 1 . . . s n such that s i ∈ P ost(s i-1 ) for all 0 < i ≤ n. An infinite path fragment π is an infinite state sequence s 0 s 1 s 2 . . . such that s i ∈ P ost(s i-1 ) for all 0 < i. A maximal path fragment is either a finite path fragment that ends in a terminal state, or an infinite path fragment. A path fragment is called initial if it starts in an initial state, i.e., if s 0 ∈ I. A path of KS is an initial, maximal path fragment. P aths(s) denotes the set of paths starting in s. All paths of a Kripke structure with no terminal state are infinite. Definition 3 (Trace). The trace of a path π = s 0 s 1 . . . is defined as T = trace(π) = La(s 0 )La(s 1 ) . . . . Thus, the trace of a path is the sequence of sets of atomic propositions that are valid in the states of the path. T [0] extracts the first atomic proposition of the trace, i.e., T [0] = La(s 0 ). Let T races(s) denote the set of traces of s, and T races(KS) the set of traces of the initial states of KS: T races(s) = trace(P aths(s)) and T races(KS) = ∪ s∈I T races(s).

Definition 4 (Combination of Kripke structures

KS 1 ⊕ KS 2 ). For KS i = (S i , → i , I i , AP, La i ), i = 1, 2: KS 1 ⊕ KS 2 = (S 1 S 2 , → 1 ∪ → 2 , I 1 ∪ I 2 ,
KS 1 KS 2 iff ∀T 1 ∈ T races(KS 1 )(∃T 2 ∈ T races(KS 2 ). T 1 T 2 )
Definition 6 (Stutter bisimulation). A stutter bisimulation for KS is a binary relation R on S such that for all (s 1 , s 2 ) ∈ R, the following three conditions hold: (1) La(s 1 ) = La(s 2 ). ( 2

) If s 1 ∈ P ost(s 1 ) with (s 1 , s 2 ) ∈ R, then there exists a finite path fragment s 2 u 1 . . . u n s 2 with 0 ≤ n and (s 1 , u i ) ∈ R, i = 1, . . . , n and (s 1 , s 2 ) ∈ R. (3) If s 2 ∈ P ost(s 2 ) with (s 1 , s 2 ) ∈ R, then there exists a finite path fragment s 1 v 1 . . . v n s 1 with 0 ≤ n and (v i , s 2 ) ∈ R, i = 1, . . . , n and (s 1 , s 2 ) ∈ R.
Definition 7 (Divergence stutter bisimulation). Let R be an equivalence relation on S. A state s ∈ S is R-divergent if there exists an infinite path fragment π = ss 1 s 2 • • • ∈ P aths(s) such that (s, s j ) ∈ R for all 0 < j. Stated in words, a state s is R-divergent if there is an infinite path starting in s that only visits states in

[s] R . [s] R is the equivalence class of s under the equivalence relation R. R is divergence-sensitive if for any (s 1 , s 2 ) ∈ R: if s 1 is R-divergent, then s 2 is R-divergent. States s 1 , s 2 are divergent stutter bisimilar, denoted s 1 ≈ div s 2 , if there exists a divergence sensitive stutter bisimulation R such that (s 1 , s 2 ) ∈ R.

Definition 8 (Divergent stutter bisimilar paths). For infinite path fragments π

i = s 0,i s 1,i s 2,i . . . , i = 1, 2 in KS, π 1 is divergent stutter bisimilar to π 2 , denoted π 1 ≈ div π 2 if
and only if there exists an infinite sequence of indices 0 = j 0 < j 1 < j 2 < . . . and 0 = k 0 < k 1 < k 2 < . . . with:

s j,1 ≈ div s k,2 for all j r-1 ≤ j < j r and k r-1 ≤ k < k r with r = 1, 2, . . .
The following lemma follows directly from the definition of ≈ div on paths and on paths.

Lemma 1. For all infinite paths π 1 and π 2 , we have π 1 ≈ div π 2 implies π 1 π 2 . Lemma 2. Divergent stutter bisimilar states have divergent stutter bisimilar paths:

s 1 ≈ div s 2 implies ∀π 1 ∈ P aths(s 1 ) (∃π 2 ∈ P aths(s 2 ). π 1 ≈ div π 2 )
Proof : see [START_REF] Baier | Principles of model checking[END_REF], page 549.

Definition 9 (Divergence stutter bisimulation quotient KS/ ≈ div ). The quotient of a Kripke structure KS is defined by KS/ ≈ div = (S/ ≈ div , → , I , AP, La ), where

S/ ≈ div = {[s] ≈ div |s ∈ S}, La ([s] ≈ div ) = La(s), and → is defined by s → s ∧ s ≈ div s [s] ≈ div → [s ] ≈ div and s is ≈ div -divergent [s] ≈ div → [s] ≈ div Theorem 1.
For any Kripke structure KS, we have KS ≈ div KS/ ≈ div .

Proof : Follows from the fact that R = {(s, [s] ≈ div )|s ∈ S} is a divergence stutter bisimulation for (KS, KS/ ≈ div ).

Observational Determinism

A concurrent program is secure if it appears deterministic to a low observer and produces indistinguishable executions. Zdancevic and Myers [START_REF] Zdancewic | Observational determinism for concurrent program security[END_REF] call this observational determinism and define it as:

∀ T, T ∈ T races(P ). T [0] = L T [0] =⇒ T ≈ L T
where KS is a model of the program (e.g., a Kripke structure, modelling the program executions). Indistinguishability to a low observer is expressed as state equivalence relation = L and trace equivalence relation ≈ L . Zdancevic and Myers define trace equivalence as prefix and stutter equivalence of the sequence of states in each trace. However, Huisman et al. [START_REF] Huisman | A temporal logic characterisation of observational de-terminism[END_REF] argue that allowing prefixing causes information flows. That's why they propose stutter equivalence instead of prefix and stutter equivalence. For example, consider the following program:

l :=0; while (h >0) then { l ++} ( P1 )
where h is a high variable and l is a low veriable. The set of traces of this program is {< 0 >, < 0, 1 >, < 0, 1, 2 >, . . . }. These traces are prefix and stutter equivalent, hence considered secure by the definition of Zdancevic and Myers; But, the attacker can easily get the value of h by observing the traces. Huisman et al. [START_REF] Huisman | A temporal logic characterisation of observational de-terminism[END_REF] require stutter equivalence of traces of each low variable, but as Terauchi [START_REF] Terauchi | A type System for observational determinism[END_REF] shows, this kind of definition is not as restrictive as possible and accepts leaky programs. Thus, Terauchi requires prefix stutter equivalence of all traces w.r.t. all low variables. Consequently, we define observational determinism in terms of stutter equivalence on all low variables:

∀ T, T ∈ T races(P ). T [0] = L T [0] =⇒ T L T
where L is stutter trace equivalence. For example, consider the following insecure program that can reveal the value of h:

l 1 :=0; l 2 :=0; l 1 :=1 || if ( l 1 =1) then l 2 := h ( P2 )
where || is the parallel operator. If the right program is executed first, the corresponding trace of low variables would be: < (0, 0), (0, 0), (1, 0) >. Each ordered pair (l 1 , l 2 ) shows the values of low variables in each state of the program. If the left program is executed first, the following traces are produced: < (0, 0), (1, 0), (1, h) >. As you can see, these traces are not stutter equivalent, so the program is insecure. As another example, consider the following secure program:

l 1 :=0; l 2 :=0; l 1 :=2 || if ( l 1 =1) then l 2 := h ( P3 )
If the right program is executed first, the corresponding trace would be: < (0, 0), (0, 0), (2, 0) >, but if the left program is executed first, the following trace is produced: < (0, 0), (2, 0), (2, 0) >. These two traces are stutter equivalent, hence the program is secure. Thus, this paper defines trace indistinguishability in observational determinism as stutter equivalence.

Verification of Observational Determinism

Let us assume KS = (S, →, I, AP, La) is a Kripke structure that models the behavior of the concurrent execution of the processes (or threads) of a concurrent program. AP is the set of the values of low variables and the function La labels each state with these values. It is assumed that the state space of KS is finite.

If KS has a terminal state s n , we include a transition s n → s n , i.e., a self-loop, ensuring that the Kripke structure has no terminal state. Therefore, all traces of KS are infinite.

The main steps of the verification algorithm are outlined in Algorithm 1. The input of this algorithm is a finite Kripke structure KS modeling the program, and the output is yes or no. The first step is to partition the set I of initial states into sets of low equivalent initial states called initial state clusters ISC 1 , . . . , ISC m , and define ISC = {ISC 1 , . . . , ISC m }. The second step is to extract an arbitrary trace T i from KS for each initial state cluster and build a Kripke structure KST i from the path in KS corresponding to trace T i . As the next step, we combine Kripke structures KST i (i = 1, . . . , |ISC|), forming a single Kripke structure KST = (S KST , → KST , I KST , AP KST , La KST ), where

KST = KST 1 ⊕ KST 2 ⊕ . . .
∀C ∈(S S KST )/ ≈ div KS⊕KST , ∀s 0 , s 0 ∈ ISC i , 1 ≤ i ≤ |ISC|. s 0 ∈ C ⇔ s 0 ∈ C and ISC i ∩ C = φ ⇔ I KST ∩ C = φ
where stands for disjoint union and (S S KST )/ ≈ div KS⊕KST denotes the quotient space with respect to ≈ div KS⊕KST , i.e., the set of all divergence stutter bisimulation equivalence classes in S S KST .

Proof : To prove that KS is observational deterministic, one should prove that for every initial state of KS, all traces starting in that state are stutter equivalent. Thus, for all traces starting from an initial state s 0 of KS, there should be a stutter equivalent trace of KST starting from an initial state st 0 of KST . By Lemma 1, stutter equivalence of traces reduces to divergence stutter bisimulation. From Lemma 2, it follows that each initial state of KS should be divergent stutter bisimilar to an initial state in KST , and vice versa. Thus, KS and KST should be divergent stutter bisimilar. Then, KS ≈ div KST if and only if ∀C ∈ (S S KST )/ ≈ div KS⊕KST . I = φ ⇐⇒ I KST = φ where (S S KST )/ ≈ div KS⊕KST denotes the quotient space with respect to ≈ div KS⊕KST . Considering that some initial states may be low equivalent and consequently they form initial state clusters, it is sufficient to take an arbitrary trace for only each initial state cluster. Of course, all states of an initial state cluster should have stutter equivalent traces and thus should be divergent stutter bisimilar. As a result, KS is observational deterministic if and only if

∀C ∈ (S S KST )/ ≈ div KS⊕KST , ∀s 0 , s 0 ∈ ISC i , 1 ≤ i ≤ |ISC|. s 0 ∈ C ⇔ s 0 ∈ C and ISC i ∩ C = φ ⇔ I KST ∩ C = φ
The input finite Kripke structure KS has no terminal states. Hence, all traces are infinite and form a cycle in KS. To take an arbitrary trace from KS, we can use cycle detection algorithms of graphs. In order to detect cycle, a modified depth first search called colored DFS may be used. In colored DFS, all states are initially marked white. When a state is encountered, it is marked grey, and when its successors are completely visited, it is marked black. If a grey state is ever encountered, then there is a cycle and sequence of states pushed in the stack of the DFS so far forms a path.

It remains to explain how to compute divergence stutter bisimulation quotient of KS ⊕ KST . The algorithm to compute the quotient relies on a partition refinement technique, where the finite state space S S KST is partitioned in blocks. Starting from a straightforward initial partition, where all states with the same label (low variable values) form a partition, the algorithm successively refines these partitions until a stable partition is reached. A partition is stable if it only contains divergent stutter bisimilar states and no refinement is possible on it. Further details can be found, e.g. in [START_REF] Groote | An efficient algorithm for branching bisimulation and stutter-ing equivalence[END_REF], [START_REF] Baier | Principles of model checking[END_REF].

Complexity. The time complexity of finding an arbitrary trace is O(M ), where M denotes the number of transitions of KS. Thus, the time complexity of constructing KST is O(|I|.M ). The quotient space of KS ⊕KST under ≈ div can be computed in time O((|S| + M ) + |S|.(|AP | + M )) under the assumption that M |S| [START_REF] Baier | Principles of model checking[END_REF]. Thus, the costs of verifying observational determinism for concurrent programs are dominated by the costs of computing the quotient space under ≈ div , which is polynomial-time.

Using the quotient space to verify observational determinism has two advantages: (1) Instead of analyzing the concrete model of the program, a minimized abstract model is analyzed. Provided the quotiening preserves stutter equivalence, the analysis of the minimized model suffices to decide the satisfaction of observational determinism in the program. [START_REF] Smith | Principles of secure information flow analysis[END_REF] The proposed approach can easily be adapted to verify programs with infinitely many states, as there are efficient algorithms for computing the quotient space of infinite state programs [START_REF] Chutinan | Verification of infinite-state dynamic systems using approxi-mate quotient transition systems[END_REF].

Example. Consider the following program from [START_REF] Ngo | Qualitative and quantitative information flow analysis for multi-thread pro-grams[END_REF]: where h is a boolean and high variable and l is a low variable. The Kripke structure KS of the program P4 and the Kripke structure KST of an arbitrary trace of KS are shown in Figure 1. The equivalence classes of KS ⊕ KST under

≈ div are [s 0 ] div = {s 0 , s 7 }, [s 1 ] div = {s 1 , s 8 , st 0 , st 1 }, [s 2 ] div = {s 2 , s 9 , st 2 }, [ s 3
] div = {s 3 , s 10 , s 11 , st 3 }, [s 4 ] div = {s 4 , s 5 , s 12 , s 13 , s 14 } and [s 6 ] div = {s 6 , s 15 }. Therefore, the divergence stutter bisimulation quotient of it is computed as depicted in Figure 2. Since the initial state s 0 of KS and the initial state st 0 of KST are not in the same equivalence class, the program is labelled as insecure.

Related Work

Zdancevic and Myers [START_REF] Zdancewic | Observational determinism for concurrent program security[END_REF] define observational determinism in terms of prefix and stutter equivalence each low variable. Huisman et al. [START_REF] Huisman | A temporal logic characterisation of observational de-terminism[END_REF] show that allowing prefixing permits some leaks, so they define observational determinism in terms of stutter equivalence on each low variable. Terauchi [START_REF] Terauchi | A type System for observational determinism[END_REF] shows that independent consideration of low variables is not correct and information flows may occur. Hence, he proposes prefix and stutter equivalence on all low variables. Huisman and Blondeel [START_REF] Huisman | Model-checking secure information flow for multithreaded programs[END_REF] define observational determinism in terms of stutter equivalence on all low variables. Ngo et al. [START_REF] Ngo | Effective verification of confidentiality for multi-threaded programs[END_REF] defines observational determinism with two conditions: condition 1 requires stutter equivalence on each low variable and condition 2 requires stutter equivalence on all low variables. Ngo et al. argue that a concurrent program satisfying both of these conditions is secure.

A common approach to verify information flow properties is the use of type systems. A type system is a collection of type inference rules for assigning types to variables of a programming language and making judgments about programs [START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. With a type system developed for secure information flow, a program can be type checked for secure-flow violations [START_REF] Smith | Secure information flow in a multi-threaded imperative language[END_REF]. But type systems are not extensible, as for each variation of confidentiality policy and programming language to be verified, a new type system should be redefined and proven sound. For more details about disadvantages of type systems, see [START_REF] Barthe | Secure information flow by self-composition[END_REF].

Accordingly, logic-based verification and model checking has been advocated. But as security policies are not trace properties [START_REF] Mclean | Proving noninterference and functional correctness using traces[END_REF], [START_REF] Clarkson | Hyperproperties[END_REF], standard logic-based verification and model checking methods can't be utilized and need to be modified. Trace properties, e.g. safety or liveness properties [START_REF] Baier | Principles of model checking[END_REF], are properties of individual traces; But most of security policies, such as secure information flow, are properties of sets of traces, called hyperproperties [START_REF] Clarkson | Hyperproperties[END_REF]. For instance, observational determinism is a hyperproperty because a trace is allowed if it is indistinguishable from all other traces having the same low vales. Various attempts for logical specification of information flow properties has been made. One promising one is self-composition which composes a program with a copy of it, with all variables renamed. Then, the problem of verifying secure infor-mation flow is reduced to a trace property for the composed program. Huisman and Blondeel [START_REF] Huisman | Model-checking secure information flow for multithreaded programs[END_REF] use this idea to model check observational determinism for multi-threaded programs. They specify observational determinism in µ-calculus. A disadvantage with these kinds of methods that exploit logical verification and self-composition is the common problem of state space explosion [START_REF] Clarke | The birth of model checking[END_REF], [START_REF] Emerson | The beginning of model checking: A personal perspective[END_REF].

The concept of stutter equivalence in the definition of observational determinism brings weak bisimulation to mind. Ngo et al. [START_REF] Ngo | Effective verification of confidentiality for multi-threaded programs[END_REF] use bisimulation to verify observational determinism in multi-threaded programs. They make a copy of the program for each initial state of the program and check bisimilarity of each pair of the programs after removing stutter steps and determinizing them. But the cost of determinizing a program is exponential in the size of the program. This method suffers from state space explosion problem too, as it makes a copy of the program for each initial state of it.

Another line of research for verifying hyperproperties is to extend temporal logics and introduce new logics to specify these properties. Many attempts have been made, including HyperLTL, HyperCTL* [START_REF] Clarkson | Temporal Logics for Hyperproperties[END_REF], HyperCTL [START_REF] Finkbeiner | A temporal logic for hyperproperties[END_REF], SecLTL [START_REF] Dimitrova | Model checking infor-mation flow in reactive systems[END_REF], etc. Clarkson et al. [START_REF] Clarkson | Temporal Logics for Hyperproperties[END_REF] specify observational determinism and many other security properties in HyperLTL and provide model checking techniques for verifying HyperLTL and HyperCTL*. Finkbeiner et al. [START_REF] Finkbeiner | A temporal logic for hyperproperties[END_REF] introduce HyperCTL, which extends CTL* with path variables. They reduce the model checking problem for HyperCTL to the satisfiability problem for QPTL to obtain a model checking algorithm for HyperCTL. Dimitrova et al. [START_REF] Dimitrova | Model checking infor-mation flow in reactive systems[END_REF] add a new modal operator, the hide operator, to LTL and name the resulting logic SecLTL. They propose an automata-theoretic technique for model checking SecLTL.

A similar research to our work is Mantel's unwinding possibilistic security properties [START_REF] Mantel | Unwinding possibilistic security properties[END_REF]. In this work, he proposes a modular framework in which most security properties can be composed from a set of basic security predicates (BSPs); he also presents unwinding conditions for most BSPs. These unwinding conditions can be seen as simulation relations on system states. Intuitively, unwinding conditions require that each high transition is simulated in such a way that a low observer cannot infer whether such high transition has been performed or not. Thus the low observation of the process is not influenced in any way by its high behavior. In 2011, D'Souza et al. [START_REF] Souza | Model-checking trace-based infor-mation flow properties[END_REF] propose an automata-theoretic technique for model checking Mantel's BSPs. The proposed model checking approach is based on deciding set inclusion on regular languages.

Conclusion

This paper discusses a bisimulation-based approach for model checking observational determinism in concurrent programs. Concretely, we extract some trace(s) of the program and check stutter trace equivalence between the trace(s) and the program. This is done by computing a bisimulation quotient. The time complexity of the verification is polynomial. The advantage of our proposed approach is that the analysis is done on a minimized abstract model of the program. Hence, the state explosion problem may be avoided. Another advantage is that the approach can be easily adapted for infinite state programs.

As future work, we plan to implement the proposed approach. We will also study whether bisimulation-based modular minimization algorithms are appropriate for verifying observational determinism. We also aim to modify our algorithm and use compositional verification techniques to benefit from modular structure of the concurrent program.

Fig. 1 .

 1 Fig. 1. The Kripke structure KS of P5 and the Kripke structure KST of an arbitrary trace of KS

Fig. 2 .

 2 Fig. 2. The divergence stutter bisimulation quotient of KS ⊕ KST for P5

  AP, La) where stands for disjoint union and La(s) = La i (s) if s ∈ S i . , A 1 , A 2 , • • • ⊆ AP where A + i isthe Kleene plus operation on A i and is defined as A + i = {x 1 x 2 . . . x k |k > 0 and each x i = A i }. Kripke structures KS i over AP , i = 1, 2 , are stutter trace equivalent, denoted KS 1 KS 2 , if KS 1 KS 2 and KS 2 KS 1 , where is defined by:

	Definition 5 (Stutter equivalence). Traces T 1 and T 2 over 2 AP are stutter
	equivalent, denoted T 1	T 2 , if they are both of the form A + 0 A + 1 A + 2 . . . for
	A 0

  KST |ISC| . The following theorem reduces the problem of verifying observational determinism to checking divergence stutter bisimulation of KS and KST . Partition the set I of initial states into initial state clusters; 2 Take an arbitrary trace T i of KS for each initial state cluster; 3 Construct Kripke structure KST i from the path in KS corresponding to trace T i ; 4 Construct Kripke structure KST = KST 1 ⊕ KST 2 • • • ⊕ KST |ISC| ; 5 Compute divergence stutter bisimulation quotient of KS ⊕ KST ; 6 for each initial state cluster ISC i do 7 for each pair of initial states s 0 and s 0 in ISC i do

		input : finite Kripke structure KS modeling the program
		output: yes if the program satisfies observational determinism;
		Otherwise, no
	1 8	if [s 0 ] ≈ div KS⊕KST = [s 0 ] ≈ div KS⊕KST then
	9	return no;
	15	else
	16	end
	17 end
	18 return yes;
		Algorithm 1: Verification of observational determinism
		Theorem 2. The problem of the verification of observational determinism is
	reduced to the following problem:

10 else 11 end 12 for an arbitrary state s 0 in ISC i and its correspondent initial state st 0 in KST do 13 if [s 0 ] ≈ div KS⊕KST = [st 0 ] ≈ div KS⊕KST then 14 return no;


Chetan Bansal
email: chetanb@microsoft.com

Sören Preibusch

Natasa Milic-Frayling

Cache Timing Attacks revisited: efficient and repeatable browser history, OS and network sniffing

Keywords: Privacy, cache timing attacks, cyber-security, cyber-espionage, browser history sniffing

Cache Timing Attacks (CTAs) have been shown to leak Web browsing history. Until recently, they were deemed a limited threat to individuals' privacy because of their narrow attack surface and vectors, and a lack of robustness and efficiency. Our attack implementation exploits the Web Worker APIs to parallelise cache probing (300 requests/second) and applies time-outs on cache requests to prevent cache pollution. We demonstrate robust cache attacks at the browser, operating system and Web proxy level. Private browsing sessions, HTTPS and corporate intranets are vulnerable. Through case studies of (1) anti-phishing protection in online banking, (2) Web search using the address bar in browsers, (3) publishing of personal images in social media, and (4) use of desktop search, we show that CTAs can seriously compromise privacy and security of individuals and organisations. Options for protection from CTAs are limited. The lack of effective defence, and the ability to mount attacks without cooperation of other websites, makes the improved CTAs serious contenders for cyber-espionage and a broad consumer and corporate surveillance.

Introduction

Web caching is a common performance enhancing mechanism. It improves Web browsing speed, for the convenience of the consumer, and reduces the network traffic, thus decreasing the cost for the provider and the user. Caching is not limited to the Web browser but also used by the operating system and network proxies to improve the user experience (Fig. 1). This convenience comes at the cost of decreased user privacy since caches store persistent information that can be interrogated by attacker websites. Since the early Internet days, browsers have adopted the same-origin principle to limit the interaction between websites from different domains and to have cookies and JavaScript's from different sites coexist without interfering [START_REF]Mozilla Developer Network and individual contributors[END_REF]. However, this principle is not applied to the entire persistent browser state. The ability for one site to learn about visits of individuals to other sites has fuelled a lucrative Internet economy around advertising services and user tracking across websites [START_REF] Gomer | Network Analysis of Third Party Tracking: User Exposure to Tracking Cookies through Search[END_REF]. Despite the privacy risks, only rudimentary technical support and policy-based protection have been offered to users to control their exposure. At the same time, browsing history is considered personal information [START_REF] Carrascal | Your browsing behavior for a big mac: economics of personal information online[END_REF], and consumers dislike advertisers using their browsing history even when they are assured to remain anonymous [START_REF] Truste | Behavioral Targeting: Not that Bad?! TRUSTe Survey Shows Decline in Concern for Behavioral Targeting[END_REF].

While cookie-based user tracking is gaining attention of the general public and policy makers, privacy violations due to cache timing attacks (CTAs) are still an obscure matter. Whereas history sniffing through 'coloured hyperlinks' has been fixed by browser manufacturers, CTAs are harder to detect and difficult to prevent [START_REF] Felten | Timing attacks on web privacy[END_REF] [START_REF] Jackson | Protecting browser state from web privacy attacks[END_REF]. Instead of placing new objects into the cache, CTAs probe the cache for the existence of specific items and make inferences about user activities that leave traces in the cache (e.g., visits to websites). More precisely, the attackers time the browser's response to an item request to determine whether the item was cached (fast response) or fetched from the website (slow response). In the former case, they can conclude that the user has visited the Web resource in the recent past.

Since CTAs require active probing for specific items and careful measurement of the time responses, they have been considered limited in the damage they can cause and the scale they can achieve. A limiting factor in CTAs is the need to lure the victim to the attacker's Web page that hosts the JavaScript for carrying out the attack. Furthermore, a simplistic probing of the cache only allows one-time inquiry since checking for the presence of an item requires reading the corresponding file which is then added to the cache. This side effect contaminates (or 'pollutes') the cache and precludes iterative probing. We revisit the implementation of CTAs and investigate the scope of their effectiveness in the contemporary ecosystem.

New Web paradigms (e.g., HTML5 and AJAX) enable rich, interactive end-user applications. Modern browsers expose comprehensive APIs and position the browser as an 'operating system' that hosts third-party applications (e.g., Chrome OS). At the same time, the scope of Web activities has expanded considerably to include high-stakes activities such as banking, e-commerce, and e-governance that are attractive targets for attacks. Also, in online social media activities, personal information flows in abundance.

In this paper we demonstrate how CTAs can be implemented to overcome the discussed limitations. We use two specific techniques: (a) time-outs on cache requests and (b) multi-threaded cache probing using Web Worker APIs, to create repeatable and efficient CTAs, making them a serious contender for cyber-espionage and for individual and enterprise-level surveillance by any third party. As a consequence, CTAs become a serious privacy threat both to individuals and enterprises.

Our research makes the following contributions: (1) extended the scope of CTAs by including practical attacks on operating systems, browser components, banking and social websites, as well as first real-world, practical attacks on proxy caches that open door for enterprise level tracking and surveillance and (2) improved efficiency and repeatability of CTAs by eliminating cache 'contamination' during cache probing.

We begin by situating our work within CTA research and follow with the technical description of our approach. We present four case studies that demonstrate the improvements in CTAs. We then discuss remedies to reduce the damage of CTAs before concluding with the summary of our contributions and an outlook on future work.

2

Related work

Browsing history extraction

The ability of a website to probe whether a hyperlink is displayed as a visited link, through a CSS a:visited rule, was at the heart of the first sniffing attacks on browser history [START_REF] Wondracek | A Practical Attack to De-anonymize Social Network Users[END_REF]. Fortunately, the vulnerability due to the leak of the visited link colour has now been fixed by all major browser manufacturers, defending from attacks based upon it. Timing attacks have been well-known for over a decade but remained limited to browser caches and were not considered in detail to achieve robustness and scale. Image-loading times in a browser are a cache-based side channel that can leak information about browsing history. The initial discussion dates back to 2000 by Felten et al. [START_REF] Felten | Timing attacks on web privacy[END_REF] who introduced web timing attacks and showed how they can be used to compromise users' browsing histories. They also discussed timing attacks on DNS and proxy caches.

Considering further the cache timing for DNS and browser, Jackson et al. [START_REF] Jackson | Protecting browser state from web privacy attacks[END_REF] refined the same-origin policy to also cover the browser cache. They implemented their proposal as a Firefox extension, but the impact on the overall ecosystem remained small. The add-on gained no traction amongst users and browser vendors did not adopt the design [START_REF] Jackson | SafeCache: Add-ons for Firefox[END_REF]. We discuss mitigations in more detail in Section 5.

Cache timing for inference of private information and identity

More recently, targeted timing attacks have been shown to leak very specific information about the users. Jia et al. demonstrated leakage of users' geo-location through CTAs [START_REF] Jia | I Know Where You've Been: Geo-Inference Attacks via the Browser Cache[END_REF]. According to them, 62% of the Alexa top 100 websites enable attackers to infer users' geo-location based on cached resources. For instance, websites like Google or Craigslist are personalised by user location (e.g., country or city specific domains and URLs or location-sensitive images). However, due to the lack of empirical studies, user damages from the described leakage of country or city information are unclear. It seems that, unless geo-location attack is combined with other non-trivial attacks, it can only be exploited for targeted phishing attacks. The robustness and accuracy of the attack are questionable, as is the effectiveness with a cache lookup frequency of 5 to 10 URLs per second. In our work, we consider these limitations, as well as the repeatability of the attacks. Cache timing techniques also misuse the browser cache as a persistent data store, similar to cookies, and thus support identity attacks. Cache cookies can be created by interpreting each cache hit or miss as a single bit [START_REF] Felten | Timing attacks on web privacy[END_REF]. In this manner, a series of URLs can be used to persist several bits of information such as session ids or even unique tracking ids, despite the users' efforts to suppress cookies in their browsers. In the absence of access control for the browser cache, cache fingerprints can be read or written across origins akin to third-party cookies.

3

Attack principles and improvements Delivery of the attacks. CTAs can be executed without help from the legitimate site and by any Web-savvy user who is able to implement (or copy) a cache probing Java-Script. Delivery of a malicious JavaScript is not difficult to achieve due to the many ways to distribute URLs, including emails and social media. Advertisements and social networks are the most common channels to distribute JavaScript based malware [10] [11]. Cache probing JavaScripts can be embedded in advertising banners, or delivered through the attacker page by ensuring that it ranks high in search results.

Unlike other JavaScript attacks, like CSR, XSS, etc., timing attacks are based on a polling mechanism. The malicious script has to make a request for each URL and time the response to make an inference. The larger the number of URLs, the longer the script has to run. Thus, cache probing requires a very speed-efficient attack. Otherwise, the victim needs to be exposed to the attack for a prohibitively long time. Finally, previous attacks were limited in their scope; they could only be executed once due to cache contamination with requested URLs.

Attack deployment. Our CTA implementation does not require any custom hardware or software. We have tested the attacks on common browsers, OS, services and real world proxies and banking websites. Our exact setup was a Windows 8.1 PC, on the corporate network of the authors. Attacks are done using JavaScript which can be hosted on any website. The minimum browser requirements for the Web Worker API are Internet Explorer 10, Chrome 4 and Firefox 3.5. Some attacks, like the one described in Section 4.4, require the attacker to host a website within the intranet.

Improved CTAs

Overall performance. In order to make the timing attacks scalable and avoid cache contamination, we use Web Workers and timeouts on probing requests. Previously, cache contamination was avoided through the same-origin policy and iframes [START_REF] Zalewski | Chrome & Opera PoC: rapid history extraction through non-destructive cache timing[END_REF]. However, that approach requires DOM access which creates a considerable overhead and leads to poor performance. Furthermore, the DOM is not available to Web Workers due to concurrency issues. As seen in Fig. 2, our parallel implementation of cache attacks is 15 times more efficient than the best-performing approach so far: it takes 0.5 seconds to complete 150 requests, compared to 7.4 sec for the same 150 requests using the CoreDump algorithm [START_REF] Zalewski | Chrome & Opera PoC: rapid history extraction through non-destructive cache timing[END_REF]. It is also more resilient to cache contamination.

Web Workers. Prior to HTML5, JavaScript did not have any notion of multi-threading.

All the scripts on a given web page executed in a single thread. Asynchronous timers using setTimeout and setInterval functions were used to simulate multi-threading. With the introduction of Web Workers, concurrent background tasks can be spawned as OSlevel threads. The worker thread can perform tasks without interfering with the user interface. The feature is supported by all major desktop and mobile browsers. Our experimental setup included successful tests with Internet Explorer, Firefox, Chrome, and Opera.

Time-out. We use high resolution timeouts for the XMLHttpRequests to avoid cache contamination during attacks. Listing 1 shows a code snippet where we use very small timeout values (5ms) to terminate the request before it is completed. This makes sure that the cache does not include the requested URLs due to probing. The timeout value depends on the type of cache we probe (e.g., a browser or a proxy cache). We extensively tested the timeout technique using Chrome and Opera; similar can be done for other browsers. For attacking the browser cache, the timeout value of 5ms was sufficient while for proxies it was 15ms. The values vary based on the client configuration, bandwidth and network latency. The attacker can pre-compute these values for a specific victim by running benchmarks. We apply a simple method; for browser and proxy caches we make 5 requests, each for cached and un-cached resources, and calculate the mean and max timeout values.

Extended attack surfaces. First, we consider scenarios beyond the browsing history attacks and show that sensitive resources like security images, commonly used on banking website, and XML/JSON based API calls can be targeted to leak user's private information. Second, we exploit Web caches that are not limited to browsers but included in the operating system and network proxies.

Case studies

In this section we demonstrate how CTAs render existing anti-phishing defences useless (Section 4.1) and how they can be used to revive and improve previous user deanonymisation attacks (Section 4.2). We also present two novel case studies of CTAs applied to monitoring Web search and OS file-system queries (Sections 4.3 and 4.4).

Fig. 2.

Total time in seconds to complete 150 requests. Benchmark of our cache probing technique (single-threaded or multi-threaded) against the existing geo-inference algorithm [START_REF] Jia | I Know Where You've Been: Geo-Inference Attacks via the Browser Cache[END_REF] and the CoreDump algorithm [START_REF] Zalewski | Chrome & Opera PoC: rapid history extraction through non-destructive cache timing[END_REF]. Smaller numbers are better.

Online banking security images

Site-to-user is an anti-phishing product by RSA Security based on the challenge-response model. The product is used by major financial institutions like Virgin Money, HDFC Bank Ltd., and many others. Through Site-to-user a legitimate website can authenticate itself to the user and prove that it is not a phishing site. When a user creates her account, she is asked to choose an image and a text phrase as part of the Site-touser protection. Now, whenever the user visits the website to log-in, the same Site-touser image and text are displayed after she enters her customer id and before she enters her password. Thus, the user can verify that the site is legitimate.

The Site-to-user protection is not completely secure. It is vulnerable to man-in-themiddle attacks [START_REF] Youll | Fraud vulnerabilities in sitekey security at Bank of America[END_REF] where a malicious phishing website first asks the user to enter the customer id. Subsequently, serving as a proxy, the attacker makes a request to the real banking website to fetch the image and display it back to the user. Albeit simple to implement, this attack is also easy to detect in real-time because of multiple requests from different clients for the same customer id, in a very short time span.

We describe a new attack against Site-to-user that is difficult to detect by the banking service and equally difficult to prevent. In this instance a phishing site recovers the image directly from the user through a CTA. We confirmed the attack against a real banking website (Fig. 3).

Attack implementation.

Since the Site-to-user images are accessible to any individual at the time of subscribing to the service, the attacker has an opportunity to acquire the entire collection of images used by the service. This one-off effort in preparing the resources enables phishing attack across a broad population of customers. Figure 3 illustrates the time (in milliseconds) to get a response from the cache of the selected 283 Site-to-user images.

Responses by manufacturer. RSA Security acknowledged the vulnerability in both the on-premise and hosted versions of RSA Adaptive Authentication. They fixed the vulnerability by setting no-cache headers for the hosted deployment and they also communicated the mitigation to their on-premise customers. Fig. 3. Request response times in milliseconds for 283 Site-to-user images, colour-coded by magnitude. Green and framed, the correctly identified, cached image (2ms). Red, an outlier that does not impact the success of the attack (1600ms).

User identification in social networks

Social Networking Sites (SNS) like Facebook, Twitter or LinkedIn are among the most popular destinations on the Web [START_REF]Top Sites in United States[END_REF]. Facebook has more than 800 million daily active users [START_REF] Facebook | Company Info | Facebook Newsroom[END_REF]. SNS store and expose more current and historical personal information about their users and their relations than any other public websites. Personal data on SNS is not limited to personal information, like demographics (age, name, sex, etc.) and profile pictures, but often includes real-time location and status of offline/online friends [START_REF] Bonneau | The Privacy Jungle: On the Market for Data Protection in Social Networks[END_REF]. Social networking services used in the workplace include data about the organisation, internal team documents, and internal communication. They may also include more personal matter, such as job applications and inquiries of the team members. Linking and exposing such information could be incriminatory. Consequently, security and privacy attacks on these sites could have detrimental effects for their users.

Past SNS attacks involved methods for browser history sniffing based on CSS visited link vulnerability [START_REF] Wondracek | A Practical Attack to De-anonymize Social Network Users[END_REF], aiming to de-anonymise a person within a set of known users. While the CSS vulnerability has been fixed, alternative attacks resorted to the analysis of the Transport Layer Security (TLS) traffic. Because TLS does not hide the length of the response, user identification can be done based on the pre-computed size of the users' profile images [START_REF] Pironti | Identifying Website Users by TLS Traffic Analysis: New Attacks and Effective Countermeasures[END_REF].

Attack scenario. Methods for de-anonymising users can be applied to track audiences beyond SNS. For example, a marketing campaign team posts a link to the new promotion on the corporate Facebook page and wants to know who among the company's followers have clicked on the link. Such data is normally concealed from the company by the SNS platform due to privacy reasons. Similarly, in the case of a professional network like LinkedIn, clicks on job adverts could be traced and linked back to employees' profiles. The attack can also be used to circumvent privacy-enhancing techniques built into SNS, such as anonymous groups. Attack implementation. Our attack enables any malicious website to de-anonymise an SNS user by checking if she is within a pre-defined set of users. It exploits the mapping between SNS users and their unique, self-uploaded profile images, a defining feature of SNS [START_REF] Bonneau | The Privacy Jungle: On the Market for Data Protection in Social Networks[END_REF]. Uploaded pictures are assigned public, stable and unique URLs, cacheable by browsers for long durations. The user's cache is probed for all the images to determine which might be the user's. Figure 4 demonstrates the ability of our attack to consistently measure the difference in response times for cached versus un-cached Twitter profile pictures.

Our attack is easier to execute than previously described de-anonymisation attacks. As noted, history sniffing through differential colouring of visited links has long been fixed and is no longer possible. Furthermore, in contrast to the traffic analysis, our adversary only needs to set up a third-party website; there is no need for network eavesdropping. This increases the effectiveness of the attack because SNS members can be geographically distributed, i.e., not confined to a single physical network.

Mitigation. SNS like Twitter have two options to prevent the attack: first, by making profile pictures un-cacheable; second, by making URLs of profile pictures dependent on the requesting users, so that attackers cannot compile a set of probing URLs.

Monitoring search queries in real-time

The CTA scenarios covered in the existing literature are limited to targeting image objects. As we noted in Section 3, images are not the only cacheable content type. Other types include XML, JSON, CSV, and HTML. XML and JSON objects are particularly interesting because they typically carry users' personal data in the requested URLs, for example, user identifiers and search keywords. We demonstrate the threat of XML/JSON caching by constructing attacks that target information entered by the user into the address bar of a Web browser. The implications are serious because the address bars of modern browsers allow users to type in search queries and have them processed directly by a default search engine. Thus, such queries are exposed to malicious websites which can scan the browser cache. As per our tests, these attacks work on most of the commonly used browsers (Internet Explorer, Firefox, and Chrome) and across multiple search providers such as Bing, Yahoo!, Google, and Wikipedia; Ask and AOL do not show the same vulnerability.

Attack scenario. In many instances, browsers are configured to provide real-time suggestions to the users as they type in their queries or Web addresses. Continuous AJAX calls are made to the search provider during this user interaction. For instance, a call made by Chrome to Yahoo! (non-essential parameters omitted): http://ff.search.yahoo.com/gossip?output=fxjson&command=userquery.

where "userquery" refers to the query typed by the user in the Omnibox. Calls made to Google, Bing and other search engines look similar. The following sequence of AJAX calls are made when the user types in "sec15": /gossip?output=fxjson&command=s /gossip?output=fxjson&command=se /gossip?output=fxjson&command=sec /gossip?output=fxjson&command=sec1 /gossip?output=fxjson&command=sec15.

The search engine responds to each call with a JSON or XML object that is placed in the browser cache. Because this cache is shared with Web domains, a malicious website can use CTAs to extract the queries using the techniques described in Section 3. Our attack is stronger than the packet size based attacks by Chen et al. [START_REF] Chen | Side-Channel Leaks in Web Applications: A Reality Today, a Challenge Tomorrow[END_REF] in two ways: (1) their adversary model is a network eavesdropper [START_REF] Chen | Side-Channel Leaks in Web Applications: A Reality Today, a Challenge Tomorrow[END_REF], while ours is simply a third party website; (2) their attack is based on the packet sizes of responses [START_REF] Chen | Side-Channel Leaks in Web Applications: A Reality Today, a Challenge Tomorrow[END_REF], while ours is based on cache timing and enables the attacker to leak information at any later time as well. Listing 1 shows our script to carry out the probing.

Mitigation. Ideally, the cache for the address bar, search box and all other browser components should be isolated. Furthermore, one could append a user specific nonce to the requests (Section 5).

Responses by manufacturers. After our report, Bing enabled no-caching headers, effectively preventing CTAs on searches entered into the Browser address bar. Impact. The attack is critical because any attacker that can publish in the intranet zone can sniff users' activities in the OS from within the browser. Brute force and dictionary techniques can recover users' searches which might contain software names (e.g., unreleased codenames, confidential intellectual property), personal files or Web searches.

The requirement for the attacker to publish a website within an intranet is a hurdle but much lower than for traffic analysis-attacks that require access to the local network.

Mitigation. The cache for each OS component should be isolated, from any Internet or intranet Web pages.

Response by manufacturer. After our report, Bing enabled no-caching headers, effectively preventing CTAs on searches entered into the Windows SmartSearch.

Potential defences and their limits

Despite the previous research in this area, browser vendors have not yet taken actions to mitigate against CTAs. With deeper integration of Web services, it is critical that Web caches are carefully designed, by considering the timing side channel. Furthermore, with significant performance improvements of browsers in recent years [START_REF]The BIG browser benchmark[END_REF], timing attacks have become more precise. Finally, as described in Section 3, multi-threading in JavaScript makes highly scalable brute force CTAs efficient. Thus, it is necessary to re-evaluate previously proposed mitigations and implement additional ones to address these issues.

Failed mitigations

Felten et al. [START_REF] Felten | Timing attacks on web privacy[END_REF] proposed various hypothetical solutions such as disabling caches and JavaScript, and altering hit or miss timings. Unfortunately, disabling JavaScript will break most of the modern websites and disabling caching will lead to significant performance degradation for the Internet. Furthermore, altering hit or miss timings is not possible without affecting user experience and slowing Web applications. Solutions in the form of "domain tagging" [START_REF] Felten | Timing attacks on web privacy[END_REF], i.e., tagging each request with the domain that is making a request, could help with stopping attackers but poses a problem when resources need to be shared across multiple domains. That is the case for content delivery networks (CDNs), in use at over 55% of the top Alexa 1000 websites [START_REF] Datanyze | CDN market share in the Alexa top 1K[END_REF]. The same applies to the "domain tagging" method by Jackson et al. [START_REF] Jackson | Protecting browser state from web privacy attacks[END_REF].

HTTPS and private browsing don't help

HTTPS responses that are cached in the browser or by the OS are as vulnerable as HTTP responses. Caching is controlled only through the headers; thus, there is no differentiation between HTTPS and HTTP requests [START_REF] Msdn | HTTPS Caching and Internet Explorer -IEInternals[END_REF][START_REF]Browser.cache.disk cache ssl[END_REF]. Private browsing is a feature of modern browsers designed to sandbox a session. Data (history, cookies, local storage) pertaining to the private session are discarded when the session is closed. This may seem like a reasonable mitigation; however, the cache is shared between all websites, tabs, and the search-box/address bar opened within the private session. A malicious website can still leak data from any website accessed within the private session. Furthermore, it can still sniff data from the proxy cache.

Our proposed mitigations

We have demonstrated how various Web caches can be exploited to leak data using CTAs. Any counter-measure which impacts performance or requires Web scale changes cannot be expected to be implemented. Furthermore, there is no single mitigation that can fix all the attacks we have described. Issues with the "domain tagging" method can be resolved by using the recently introduced Web standard for "resource timing" API [START_REF] W3c | Resource Timing[END_REF]. By default, the cache is shared among all origins. However, for privacy sensitive resources, a list of origins can be provided in the response. These are allowed to load a resource from the cache without having requested it earlier. However, this requires changes in the standards, browsers and also Web servers.

A more pragmatic approach is to append a user or session specific nonce ('number used once') to all URLs with privacy-sensitive data. The CTAs attacker would then need to know or guess the URL in order to probe for it. This mediation does not require Web-scale changes and can be implemented with a minimal effort by developers. Most of the requests by Google and YouTube, for instance, append a nonce.

Probing detection and prevention. As an alternative defence, JavaScript engines could be augmented to detect and then prevent cache probing, thereby blocking the attack vector. Detection could be through the source code [START_REF] Acar | FPDetective: dusting the web for fingerprinters[END_REF], or through behavioural analyses. Such mitigation adopts the route of antivirus software: instead of fixing the vulnerability we hinder its exploitation. Despite its near-term effectiveness, this approach incurs long-term costs and may result in an arms' race between attackers and their targets.

6

Discussion and concluding remarks

Cyber-espionage of corporate intranets

We have demonstrated how an attacker can de-identify users even on professional social networks (Section 4.2), monitor Web search queries in real-time (Section 4.3), and trace files that users are searching for on their desktop PCs (Section 4.4). An attacker can combine these mechanisms to harvest data from corporate intranets as well. For the exploitation of OS search, the attacker has to be on the intranet (e.g., a rogue employee), but for the rest, any Internet website can deploy the attack.

The caches built into Web proxies (Fig. 1) expand the CTA surface. All major commercial proxy server software have a built-in cache to enable faster loading of frequently accessed resources across users behind the proxy. They are susceptible to the same side channel attack as the browser cache. However, such CTAs are more critical since a malicious Web page can sniff traffic from closed intranets such as hospitals and educational institutions and corporate networks. In some cases, users may not be aware that they share a proxy with others, or cannot change the proxy settings. That particularly applies to the mobile Internet. In our experiments we were able to use a malicious web page to sniff users' queries and traffic from a corporate network.

Taken together, cache attacks at the browser, operating system, and proxy level open door to targeted cyber-espionage. Confidential information can be sniffed from a corporate network. Gathered information can also be used to mount a credible social engineering attack in a second step, for instance, in combination with targeted individuals, identified over Facebook (Section 4.2).

Policy recommendations and managerial implications

Finding the balance between surveillance and national security is an essential challenge for each society that recognises its citizens' preference for privacy and self-determination. Availability of ad-hoc surveillance "of anyone by anyone", within and outside the workspace, can be easily monetised by a service and, without proper intervention, can become a common practice and an economically viable enterprise. Once such practices take root, they are hard to weed out, as was the case with super cookies [START_REF] Holter | KISSmetrics Settles ETags Tracking Class Action Lawsuit[END_REF]. Thus, one would need to act swiftly to prevent the emergence of services that allow attack at scale. At the corporate level, CIOs and system administrators need to be vigilant in guarding corporate information that can be revealed through employees' activities. This needs to go hand-in-hand with the policy recommendations and work with standardisation bodies to consider adaptations of the cache design.

Fig. 1 .

 1 Fig. 1. Interaction among different caching facilities with the user PC and Web network.

Listing 1 :

 1 function isRequestCached(URI, callback) { var timeStamp, timedOut = false; var xhr = new XMLHttpRequest(); xhr.open('GET', URI, true); xhr.onreadystatechange = function() { setTimeout(function() { callback(!timedOut); }, 2); }; xhr.timeout = 5; // milliseconds xhr.ontimeout = function() { timedOut = true; } timeStamp = getTimeStamp(); xhr.send(null); } JavaScript function snippet for timing queries.

Fig. 4 .

 4 Fig.4. Request response times in milliseconds for the same Twitter profile picture in the three standard sizes (100 repetitions). For un-cached media, response times vary but are always above response times for cached media, which are all consistently negligible.

Fig. 5 .

 5 Fig. 5. Windows search provide auto-suggest across PC settings, local and cloud documents, the Web and Windows Store

existed in

	3.1	Attack mechanics
	Attack principle. Although the same-origin policy [1] restricts cross-origin access to
	security critical APIs, such as DOM, Cookies, Local Storage, XMLHttpRequest, it al-
	lows for shared caches and cross-origin embedding of resources-a fundamental prin-
	ciple of hypermedia. For instance, if the domain A.com embeds a resource
	A.com/file.ext then the resource is cached by the browser on page load. Subsequently,
	any other origin can load A.com/file.ext and measure the loading time to infer whether
	the resource already

the cache or not. This can be further used to imply that the targeted user requested A.com/file.ext earlier.

  As discussed in Section 4.4, browser and OS components currently leak information because they share the cache with Web pages. Unlike proxy caches, even HTTPS requests are stored in browser caches, making this more critical. Segmentation is an easy yet effective fix. Each component, plugin or extension should have a separate cache so that there is no side channel leak to a malicious Web page or a malicious component.

Cache segmentation: browser and OS.

Proxy cache. To prevent CTAs on Web proxies, appropriate no-cache headers should be set on all responses with any private data (e.g., API calls, image requests, etc.). The "Cache-control: private" header can be set to prevent any public proxy caching.

Browser cache. Because of the current design of the browser cache, this is the hardest case of CTAs to fix. To begin with, we recommend that none of the security critical resources (such as Site-to-user images) are cached at all. Website developers should disable caching by setting the appropriate no-cache headers. Eliminating caching altogether is simply not practical; the Web architecture relies on caches.

Acknowledgements. The authors would like to thank Pushkar Chitnis, B. Ashok, Cedric Fournet, Sriram Rajamani and the reviewers for their helpful comments leading to significant improvements to this paper. We would also like to acknowledge the Microsoft and RSA Security teams for prompt and constructive discussions about our attacks.

Summary and Future Work

In this paper, we broadened the scope of cache timing attacks by demonstrating CTAs against banking sites, social networks, browser components, and operating systems. Our case studies show that cache timing attacks are applicable to much more critical scenarios than those previously considered. Our technique leverages fine-grained timeouts and HTML5 Web Workers to make the attacks more efficient, without contaminating the cache while probing. The robustness, effectiveness, and the non-cooperative nature of the attack increase the risk to undetectable, widespread attacks as part of the cyber espionage, ad-hoc surveillance of individuals and groups, un-consented identification and de-anonymisation. We discussed potential counter-measures and identified practical mitigations for each scenario that can be easily incorporated in the application design without requiring Web-scale changes.

Our future research will involve empirical studies of attack scenarios to evaluate both the applicability and the effectiveness of the CTAs. We plan a large-scale survey of cache implementations in operating systems across platforms (desktop, mobile, embedded), Web browsers and Web and desktop applications (e.g., mail, document authoring). Our work on systems security will be complemented by a user study to gauge reactions to the unexpected privacy invasions. We foresee outreach efforts to raise awareness amongst consumers and IT professionals.