Ahmed A Abouelfarag
email: abouelfarag@aast.edu

Walid Mohamed Aly
email: walid.ali@aast.edu

Ashraf Gamal Elbialy
email: ashraf2k@gmail.com

Performance Analysis and Tuning for Parallelization of Ant Colony Optimization by Using OpenMP

Keywords: Parallel Metaheuristic, Ant Colony Optimization, shared memory model, OpenMP, Parallel Threads

Ant colony optimization algorithm (ACO) is a soft computing metaheuristic that belongs to swarm intelligence methods. ACO has proven a well performance in solving certain NP-hard problems in polynomial time. This paper proposes the analysis, design and implementation of ACO as a parallel metaheuristics using the OpenMP framework. To improve the efficiency of ACO parallelization, different related aspects are examined, including scheduling of threads, race hazards and efficient tuning of the effective number of threads. A case study of solving the traveling salesman problem (TSP) using different configurations is presented to evaluate the performance of the proposed approach. Experimental results show a significant speedup in execution time for more than 3 times over the sequential implementation.

Introduction

Some of the real-life optimization problems cannot be tackled by exact methods which would be implemented laboriously and in a time-consuming manner. For such optimization problems, metaheuristics are used with less computational effort to find good solution from a set of large feasible solutions. Although other algorithms may give the exact solution to some problems, metaheuristics provide a kind of nearoptimal solution for a wide range of NP-hard problems [START_REF] Alba | Parallel Metaheuristics: A New Class of Algorithms[END_REF]. Since introduced in 1992 by Marco Dorigo [START_REF] Dorigo | Optimization, Learning and Natural Algorithms[END_REF], ACO algorithms have been applied to many combinatorial optimization problems, ranging from Scheduling Problems [START_REF] Chen | Ant Colony Optimization Approach to Grid Workflow Scheduling Problem with Various QoS Requirements[END_REF] to routing vehicles [START_REF] Donati | Time dependent vehicle routing problem with a multi ant colony system[END_REF] and a lot of derived methods have been adapted to dynamic problems in real variables, multi-targets and parallel implementations.

ACO was proposed as a solution when suffering from limited computation capacity and incomplete information [START_REF] Chen | Ant Colony Optimization Approach to Grid Workflow Scheduling Problem with Various QoS Requirements[END_REF]. ACO metaheuristic proved a significant perfor-mance improvement compared with other metaheuristic techniques in solving many NP-hard problems such as solving the traveling salesman problem [START_REF] Dumitrescu | Combinations of local search and exact algorithms[END_REF].

The multicore computation power encouraged the modification of the standard metaheuristic approaches to be applied in a parallel form.

In this paper, OpenMP is used on CPU with multi-cores to measure the performance speedup. To make the data accessible and shared for all parallel threads in global address space, a shared memory model is implemented in C++. OpenMP is implemented with its parallel regions, directives to control "for" loops. Scheduling clause for fine tuning. For eliminating race condition, omp critical sections have been also implemented.

The importance of TSP problem as a test case comes from its history of applications with many metaheuristics. TSP is also easy for mapping with real life problems.

The speedup gain in parallelization of a typical sequential TSP with ACO depends mainly on the proper analysis of where parallel regions should be placed in the algorithm. Theoretically, Amdahl's law [START_REF] Amdahl | Validity of the single processor approach to achieving large Scale Computing capabilities[END_REF] limits the expected speedup achieved to an algorithm by a relation between parts that could be parallel to the parts remain serial. One of the targets of the experiment is to assign the optimal number of parallel threads and tuning them dynamically with the available number of CPU cores to get effective speedup.

This paper is organized as the following: in Section 2, the related work to ACO and the research efforts towards its parallelization are presented. Section 3 presents the sequential ACO algorithm mapped to TSP. In section 4, the proposed ACO parallelization using OpenMP is presented where its sub-sections show the analysis of different elements of OpenMP and its effects on performance. In section 5, results and performance evaluation are investigated using the TSP problem as an implementation of parallel ACO algorithm. Finally, section 6 concludes the research and suggests the future work.

Related Work

Many strategies have been followed to implement ACO algorithm on different parallel platforms. In [START_REF] Arnautovic | Parallelization of the ant colony optimization for the shortest path problem using OpenMP and CUDA (MIPRO)[END_REF], Compute Unified Device Architecture (CUDA) is used to get the parallel throughput when executing more concurrent threads over GPUs. Results showed faster execution time with CUDA than OpenMP, but the main disadvantage of CUDA computing power is its dependence on GPU memory capacity related to problem size.

Marco Dorigo and Krzysztof Socha [START_REF] Dorigo | An Introduction to Ant Colony Optimization[END_REF] addressed that the central component of ACO is the pheromone model. Based on the underlying model of the problem, parallelization of this component is the master point to the parallel ACO.

Bullnheimer et al. [START_REF] Bullnheimer | Parallelization strategies for the ant system[END_REF], introduced the parallel execution of the ants construction phase in a single colony. This research target was decreasing computations time by distributing ants to computing elements. They suggested two strategies for implementing ACO for parallelization: the synchronous parallel algorithm and the partially asynchronous parallel algorithm. Through their experiment, they used TSP and evalu-ated the speedup and efficiency. In the synchronous parallel algorithm, the speedup is poor for the small problem size and resulting to "slowdown" the efficiency close to zero. While in large problem size, the speedup is improved by increasing the number of workers (slaves). Communication and idle time have a great effect on limiting the overall performance. The authors conclude that the second approach, partially asynchronous parallel algorithm, implemented the concept of parallelism with better speedup and efficiency. The disadvantage of this model was the communication overhead for the master ant waiting for the workers to finish their task.

Stützle [START_REF] Stützle | Parallelisation strategies for ant colony optimization[END_REF], introduced the execution of multiple ant colonies, where the ant colonies are distributed to processors in order to increase the speed of computations and to improve solution quality by introducing cooperation between colonies. This method would be implemented through distributed memory model which would require a huge communication that caused high overhead affecting the overall performance.

Xiong Jie et al. [START_REF] Xiong | A New Parallel Ant Colony Optimization Algorithm Based On Message Passing Interface[END_REF] used message passing interface MPI with C language to present a new parallel ACO interacting multi ant colonies. The main drawback of this approach is the coarse-granularity where the master node have to wait for all slave nodes to finish their work and then updates with the new low cost solution.

This paper proposes a solution with OpenMP to get the performance gain of parallel regions. These parallel regions provide parallelizing to the ACO algorithm by controlling the time-consuming loops, avoiding race hazards and maintain load balance.

3

The ACO Algorithm

In ACO as a metaheuristic, cooperation is a key design component of ACO algorithms [START_REF] Dorigo | Ant colony optimization" A Bradford Book[END_REF]. The artificial cooperating ants build a solution for a combinatorial optimization problem by traversing a fully connected graph. Solution is built in a constructive method. The solution component is denoted by cij , c is representing a set of all possible solution components. When combining c components with graph vertices V or with set of edges E the result would be the graph GC(V,E).

ACO Solution Steps

ACO algorithm consists of three main procedures which are:  ConstructAntsSolutions(edge selection) phase: the ants traversed through adjacent neighbor nodes of the graph is made by a stochastic local decision according to two main factors, pheromone trails and heuristic information. The solution construction phase starts with a partial solution s p =ϕ. From the adjacent neighbors a feasible solution component N(s p ) ⊆ C is added to the partial solution. The partial built solution made by an ant is evaluated for the purpose of using it later in the UpdatePheromones procedure. Dorigo [START_REF] Dorigo | Ant colony optimization" A Bradford Book[END_REF] formed an equation for the probability of selecting solution component:

() . ( | ) , ( ) . p il ij p p ij ij ij ij N ij p N cs c s c s              ( 1
)
Where τij is the deposited pheromone value in the transition from state i to state j, and ηij is the heuristic value between i, j. Both τij , ηij associated with the component cij. Where α and β are two parameters which controls the parameters of τij and ηij respectively, where α ≥ 0, β ≥ 1

 LocalSearch phase: This step is started after solution construction phase and before pheromone update. The result of this step are locally optimized solutions. This is required -as a centralized action -to improve the solution construction phase.  UpdatePheromones phase: is the most important phase where a procedure of pheromone level is increased or decreased. After all ants completed the solution, the following rule controls the pheromone update:

(1 )

k ij ij ij k          ( 2
)
Where ρ is pheromone evaporation coefficient and

k ij 
 is the amount of phero- mone released by k-th ants on the trip finished between i, j

k Q if ant k traverse edge i j k ij else L    ( , ) 0 {
Where Q is a constant, Lk is tour length traversed by the ant k. Continues increase in pheromone levels in each iteration would produce an attractive path to the following iterations. This leads to the trap of local optima ants discarding the exploration of other connections. To explore new areas, pheromone evaporation rate is activated to participate in lowering pheromone levels in each tour.

3.2

The ACO Algorithm for TSP

As the exemplary task, Traveling Salesman Problem TSP is considered to verify the efficiency of the proposed parallel approach as well as some related aspects like the scheduling of threads, the race hazards and tuning of the effective number of threads.

In the algorithm of TSP, the weighted graph G = (N, A) where N is the number of nodes representing cities. The connection between cities (i,j) ϵ A and dij is the distance between (i,j). The τij representing the desirability of visiting city j directly after visiting city i according to pheromone trails, ηij depicts the heuristic information where ηij =1/ dij and there will be a matrix of τij which includes pheromone trails. The value of pheromone at initial state for TSP is:

  0/ ij min mC   ( 4
)
Where m is the number of ants, Cmin is the minimum distance between any i, j. When ants planning to construct its path ant k determines the probability P of visiting the next city according to formula in (1).

The j is the city not visited yet by ant k, both α and β are two parameters which control the relative importance of pheromone (τij) against heuristic information (ηij =1/dij), tabuk is the list of already visited cities by k-th ants. The update pheromone process starts after all ants have finished their tours construction. At first, pheromone values are lowered by a constant factor for all connections between cities. Then, pheromone levels are increased only for the visited connections by ants, pheromone evaporation determined by:

(1 )

ij ij     (5)
Consider ρ as pheromone evaporation rate, where 0< ρ ≤1. After number of iterations, the ants release pheromone in all visited connections during their tour formula in (2) Where ()

k ij t  
denotes the amount of pheromone deposited by ant k on the trip finished between nodes i and j defined as in formula (3).

Proposed ACO Parallelization by Using OpenMP

ACO is a potential candidate for parallelization for different reasons, including:  The individual independent behavior of ants.  The large number of iterations required in updating pheromone trails.  The computations needed for the single ant to construct a solution in the graph.

Parallel ACO could be implemented with two different strategies [START_REF] Xue-Dong | The basic principle and application of ant colony optimization algorithm[END_REF]:  Coarse-grained: single CPU is being used by many ants or even the whole colony with rarely information exchange between CPUs  Fine-grained: few numbers of ants are to be assigned with each core of CPU with more communication and information exchange between them. The main difference between previous two approaches is the amount of information exchange between the CPUs. Fine-grain model needs more communication which causes an overhead consuming most of the execution time. Coarse-grain parallelization model is most suitable for multiple colonies of ACO implementation [START_REF] Dorigo | Ant colony system: a cooperative learning approach to the traveling salesman problem[END_REF]. Finegrain parallelization strategy has been adopted in this paper to study the behavior of multithreading with relation to the multicores available in CPU with a single colony.

An improvement in ACO algorithm could be achieved mainly by using multithread programming with multi-core processors. This section introduces an implementation for parallel ACO using OpenMP platform. A shared memory model has been chosen to get the benefit of creating a common space sharing pheromone matrix without the overhead of communication, especially when applying both "Con-structAntSolutions" and "UpdatePheromones" processes. OpenMP is implemented to reduce the execution time and not altering the ACO algorithm with major change.

The main effort here is to analyze and select the places which consume most execution time in the sequential ACO and to overcome the problem of communication overhead by using the OpenMP directives. Larger and in-place OpenMP parallel regions are used, because fragmented parallel regions would increase the overhead of creating and terminating threads.

4.1

Tuning Optimal Number of Threads.

One of the major questions here when implementing parallel regions is: what is the optimal number of threads to execute through for loops? To answer this question, a hypothesis have been adopted. The optimal number of threads would depend on both parallel implementation of ACO and the number of multi-cores available in the CPU. This is according to two factors.  Amdahl's law8], which means that adding more threads would be neglected with no significant speedup because of sequential part.  The number of threads can be chosen to be more than the number of cores. This is the case when a thread is in waiting/blocking condition. Hyperthreading availability in modern CPUs provides management for many threads per core.

Tuning Parallel Regions.

The pseudocode of ACO is shown in Fig. 1, which simplifies the three main components of the algorithm. The "ConstructAntSolutions" is the function of asynchronous concurrent ants while visiting neighbor nodes of the graph. Ants progressively build their path towards the optimal solution with the help of "UpdatePheromones" function. In the function of "UpdatePheromones" the pheromone trails are updated with increased levels of pheromones by releasing more pheromone on connections between nodes, or the pheromone decreased by the effect of evaporation. Increasing pheromone levels means increasing the probability of successive future ants in their way to find the shortest path allowing only specific ants to release pheromone.

procedure ACOMetaheuristic Begin Set parameters, initialize pheromone trails while (termination condition not met) do ConstructAntSolutions ApplyLocalSearch % optional UpdatePheromones end while end

Fig. 1. The pseudocode of ACO

The main experimental objective here is to apply a pragma omp parallel region to the main parts of ACO, first on ConstructAntSolutions only and then measure the performance. After that, the parallel region will be applied to updatePheromone procedure, where a parallel "for" applied with "n" number of threads. At the end of each parallel region there will be an implicit automatic barrier, its mission is to synchronize with the main thread before starting new parallel region.

4.3

Tuning OpenMP Scheduling Clause.

Three types of OpenMP schedule clause could be experimented to control the granularity of thread execution: static (which is the default), dynamic, and guided schedule. The default scheduling used in parallel for is static, which distributes the work and iterations between threads. This is not the case of different jobs assigned to different ants. The proposed solution adds the schedule dynamic clause to the "parallel for" loops to give a full control for the distribution of iterations to the available threads. The iteration granularity is determined by the chunk size. The main benefit of dynamic scheduling is its flexibility in assigning more chunks to threads that can finish their chunks earlier. The rule is, the fastest thread shouldn't wait for the slowest.

Eliminating Race Condition Hazards

The race condition would occur when many threads update the same memory location at the same time. ACO algorithm may suffer from this problem, especially when two or more ants are trying to update the pheromone matrix at the same time. To avoid data race condition in the process of increasing/decreasing pheromone levels, critical sections are applied. However, in our proposed parallelization, each thread will be responsible for updating pheromone level of each edge. Thus, the value of pheromone level update is the sole responsibility of a single thread. Accordingly, race hazards can be eliminated.

Results and Performance Analysis

In this paper, Travel Salesman Problem (TSP) NP-hard problem has been chosen as a well-known application of the generic ACO algorithm. In this paper, TSP parameters were initially set, and OpenMP was applied as a parallelization API. After that, results were gathered from the experiment. Finally, the performance of ACO algorithm with OpenMP was finally analyzed.

ACO Parallelization Environment.

In the conducted experiment of this paper, OpenMP 4.0 and Visual Studio Ultimate 2013, ACO algorithm was implemented in C++. Computer configuration is Intel® Core™ i5-460M 2.53GHz, CPU-L3 cache 3MB, 4GB RAM.

The parallel regions of OpenMP with number of threads n=2, 4, 8, 16, 32, 64 are applied, utilizing 1000 ants. Different sizes for TSP problem with 40, 80, 130 cities are used to test the scalability of the parallelization. The test and the analysis would measure the speedup to gauge the parallelization impact on execution time and efficiency. The performance is measured by using speedup which shows the performance to determine the optimal solution in a specific computing time:

/ sp speedup tt  (6)
In equation [START_REF] Xue-Dong | The basic principle and application of ant colony optimization algorithm[END_REF], ts is the time required to solve the problem with the sequential version of code on a specific computer, tp is the time to solve the same problem with the parallel version of code using p threads on the same computer. And the efficiency of the parallel implementation is calculated through the equation: / efficiency speedup P 

The strategy of implementation described before has been put under experiment by starting from an existing sequential implementation. Then, the appropriate OpenMP directives were added, the necessary changes were made as discussed before.

To achieve accurate results representing real execution time, code running was repeated ten times for every change in thread numbers. In this experiment, Sequential code was applied first to measure the difference between parallel and sequential versions of code. Tables 1,2, 3 show the results of average execution time, speedup and efficiency when default schedule static was initially applied, then the application of dynamic schedule with n number of threads was compared showing the difference. By using k=1000 as number of ants, the experiment was sequentially executed with problem size of 40 cities of the ACO and the execution time was marked. Parallelization started with 2, 4, 8, 16, 32, and 64 threads respectively. Then, the same experiment was repeated with different problem sizes 80 and 130 cities. The speedup and efficiency are measured by equations ( 6) and [START_REF] Dorigo | Ant colony system: a cooperative learning approach to the traveling salesman problem[END_REF]. Analyzing the results of execution times in table 2 has proved a better performance by using 4 and 8 threads, then no significant speedup was noticed on adding more threads. The colony size increased to 80 cities. A better performance took place with a leap in execution time especially after applying dynamic scheduling clause. The same could be addressed by increasing the TSP problem size to 130 cities as shown in Table 3. A fine tuning was done using schedule dynamic clause which caused a noticed performance speedup. This is due to the dynamically generated chunks at runtime which control the thread execution over iterations. After combining the results from the three tables 1, 2, and 3 in Fig. 2, a relative speedup for parallelization over sequential implementation was observed especially on increasing the TSP problem size 40, 80 and then 130 cities. As shown in table 4, parallel regions of OpenMP wraps the most time consuming parts of ACO algorithm. When execution time was measured for each region, Updatepheromone was found to be the most time-consuming part. A speedup was achieved after applying OpenMP parallel. This is clearly illustrated in Fig. 3 which shows a significant time-consuming UpdatePheromone function and AntSolutionConstruction is the second most time-consuming part. They both gain significant speedup after applying parallel regions of OpenMP. As the main goal is to provide better performance through parallelism, the experiments in this research would investigate the optimal number of threads needed. For this purpose, a tool of thread visualizing and monitoring the interaction and relation between threads and cores has been used. One selected tool is Microsoft concurrency visualizer which is a plug-in tool for Visual studio 2013. Different numbers of threads were implemented in each run and results have been collected and analyzed in the results section.

In the current experiment, 1, 4, and 8 threads have been selected to be analyzed by Concurrency Visualizer on a machine with 4 logical cores for the following reasons:  Finding the optimal number of threads related to the available number of cores.  Visualizing and analysis of concurrently executing 4 threads that's equal to the number of logical cores.  Visualizing and analysis of concurrently executing 8 threads that's more than the number of cores.  Visualizing and analysis of the behavior of multithreads and how they execute, block, and synchronize.

Executing the ACO with a bigger number of threads than the number of cores, an overhead of context switching, synchronization, and preemption of the threads is detected. In the meanwhile, OpenMP gives a better utilization of the multicore environment. Fig. 5, shows a detailed view of 4 and 8 threads on 2 cores CPU with hyperthreading which are logically equivalent to 4 cores. When the number of threads is equal to the number of cores, threads are distributed among the available cores. The advantage of this is less synchronization and preemption time. Most of this saved time is assigned to execution causing the parallel threads to achieve better speedup. Whereas, if the number of threads largely exceeds the number of available cores, an overhead and time wasting is detected. This is because of thread blocking, synchronization, and context switching. This experiment shows the fact that the optimal number of threads should not exceed the available number of cores. Consequently, if the possibility of thread blocking does not exist, the number of threads should be optimized according to the available number of cores, as each thread will utilize each CPU core. In this research, parallel implementation of ACO using OpenMP API directives effectively solves the common TSP problem. Results were evaluated, and comparison between sequential and parallel multithread were also analyzed. OpenMP parallel regions achieved a speedup more than 3X of sequential execution. The optimal number of threads was found to be equal to the number of processors available. With TSP sizes of 40, 80, and 130 cities, better speedup was detected with a larger number of cities. Moreover, tuning was added to the implementation of parallel ACO using OpenMP with different schedules clauses. Dynamic schedule was found to achieve better performance with average speedup 8-25% than default schedule clause especially on increasing the number of cities. This paper shows an upper border of speedup related to the available number of cores.

The future work would be oriented towards using this kind of parallel implementation using OpenMP for different newly metaheuristics such as Cuckoo search (CS) and to compare results to parallel ACO and measures which one positively affected more by the parallelization of OpenMP platform..

Fig. 2 .

 2 Fig. 2. The speedup with n number of threads applied on different ant colony sizes

Fig. 3 .Fig. 4 .

 34 Fig. 3. Execution time of Parallel regions against different n threads with same problem size

Fig. 5 .

 5 Fig. 5. Thread distribution when executing 4 and 8 threads/2 cores CPU with hyper-threading

Table 1 .

 1 Ant colony size, 40 cities 1000 ants

	Number of threads	Default Schedule Exec. time(sec)	Dynamic Schedule Execu-tion time(sec)	Speedup (sequen-tial to dynamic)	Efficiency
	Sequential	1.5855	1.5855	-	-
	2	1.2543	1.1264	1.41	0.70
	4	1.0347	0.9427	1.68	0.42
	8	1.0494	0.9338	1.70	0.21
	16	1.0764	0.9430	1.68	0.11
	32	1.0603	0.9454	1.68	0.05
	64	1.0761	0.9650	1.64	0.02

Table 2 .

 2 Ant colony size, 80 cities, 1000 ants

	Number of threads Dynamic Exec. time(sec)	speedup	efficiency
	Sequential	7.0755	-	-
	2	4.0492	1.75	0.87
	4	2.7932	2.53	0.63
	8	2.7204	2.60	0.33
	16	2.7889	2.54	0.16
	32	2.8113	2.52	0.08
	64	2.8151	2.51	0.04

Table 3 .

 3 Ant colony size, 130 cities 1000 ants

	Number of threads	Default Schedule Execution time(sec)	Dynamic Schedule Execution time(sec)	speedup (sequential to dynamic)	efficiency
	Sequential	25.9013	25.9013	-	-
	2	17.764	10.6557	2.43	1.22
	4	9.57293	7.3100	3.54	0.89
	8	8.1691	7.2090	3.59	0.45
	16	7.90743	7.2510	3.57	0.22
	32	7.79117	7.3096	3.54	0.11
	64	7.80114	7.3259	3.54	0.06

Table 4 .

 4 Execution time of Parallel regions against different n threads

	number of threads	initialize Phero-moneTrail	AntSolution Con-struction	update Pheromone	Overall execution time
	1	0.000135	2.414022	9.531944	12.29551
	2	0.000078	1.298681	4.116056	5.677514
	4	0.000072	0.836327	3.056812	4.125318
	8	0.000098	0.807538	3.000157	4.054615
	16		0.828095	3.060481	4.188573
	32	0.000139	0.832196	3.0479	4.137231
	64	0.000217	0.869248	3.024268	4.185221


Michal Piorek
email: michal.piorek@pwr.edu.pl

Chaotic properties of gait kinematic data

Keywords: deterministic chaos, nonlinear time series analysis, quaternions, human motion analysis, human gait data

Time delay reconstruction for real systems is a widely explored area of nonlinear time series analysis. However, the majority of related work relates only to univariate time series, while multivariate time series data are common too. One such example is human gait kinematic data. The main goal of this article is to present a method of nonlinear analysis for kinematic time series. This nonlinear analysis is designed for detection of chaotic behavior. The presented approach also allows for the largest Lyapunov's exponent estimation for kinematic time series. This factor helps in judging the stability of the examined system and its chaotic properties.

Introduction

Multivariate time series data are common in real systems. Many of those systems are results of the evolution of nonlinear systems dynamics. To assess the chaotic origin of time series, time delay reconstruction of a phase space is required. This step provides a view of the dynamics of the underlying system and allows the estimation of other properties of the investigated system (e.g. Lyapunov's largest exponent or one of the fractal dimensions of the reconstructed attractor). Based on the estimations of several parameters characterizing nonlinear processes, a decision about chaotic origin of time series may be taken.

According to the embedding theorem ( [START_REF] Takens | Detecting strange attractors in turbulence[END_REF]), for recovering dynamics only a univariate time series is needed, but often measurements of more than one quantityes related to the same dynamical system are available. One such case is the gait kinematic data for patients suffering from various diseases affecting walking ability.

In related work, there is a large number of applications of embedding theorem including univariate time series embedding ( [START_REF] Sauer | Embedology[END_REF], [START_REF] Stark | Delay Embeddings for Forced Systems. I. Deterministic Forcing[END_REF], [START_REF] Whitney | Differentiable manifolds[END_REF]), multivariate time series embedding ( [START_REF] Cao | Dynamics from multivariate time series[END_REF], [START_REF] Garcia | Multivariate phase space reconstruction by nearest neighbor embedding with different time delays[END_REF], [START_REF] Kocak | Nonlinear prediction of near-surface temperature via univariate and multivariate time series embedding[END_REF]), modelling ( [START_REF] Abarbanel | Analysis of observed chaotic data[END_REF], [START_REF] Fraser | Independent coordinates for strange attractors from mutual information[END_REF], [START_REF] Grassberger | Measuring the strangeness of strange attractors[END_REF]), chaos controll ( [START_REF] Andrievskii | Control of chaos: Methods and applications[END_REF], [START_REF] Cordoba | Periodical forcing for the control of chaos in a chemical reaction[END_REF], [START_REF] Parmananda | Controlling turbulence in coupled map lattice systems using feedback techniques[END_REF]), noise reduction ( [START_REF] Casdagli | State space reconstruction in the presence of noise[END_REF], [START_REF] Grassberger | On noise reduction methods for chaotic data[END_REF], [START_REF] Eric | Noise reduction in chaotic timeseries data: a survey of common methods[END_REF]) and signal classification ( [START_REF] Sugihara | Nonlinear forecasting for the classification of natural time series[END_REF]).

The method presented in this paper is designed for a nonlinear analysis procedure for gait kinematics time series (Euler Angles or Quaternion) aimed at computing the Largest Lyapunov Exponent for reconstructed dynamics for the purpose of identifying of deterministic chaos in gait kinematic data.

The presented method does not assume that investigated system is a deterministic chaotic system in the first place. This empirical approach is aimed to investigate the origin of the examined time series.

In this approach the Largest Lyapunov Exponent is also treated as a measure of human locomotion stability. In this case stability is defined as the sensitivity of a dynamic system to perturbations. This is a very popular factor in biomedical applications ( [START_REF] Dingwell | Kinematic variability and local dynamic stability of upper body motions when walking at different speeds[END_REF], [START_REF] Jb Dingwell | Local dynamic stability versus kinematic variability of continuous overground and treadmill walking[END_REF]).

The second section describes gait kinematic data time series -a subject of further investigations. It also includes information about conversion to quaternion's angle time series which allows for further efficient computations. The third section includes information about methods used in a nonlinear analysis procedure. The fourth section presents the numerical results. The conclusions are presented in section five.

Gait Kinematics Data Time series

There are three kinds of parameterisation of orientation space. Euler angles are good for human understanding of angular position. Matrices are able to do the calculations. However, quaternions are computationally efficient whilst also avoiding the singularities of Euler angles ( [START_REF] Jack | Quaternions and rotation sequences[END_REF]).

Quaternion parameterisation describes human motion which requires significant amounts of information about rotational displacement of selected segments. The method presented in this paper is designed for data captured from physical systems. We assumed that, to make a proper estimate of finite-time Lyapunov exponents experimentally, it is necessary to collect time series data captured from a large number of consecutive strides of gait ( [START_REF] Jablonski | Quaternion dynamic time warping[END_REF]).

The data are recorded as time series formed by Euler Angles. It is the most common parameterisation especially for biomedical applications.

s(n) = [β 1 (t 0 + n∆t), β 2 (t 0 + n∆t), β 3 (t 0 + n∆t)] (1)
where s(n) is a n-th sample of Euler angles measured in interval time ∆t from initial time t 0 and β 1 , β 2 , β 3 are Euler angles in a X-Y-Z sequence. Axes X, Y and Z are defined as unit vectors:

X = (1, 0, 0), Y = (0, 1, 0), Z = (0, 0, 1) (2)
Due to the fact that an Euler Angles time series is a multivariate time series, the following procedure was used to obtain better efficiency of computations.

Based on the assumption that axes X, Y and Z are unit vectors, rotation coding in Euler's Angles and in quaternions are identical. We can define quaternions for each base rotation in a Euler sequence:

q x (β 1 ) = cos( β1 2 ) + ----------→ (sin( β 1 2
), 0, 0)

q y (β 2 ) = cos( β2 2 ) + ----------→ (0, sin( β 2 2 ), 0) q z (β 3 ) = cos( β3 2 ) + ----------→ (0, 0, sin( β 3 2 )) (3)
Finally a quaternion equivalent to Euler angles representation can be calculated from three consecutive rotations described by the following quaternions:

q xyz (β 1 , β 2 , β 3 ) = q x (β 1 )q y (β 2 )q z (β 3 ) = (cos( β1 2 )cos( β2 2 )cos( β3 2 ) -sin( β1 2 )sin( β2 2 )sin( β3 2 ))+ i(sin( β1 2 )cos( β2 2 )cos( β3 2 ) -cos( β1 2 )sin( β2 2 )sin( β3 2 ))+ j(cos( β1 2 )sin( β2 2 )cos( β3 2 ) -sin( β1 2 )cos( β2 2 )sin( β3 2 ))+ k(cos( β1 2 )cos( β2 2 )sin( β3 2 ) -sin( β1 2 )sin( β2 2 )cos( β3 2 )) (4)
Quaternion's time series is formed by conversion of each value of a Euler's angles time series to unit quaternion

q(n) = q xyz (s(n)) = q xyz (β 1 (t 0 + n∆t), β 2 (t 0 + n∆t), β 3 (t 0 + n∆t)) (5)
Based on the assumption that there is greater variability in the quaternion's angle than its axis, nonlinear analysis directed at identifying the presence of deterministic chaos and local stability investigation is performed on the time series formed by angles of quaternion q(n)

α(n) = 2arccos(real(q(t 0 + n∆t))) (6)
3 Nonlinear analysis procedure for quaternion angle time series

The nonlinear analysis procedure consists of two steps: time delay reconstruction and the largest Lyapunov exponent estimation.

Time delay reconstruction

According to the Takens embedding theorem ( [START_REF] Takens | Detecting strange attractors in turbulence[END_REF]), its possible to reconstruct the state trajectory from a single time series using the algorithm below:

y(n) = [s(n), s(n + T ), . . . , s(n + (d -1))T ], ( 7
)
where T is a time delay and d is an embedding dimension, which estimates a real dimension of the observed system. The main point of the state space reconstruction method is T and d estimation. To estimate time delay T , the average mutual information I has been used, while for the embedding dimension the false nearest neighbor method ( [START_REF] Abarbanel | Analysis of observed chaotic data[END_REF]). The mutual information approach is based on information theory and transformation of linear autocorrelation to non-linear systems. More precisely, this method consists of 2-dimensional adaptive histogram ( [START_REF] Fraser | Independent coordinates for strange attractors from mutual information[END_REF]).

Let's assume that there are two nonlinear systems: A and B. The outputs of these systems are denoted as a and b, while the values of these outputs are represented by a i and b k . The mutual information factor describes how many bits of b k could be predicted where a i is known.

I AB (a i , b k ) = log 2 P AB (a i , b k ) P A (a i )P B (b k ) , (8)
where P A (a i ) is the probability that a = a The average mutual information factor can be described by:

I AB (T ) = ai,b k P AB (a i , b k )I AB (a i , b k ). (9)
In order to use this method to assess the correlation between different samples in the same time series, the Average mutual information factor is finally described by the equation:

I(T ) = N n=1 P (S(n), S(n + T )) log 2 P (S(n),S(n+T )) P (S(n))P (S(n+T )) . (10)
Fraser and Swinney ( [START_REF] Fraser | Independent coordinates for strange attractors from mutual information[END_REF]) propose that T m where the first minimum of I(T ) occurs as a useful selection of time lag T d . This selection guarantees that the measurements are somewhat independent, but not statistically independent. In case of absence of the average mutual information clear minimum, this criterion needs to be replaced by choosing T d as the time for which the average mutual information reaches four-fifths of its initial value:

I(T d ) I(0) ≈ 4 5 . (11)
The false nearest neighbours method is based on determining an acceptable minimum embedding dimension by looking at the behaviour of near neighbours under changes in the embedding dimension from d to d + 1. The most important assumption is that all points in the attractor that are close in ℜ m should be also close in ℜ m+1 . The false nearest neighbour is a point that appears to be a nearest neighbor because the embedding space is too small. When the number of false nearest neighbors arising through projection is zero in dimension d E , the attractor has been unfolded in this dimension ( [START_REF] Matthew B Kennel | Determining embedding dimension for phase-space reconstruction using a geometrical construction[END_REF]).

Assume that the dimension of space is d. The r-th nearest neighbor of y(n) is denoted by y r (n). The distance between point y(n) and it's r-th nearest neighbor is a square of the Euclidean distance.

R 2 d (n, r) = d-1 k=0 [x(n + kT ) -x r (n + kT )] 2 (12)
In going from dimension d to d + 1 by time delay embedding new coordinate x(n + T d) is added onto each delayed vectors y(n). The distance between points before and after adding new coordinates is now compared. A point is designated as a false neighbour when increase of distance is too large and the criteria below are fulfilled.

R 2 d+1 (n, r) -R 2 d (n, r) R 2 d (n, r) 1 2 = x(n + T d) -x r (n + T d) R d (n, r) > R T ol ( 13
)
where R T ol is some threshold. Authors of the method ( [START_REF] Matthew B Kennel | Determining embedding dimension for phase-space reconstruction using a geometrical construction[END_REF]), in numerical investigations, proved that for R T ol ≥ 10 the false nearest neighbors are clearly identified.

An acceptable minimum embedding dimension is chosen by looking at the percentage of false nearest neighbors during the addition of d + 1 components to the delayed vectors. When the percentage of false nearest neighbors drops to zero, a proper embedding dimension may be obtained.

The largest Lyapunov's exponent

Lyapunov's exponents examine the action of the dynamics defining the evolution of trajectories. The largest Lyapunov exponent describes the mean divergence between neighboring trajectories in the phase space by the following formula

d(t) = De λ1t ( 14
)
where D is the initial separation between neighboring points and λ 1 is the largest Lyapunov exponent. There are a few algorithms designed for the Largest Lyapunov's exponent estimation ( [START_REF] Wolf | Determining lyapunov exponents from a time series[END_REF], [START_REF] Colins | A practical method for calculating largest lyapunov exponents from small data sets[END_REF] and [START_REF] Kantz | A robust method to estimate the maximal lyapunov exponent of a time series[END_REF]). In this investigation Rosenstein's algorithm was used. The first stage of the Rosenstein algorithm is time delay reconstruction. After reconstruction, for each point on the trajectory, the nearest neighbor x ĵ is found. This point minimizes the distance to the particular reference point, x j as described below

d j (0) ≈ min x ĵ x j -x ĵ (15)
where d j (0) is the initial distance from the j-th point to its nearest neighbor, and ... is the Euclidean norm.

From the definition of λ 1 in eq. ( 14) authors ( [START_REF] Colins | A practical method for calculating largest lyapunov exponents from small data sets[END_REF]) assumed the j-th pair of nearest neighbors diverge approximately at a rate given by the largest Lyapunov exponent.

d j (i) ≈ D j e λ1(i∆t) (16)
where D j is the initial separation. We can take the logarithm of both sides eq. ( 17)

ln(d j (i)) ≈ ln(D j ) + λ 1 (i∆t) (17)
Eq. ( 17) represents a set of approximately parallel lines (for j = 1,2,...,M), each with a slope roughly proportional to λ 1 . The largest Lyapunov exponent is calculated then by linear regression

y(i) = 1 ∆t ln(d j (i)) (18)
where ... denotes the average over all values of j.

4 Numerical results The experiment involves the analysis of gait sequences which were recorded in the Human Motion Laboratory (HML) of the Polish-Japanese Institute of Information Technology by means of the Vicon Motion Kinematics Acquisition and Analysis System ( [START_REF] Kwolek | Realtime multi-view human motion tracking using 3d model and latency tolerant parallel particle swarm optimization[END_REF], [START_REF] Josiński | Quantifying chaotic behavior in treadmill walking[END_REF] , [START_REF] Jab | Application of quaternion scale space approach for motion processing[END_REF], [START_REF] Filipowicz | A generic approach to design and querying of multi-purpose human motion database[END_REF]).

Gait sequences were recorded in Euler angles. Six kinds of time series were recorded -movements of femurs, tibias and feet (left and right). The Experiment's aim was the investigation of local (associated with body parts) chaotic behaviour occurring in a human's gait. There were six investigations associated with movement of all the mentioned parts of the body's skeleton.

Conclusion

In this article, six time series captured from a large number of consecutive strides of gait were examined. Measurements came from three parts of the body: femur, foot and tibia. For each time series time delay reconstruction and largest Lyapunov's exponent estimation has been carried out. Values of all of the computed parameters for all examined time series are gathered in table 1. Time delay embedding for time series has already been widely explored by various contributors. However, most of the work in the published literature concerns only scalar time series. In this paper the method for multivariate kinematic's time series is presented. The results are promising for practical applications in human gait analysis.

Analyzing time delays estimated for these time series, it can be stated that proper time delay is different for each time series. On the other hand all of the values are in the range [15; 33]. Embedding dimension values are from the range [4; 7]. However the most frequent values are 4 and 5. It is probable that the embedding dimension value for left tibia is a numerical error. One factor to consider is the averaging time delay and embedding dimension values in further investigations.

Most of the largest Lyapunov's exponents calculated values are positive. Due to this fact human gait kinematics data exhibit the properties of chaotic behavior. It could be also stated that during human locomotion, all mentioned body parts are highly sensitive to initial conditions.

  i and P B (b k ) is the probability that b = b k and P AB (a i , b k ) is the joint probability that a = a i and b = b k .

Fig. 1 .

 1 Fig. 1. Stages of the nonlinear analysis procedure: mutual information, percentage of false nearest neighbors, logarithmic divergence reconstructed attractor

Fig. 1

 1 Fig. 1 illustrates results of successive stages of the nonlinear analysis procedure for the left femur: a) mutual information, b) percentage of false nearest neighbors, c) divergence, d) reconstructed attractor. Based on the above figure one can see that from the mutual information chart time delay embedding T = 21 could be obtained when the first minimum of I(T ) occurs. From the false nearest neighbours chart embedding dimension d = 4 is obtained when the percentage of nearest neighbours drops to zero. From the linear regression of the logarithmic divergence the largest Lyapunov exponent is estimated λ 1 = 0.3157.

Table 1

 1 includes results of the nonlinear analysis procedure for all mentioned body parts. For each of them the time delay T , embedding dimension d and the largest Lyapunov exponent have been estimated. For right foot and left tibia negative LLEs values have been observed. It could be caused by too large value of the estimated embedding dimension. However, negative value of the largest Lyapunov exponent does not undermine the possible chaotic nature of the investigated data. The positive value of the Largest Lyapunov exponent is only one indicator of the presence of deterministic chaos. The others are fractal structure of the reconstructed attractor or limited prediction of the investigated system.

	Body part	Time delay	Embedding dimension	LLE
	Left femur	21	4	0.3157
	Right femur	20	4	0.0084
	Left foot	15	4	0.0476
	Right foot	16	5	-0.0206
	Left tibia	33	7	-0.0450
	Right tibia	23	5	0.1600

Table 1 .

 1 Results from nonlinear analysis procedure for each body part

Acknowledgments. The author is grateful for the reviews, which certainly helped raise the quality of the work. The author would like to acknowledge the Polish-Japanese Institute of Information Technology for the gait sequences recorded in the Human Motion Laboratory (HML).


Gianluca Barbon

Agostino Cortesi

Pietro Ferrara

Marco Pistoia

Omer Tripp

Privacy Analysis of Android Apps: Implicit Flows and Quantitative Analysis

A static analysis is presented, based on the theory of abstract interpretation, for verifying privacy policy compliance by mobile applications. This includes instances where, for example, the application releases the user's location or device ID without authorization. It properly extends previous work on datacentric semantics for verification of privacy policy compliance by mobile applications by (i) tracking implicit information flow, and (ii) performing a quantitative analysis of information leakage. This yields to a novel combination of qualitative and quantitative analyses of information flows in mobile applications.

Introduction

Security threats are increasing in the mobile space, in particular in the Android environment. Specifically, mobile devices contain different sorts of confidential information that software might access. Such information is usually protected by permissions. However, the solutions provided by current mobile operating systems are not satisfying, and expose the user to various threats [START_REF] Enck | Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones[END_REF]. In addition, various applications and (e.g., analytics and advertisement) libraries make use of and sometimes leak user confidential data. Mobile security is also a major concern in an enterprise environment, where firms allow the use of company applications in the employee's personal device, increasing the risk of leakage of confidential business data. Therefore, there is and increasing request and need to formally verify the behavior of mobile applications, and to assess (and possibly limit) the quantity of released data. On the opposite side, a complete absence of data leakage of data would compromise the functionalities of mobile software. For instance, a navigation app like Waze needs to access the user location and communicate it to its servers in order to show appropriate traffic information. However, the user might want to prevent to leakage of her location to the advertisement engine. Ideally, we would like to impose -via suitable privacy policies -constraints on levels of data release, and give the user better awareness of the direct and indirect actual information flow concerning her personal data.

In this context, current research follows two main approaches: a statistical one [START_REF] Lowe | Quantifying information flow[END_REF][START_REF] Mccamant | Quantitative information flow as network flow capacity[END_REF] and a language based one (e.g., information flow taint analysis) [START_REF] Arzt | Flowdroid: Precise context, flow, field, object-sensitive and lifecycleaware taint analysis for android apps[END_REF][START_REF] Hammer | Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs[END_REF][START_REF] Smith | Principles of secure information flow analysis[END_REF][START_REF] Sridharan | F4f: taint analysis of framework-based web applications[END_REF][START_REF] Tripp | Hybrid security analysis of web javascript code via dynamic partial evaluation[END_REF][START_REF] Tripp | Taj: effective taint analysis of web applications[END_REF]. Both approaches suffer some weaknesses: the former does not fit well for qualitative analysis, while the latter as it is too strict, due to the fact that the non-interference notion [START_REF] Denning | A lattice model of secure information flow[END_REF] yields too many false positives limiting the effectiveness of the analysis.

In this paper, we extend our previous work [START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF]. This includes two primary contributions: (i) we investigate also implicit flows, where previously we considered only direct information release paths, and (ii) we relate explicit and implicit information flow to a quantitative notion of information leakage. We formalize our approach in the abstract interpretation framework. The advantage of such a method is that it enabes a general abstraction of all possible executions of a given program. Therefore, following the abstract-interpretation framework [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], we design an enhanced concrete semantics that formalizes how the expressions generated by the program's execution maintain footprints of (possibly confidential) data stored in the local data-store of the mobile device. With this formalization of the concrete semantics, we show how to create a sound abstraction such that the analysis is computable.

This work leads to the definition of a framework that merges quantitative and qualitative approaches by taking advantage of their respective strengths. We exploited the evaluation of single operators for the former approach and the collection of quantities of released information for the latter. Last, but certainly not least, the definition of this method has revealed the important role of the implicit flow in the leakage of secret variables. We evaluated the effectiveness of this framework over some benchmark examples.

The paper is structured as follows. After a brief introduction that describes related research and fundamental notions in Section 2, Section 3 recalls the semantics introduced by Cortesi et al. [START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF] extending it to capture implicit flows as well. Section 4 introduces the new quantitative approach that is added to the semantics described in the previous Sections. Section 5 introduces an abstraction of the quantitative analysis. Finally, in Section 6 a few significant examples of real working applications are presented and analyzed. Section 7 concludes.

Background

This Section introduces some important notions that will be used throughout the rest of the paper, and briefly describes the current related research. Implicit Flows. Implicit flows were described by Denning [START_REF] Denning | A lattice model of secure information flow[END_REF] in 1976. Implicit flows have origins from the so called control statements, like if and while statements, where they are generated by their conditional expression. For instance, consider the following example:

if b then x = 0 else x = 1;
Even if the final value of x does not allows to directly recover the value of b, the latter affects the value of x, and an indirect information flow occurs from b to x. Of course, implicit flows may yield to malicious effects [START_REF] Russo | Implicit flows in malicious and nonmalicious code[END_REF].

Quantitative Approaches. A quantitative approach tracks some quantity, or measure, of leaked information. In [START_REF] Mccamant | Quantitative information flow as network flow capacity[END_REF] a new technique is proposed for determining the quantity of sensitive information that is revealed to public. The main idea presented by the authors consists in computing a maximum flow between the program inputs and the outputs, and by setting a limit on the maximum quantity of information revealed. The information flow is measured using a sort of network flow capacity, where the maximum rate of an imaginary fluid into this network represents the maximum extent of revealed confidential information. This method requires a dynamic approach in order to construct the graph, by performing multiple runs of the target program.

Quantitative value expressed as bits. McCamant et al. [START_REF] Mccamant | Quantitative information flow as network flow capacity[END_REF] introduced a quantity concept in order to measure bits of information that can be released by the observation of a specific execution of a program. One of the first attempts to quantify information flow is the one of Lowe [START_REF] Lowe | Quantifying information flow[END_REF]. The author described quantity as number of bits, and defined the information flow as information passing between an high level user and a low level user through a covert channel. An interesting feature presented in this work consists in the assignment of 1 bit of quantity also with absence of information flow. This means that the author considers the absence of information as having value 1 bit. Finally they also introduce a time notion in the flow analysis. Another interesting approach is the one by Clark et al. [START_REF] Clark | Quantitative analysis of the leakage of confidential data[END_REF][START_REF] Clark | Quantified interference for a while language[END_REF]. First, they analyse k bit variables, where 2 k are the values that can be represented from such variables. Second, they relate the maximum content of a variable to its data type, and they consider this as the possible quantity of leakage. Finally, they define the difference between the quantity of information of a confidential input and the amount of leaked information.

Security in Mobile Environments. Nowadays smartphones are used to store, modify and collect private and confidential data, e.g. location data or phone identifier. At the same time, a lot of malicious applications able to stole data or to track users exist. Mobile operating systems are not able to grant to users an appropriate control over confidential data and on how applications manage such data [START_REF] Enck | Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones[END_REF]. These limits make these platforms a potential target for attackers. An evolution of threats in mobile environments has been stressed also by the MacAfee Labs Threats Report [START_REF]Threats Report[END_REF]; in particular it underlines the existence of untrusted marketplaces and the increasing diffusion of open-source and commercial mobile malware source code, that facilitate the creation of such threats by unskilled attackers. Among mobile operating systems, Android is currently the most prevalent one [START_REF][END_REF], thus becoming the target of various threats. This mobile environment present different vulnerabilities. First, there is a lack of common definitions for securities and a high volume of available applications that guarantees the diffusion of malicious programs [START_REF] Enck | A study of android application security[END_REF]. Second, many applications make use of private information, like the IMEI (International Mobile Station Equipment Identity), and of advertising and analytic libraries, that sends user data to remote servers for profiling. Third, the opportunity to install also applications coming from untrusted marketplaces makes the verification of these applications harder [START_REF] Rasthofer | Droidforce: Enforcing complex, data-centric, system-wide policies in android[END_REF]. Last, but not least, even if Android requests to grant permission in order to install an application, this kind of control is not sufficient to avoid undesirable behaviour, because restrictions are not fine-grained [START_REF] Fritz | Highly precise taint analysis for android application[END_REF][START_REF] Hornyack | These aren't the droids you're looking for: Retrofitting android to protect data from imperious applications[END_REF].

Confidentiality Analysis in Mobile Environments. The importance of confidentiality analysis is growing in recent years, especially in the mobile space. In this field two main approaches can be found: dynamic and static analysis methods. Among the works that use the former method we can find those regarding the evaluation of permission-hungry mobile applications [START_REF] Arzt | Flowdroid: Precise context, flow, field, object-sensitive and lifecycleaware taint analysis for android apps[END_REF][START_REF] Rasthofer | Droidforce: Enforcing complex, data-centric, system-wide policies in android[END_REF]. In particular, the work of Enck et al. [START_REF] Enck | Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones[END_REF] presents TaintDroid, a tool that monitors sensitive data by using real time tracking, avoiding the needing to get access to the applications source code. The main idea consists in tracking sensitive data that flows through systems interfaces, used by applications to get access to local data. This approach has some limitations. For instance, it does not allow the tracking of control flows, and generates false positives. Another approach is the one of Hornyack et al. with AppFence [START_REF] Hornyack | These aren't the droids you're looking for: Retrofitting android to protect data from imperious applications[END_REF], which imposes privacy controls by retrofitting the Android environment, without the need to modify applications. Yet another approach, by Tripp and Rubin [START_REF] Tripp | A bayesian approach to privacy enforcement in smartphones[END_REF], is to reason about information release in terms of data values, rather than data flow, where the judgment is based on value similarity measures fed into a Bayesian learning algorithm. However, dynamic approaches present some weaknesses. First, they fail to discover some malicious behaviour, because applications have learned to recognize analysis during execution [START_REF] Fritz | Highly precise taint analysis for android application[END_REF]. Second, the majority of dynamic approaches uses coarse-grained approximations that lead to false alarms and also missed leaks [START_REF] Arzt | Flowdroid: Precise context, flow, field, object-sensitive and lifecycleaware taint analysis for android apps[END_REF], while on the contrary static ones are able to discover potential leaks before the execution of the analysed application.

Collecting Semantics

In this section we introduce the collecting semantics, that consists in the first fundamental step of our framework design. We define the syntax, the domains, and the semantics with a specific focus on control statements.

Syntax

The formalization is focused onthree types of data: strings (s ∈ S), integers (n ∈ Z) and Booleans (b ∈ B). sexp, nexp, and bexp denotes string, integer, and Boolean expressions, respectively. is used to represent data-store entries, and lexp denotes label expressions. For instance, string expressions are defined by: sexp ::

= s | sexp 1 • sexp 2 | encrypt(sexp, k) | sub(sexp, nexp 1 , nexp 2 ) | hash(sexp) | read(lexp),
where • represents concatenation, encrypt the encryption of a string with a key k, sub the substring of sexp between n 1 and n 2 , hash the computation of the hash value, and read the function that returns the value in the data-store that corresponds to the given label.

Domain

By adexp we denote an atomic data expression that tracks the data sources of a specific value. Formally, an atomic data expression adexp is a set of elements i , {(op j , l j ) : j ∈ J} , representing that the datum corresponding to label i has been combined with data corresponding to labels j through operators op j to get the actual value of the expression.

The set of atomic data expressions is defined by:

D = { i , L i : i ∈ I ⊆ N, i ∈ Lab, L i ⊆ ℘(Op × Lab)},
where Lab is the set of labels, and Op is the set of operators.

An environment relates variables to their values as well as to their atomic data expression. Formally, Σ = D × V, where (i) D : Var -→ ℘(D) maps local variables in Var to a corresponding adexp, and (ii)

V : Var -→ (Z ∪ S)
is the usual environment that tracks value information. The special symbol represents data coming from the user input and from the constants of the program. Instead, data coming from the concrete data-store C are represented by= { i , ∅ : i ∈ I} ⊆ D such that ∀i, j ∈ I : i j ⇒ i j , and i .

Collecting Semantics

We extend the notion of atomic data expressions to collect also implicit flows generated by if and while statements. Such flows are treated in the same way as explicit flows by collecting the Boolean expression (bexp) of a conditional or loop statement, and considering it as an adexp with its operators and sources.

Definition 1 (Extended Atomic Data Expressions).

We redefine the set of atomic data expressions as:

D = { i , L i : i ∈ I}, { j , L j : j ∈ J} where L ⊆ ℘(Op × Lab).
An extended atomic data expression can be seen as a pair of two atomic data expressions, where the second one refers to the implicit flows (notice that also a Boolean or relational operator may appear). Formally, d = d e , d i , where d e and d i correspond to the explicit and implicit flows, respectively. In this way we collect also the Boolean operators.

Consider the conditional statement: if exp then x = case 1 else x = case 2 . We can interpret each expression as a combination of explicit and implicit flow:

d i f cond = d e , d i d case 1 = d e case 1 , d i case 1 d case 2 = d e case 2 , d i case 2
Notice that d i in case 1 and case 2 expresses only the implicit flow generated inside the two branches of the if statement, and it does not include the implicit flow that comes from the evaluation of the Boolean expression exp. Then, if the case 1 is chosen, we obtain:

d result = d e case 1 , {d i case 1 ∪ d e i f ∪ d i i f } where d e i f and d i i f
represent the flows in the if condition, both collected in the implicit flow of all the subsequent expressions. The value associated to x after the if-then-else statement makes explicit that x has implicit dependence on the sources of the Boolean expression. For instance, if exp = y ≥ 0, it will track that the value of x is dependent on the value of y. We denote by S N : nexp × V → Z, S S : sexp × V → S, and S B : bexp × V → {true, false} the standard concrete evaluations of numerical, string, and Boolean expressions. In addition, S L : lexp × Σ → Lab that returns a data label given a label expression. The semantics of expressions on atomic data S A : sexp × Σ → ℘(D) is described in Figure 1. The semantics has been improved w.r.t. [START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF] with a new operator, checkpwd(sexp 1 , sexp 2 ), that returns true if a secret password is equal to a given value. In addition, we track both explicit and implicit flows. In particular, we do not create any implicit flow, and we simply propagate the implicit flows generated by previous expressions:

S[[c]](a, v), { j , L j : j ∈ J} .
Similarly, we rewrite the semantics of statements that create implicit flow, that is, the semantics of if and while statements (Fig. 2). The definition of this semantics is split into explicit (S e ) and implicit (S i ) flows. We add the skip statement to handle the exit from a loop statement like the while.

S A [[x]](a, v) = a(x) S A [[read(lexp)]](a, v) = { S L [[lexp]](a, v), ∅ } S A [[encrypt(sexp, k)]](a, v) = { 1 , L 1 ∪ {([encrypt, k], 1 )} : 1 , L 1 ∈ S A [[sexp]](a, s, n)} S A [[s]](a, v) = { , ∅ } S A [[sexp 1 • sexp 2 ]](a, v) = { 1 , L 1 ∪ {(•, 2 )} , 2 , L 2 ∪ {(•, 1 )} : 1 , L 1 ∈ S A [[sexp 1 ]](a, v) , 2 , L 2 ∈ S A [[sexp 2 ]](a, v)} S A [[sub(sexp, k 1 , k 2 )]](a, v) = { 1 , L 1 ∪ {([sub, k 1 , k 2 ], 1 )} : 1 , L 1 ∈ S A [[sexp]](a, v)} S A [[hash(sexp)]](a, v) = { 1 , L 1 ∪ (hash, 1 ) : 1 , L 1 ∈ S[[sexp]](a, v)} S A [[checkpwd(sexp, s)]](a, v) = { 1 , L 1 ∪ {(checkpwd, )} : 1 , L 1 ∈ S A [[sexp 1 ]](a, v)} Fig. 1: Semantics of Expressions on Atomic Data S[[x := sexp]](a, v) = (a[x → S A [[sexp]](a, v)], v[x → S S [[sexp]](v)]) S[[skip]](a, v) = (a, v) S[[send(sexp)]](a, v) = (a, v) S[[c 1 ; c 2 ]](a, v) = S[[c 2 ]](S[[c 1 ]](a, v))) S[[if c 1 then c 2 else c 3 ]](a, v) =              S e [[c 2 ]](a, v), S i [[c 2 ]](a, v) ∪ S e [[c 1 ]](a, v) ∪ S i [[c 1 ]](a, v) if S B [[c 1 ]](v) S e [[c 3 ]](a, v), S i [[c 3 ]](a, v) ∪ S e [[¬c 1 ]](a, v) ∪ S i [[c 1 ]](a, v) otherwise S[[while c 1 do c 2 ]](a, v) = S[[ if (c 1 ) then (c 2 ; while c 1 do c 2 ) else skip ]](a, v)

Fig. 2: Concrete Semantics of Statements

Example Suppose that y contains a value arising from a data store labeled 1 , while x contains user input. We assume that > y. The following are the expressions computed by the collecting semantics, where the subscript represents the code line of the expression:

y 1 : { 1 , ∅ }, ∅ (x<=y) 4 : { 1 , {(>=, )} }, ∅ y+3 7 : { 1 , {(+, )} }, ∅ z=y+3 7 : { 1 , {(+, )} } explicit flow , { 1 , {(<, )} } implicit flow x=x+z 8 : { 1 , {(+, )} }, { 1 , {(<, )} }
The first three expressions are not affected by implicit flows, so the implicit component in these expressions is ∅. The second expression refers to the if Boolean expression, and the fourth one refers to the assignment of the else branch, and it takes into account the implicit flow generated by the if statement.

Quantitative Semantics

In this Section, we extend the collecting semantics by introducing a quantitative notion of information flow.

Quantitative Concrete Domain

We begin by representing values having a binary form to express quantities of information flows. In this way, we adopt a standardized evaluation of quantities coming from different data types.

Definition 2 (Label Dimension).

Let i be the label of a location in the data-store. ω returns the size of the memory location corresponding to the given label, and it is defined by nbit i := ω( i ), where nbit is the retrieved dimension in bits.

The value returned ω depends on the particular type of the datum:

numbers: for the sake of simplicity we consider only integer numbers. The number of bits for a label containing such kind of data is: nbits = log 2 (n) +1, -string: we adopt a simplified representation of characters. In particular, we consider an encoding representing only English alphabet (with uppercase and lowercase letters) and numerical digits. We then have 26+26+10 elements. Thus this encoding requires 6 bits for each character, and nbits = 6 × l str where l str represents the number of characters of string str, and -Boolean: such values can be only 0 or 1, so they require only 1 bit.

We now extend the collecting semantics to take into account quantities of information by adding a new expression associated to the extended adexp to the concrete state.

Definition 3 (Quantitative Expression).

We define a quantitative expression qadexp as a sequence of pairs of labels associated with quantitative values , q . This collects the quantity of information generated by implicit flows for the given label . This sequence is combined with a d q in qadexp in a unique expression as follows:

d := ( d e , d i , d q )
Therefore, we represent data expressions as follows:

D = { i , L i : i ∈ I}, { j , L j : j ∈ J} , { k , q k : k ∈ J}
where k are the labels used in statements that generate implicit flow, while q k is the associated quantity of information.

Every single pair k , q k tracks the quantity of information that label k potentially released through implicit flow. Notice that the expression d := ( d e , d i , d q ) highlights how our analysis is the result of the combination of two approaches, and in particular (i) the first two components expression comes from a qualitative approach to explicit and implicit flows, and (ii) the last one is the result of a quantitative approach.

We define as Q the domain of quantities of information. We are now in position to introduce a function that describes how quantities are collected. Definition 4 (Quantitative function φ). Let φ be a function that updates a quantitative value each time the associated label is involved in an implicit flow, such that:

val post := val pre + φ stm ( )
where φ stm : → val and pre and post refer to the statement (stm) execution.

Quantities are represented as an interval [val, val] were higher and lower bound coincide. This will allow an easier lift to the abstract value. Anyway, for the sake of readability, the singleton interval [val, val] will be denoted by a single value val.

We have to track quantities of implicit flow generated by if and while statements. Conditional expressions can result only in true and false. Thus, the information obtained from the evaluation of a Boolean condition consists only of one bit [START_REF] Mccamant | A simulation-based proof technique fordynamic information flow[END_REF].

For the sake of simplicity, we consider only the > and < (strict) operators. This avoids problems with equalities (a == b) allowing the collection of only one bit of information for each if statement [START_REF] Clark | Quantitative analysis of the leakage of confidential data[END_REF][START_REF] Clark | Quantified interference for a while language[END_REF]. Figure 3 defines the semantics of conditional expressions. Notice that we do not yet introduce quantities, while we only express how to collect equality in conditional statements using integers instead of Boolean values..

S[[sexp]](a, v) = { 1 , L 1 ∪ {(>, )} : 1 , L 1 ∈ S A [[sexp 1 ]](a, v)} S[[¬sexp]](a, v) = { 1 , L 1 ∪ {(<, )} : 1 , L 1 ∈ S A [[sexp 1 ]](a, v)} S[[sexp 1 > sexp 2 ]](a, v) = { 1 , L 1 ∪ {(>, 2 )} , 2 , L 2 ∪ {(<, 1 )} : 1 , L 1 ∈ S A [[sexp 1 ]](a, v) , 2 , L 2 ∈ S A [[sexp 2 ]](a, v)} S[[sexp 1 < sexp 2 ]](a, v) = { 1 , L 1 ∪ {(<, 2 )} , 2 , L 2 ∪ {(>, 1 )} : 1 , L 1 ∈ S A [[sexp 1 ]](a, v) , 2 , L 2 ∈ S A [[sexp 2 ]](a, v)}

Quantitative Concrete Semantics

Let ϕ be function that maps variables to quantities (ϕ : Var → qadexp). We now introduce the quantity notion into our quantitative collecting semantics. The initial quantity value is φ stm ( i ) = 0 ∀i, and it is modified by φ stm only for the statements that generate implicit flow. This means that in the other expressions the ϕ component will be carried as is. The new semantics is defined in Figures 4, 5 and6.

S A [[x]](a, ϕ, v) = a(x) S A [[read(lexp)]](a, ϕ, v) = { S L [[lexp]](a, ϕ, v), ∅ } S A [[encrypt(sexp, k)]](a, ϕ, v) = { 1 , L 1 ∪ {([encrypt, k], 1 )} : 1 , L 1 ∈ S A [[sexp]](a, ϕ, s, n)} S A [[s]](a, ϕ, v) = { , ∅ } S A [[sexp 1 • sexp 2 ]](a, ϕ, v) = { 1 , L 1 ∪ {(•, 2 )} , 2 , L 2 ∪ {(•, 1 )} : 1 , L 1 ∈ S A [[sexp 1 ]](a, ϕ, v) , 2 , L 2 ∈ S A [[sexp 2 ]](a, ϕ, v)} S A [[sub(sexp, k 1 , k 2 )]](a, ϕ, v) = { 1 , L 1 ∪ {([sub, k 1 , k 2 ], 1 )} : 1 , L 1 ∈ S A [[sexp]](a, ϕ, v)} S A [[hash(sexp)]](a, ϕ, v) = { 1 , L 1 ∪ (hash, 1 ) : 1 , L 1 ∈ S[[sexp]](a, ϕ, v)} S A [[checkpwd(sexp, s)]](a, ϕ, v) = { 1 , L 1 ∪ {(checkpwd, )} : 1 , L 1 ∈ S A [[sexp 1 ]](a, ϕ, v)} Fig. 4: Quantitative Semantics of Expressions on Atomic Data S[[x := sexp]](a, ϕ, v) = (a[x → S A [[sexp]](a, ϕ, v)], v[x → S S [[sexp]](v)]) S[[skip]](a, ϕ, v) = (a, ϕ, v) S[[send(sexp)]](a, ϕ, v) = (a, ϕ, v) S[[c 1 ; c 2 ]](a, ϕ, v) = S[[c 2 ]](S[[c 1 ]](a, ϕ, v)))
Fig. 5: Quantitative Concrete Semantics of Statements

S[[if c 1 then c 2 else c 3 ]](a, v) = • if S B [[c 1 ]](v) is True then: let (a , ϕ , v ) = S e [[c 2 ]](a, ϕ, v), S i [[c 2 ]](a, ϕ, v) ∪ S e [[c 1 ]](a, ϕ, v) ∪ S i [[c 1 ]](a, ϕ, v) in (a , ϕ [( i , q i )/( i , q i + φ stm (c 1 )) : i ∈ src(c 1 )], v ) • otherwise: let (a , ϕ , v ) = S e [[c 3 ]](a, ϕ, v), S i [[c 3 ]](a, ϕ, v) ∪ S e [[¬c 1 ]](a, ϕ, v) ∪ S i [[c 1 ]](a, ϕ, v) in (a , ϕ [( i , q i )/( i , q i + φ stm (c 1 )) : i ∈ src(c 1 )], v )
where φ stm is the quantitative function in Def. 4

S[[while c 1 do c 2 ]](a, ϕ, v) = S[[ if (c 1 ) then (c 2 ; while c 1 do c 2 ) else skip ]](a, ϕ, v)

Abstract Semantics

We now extend the abstract semantics proposed by Cortesi et al. [START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF] to implicit flows and a quantitative analysis. Our abstract semantics is parameterized by a value domain V a , and a label abstraction. First of all, we need to define a computable abstraction of quantities.

Definition 5 (Quantity Value Abstraction).

The quantity associate with label expressions is an interval. Each label a is associated to an interval of quantities where the lower and the upper bounds are the minimum and the maximum quantities of information that can be released through the implicit flow for that specific label. Therefore, the abstract qadexp is defined as a k , q a k min , q a k max .

If we have unbounded quantities, the analysis reveals a complete leakage of the associated label. In this case, the upper bound of the intervals is unbounded. Instead, for the lower bound the minimum quantity is zero.

Atomic Data Abstraction Extension

We now define the atomic data abstraction extended for handling implicit flows and quantities. Definition 6 (Abstract Extended Atomic Data and Quantities). Let us consider a set of atomic data and quantity values. We define abstract elements as

{ a w , L a w , L a w : w ∈ W}, { a z , L a z , L a z : z ∈ Z} , { a g , q a g , q a g : g ∈ Z}
where:

a w is an element that abstracts labels in Lab to track explicit flow, -a z and a g are elements that abstract labels in Lab to track implicit flow, -L a w = {(op a iw , a iw ) : i ∈ I} and L a z = {(op a jz , a jz ) : j ∈ J} represent the underapproximation of a w and a z with labels abstracted by a iw and a jz , and track explicit and implicit flows, respectively, -L a w = {(op a iw , a iw ) : i ∈ I } and L a z = {(op a jz , a jz ) : j ∈ J } represent the overapproximation of a w and a z with labels abstracted by a iw and a jz , and track explicit and implicit flows, respectively, -L a w ⊆ L a w and L a z ⊆ L a z , -q a g is an element that abstract quantites associated to a a g element, -q a kg : k ∈ J is an under-approximation of the interval of possible quantities of information associated to a g with values represented by q a kg , -q a kg : k ∈ J is an over-approximation of the interval of possible quantities of information associated to a g with values represented by q a kg , and q a g q a g .

As a corollary, we define the source set of an atomic datum { a w : w ∈ W}, { a z : z ∈ Z} expressed as src(d).

Although we inherit the abstraction and concretization functions for the explicit flows [START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF], we have to extend them to handle quantities.

Definition 7 (Quantitative Abstraction function).

We denote by α Q the abstraction function that given a set {( k , q k ) : k ∈ J} returns {(α Lab ( k ), q a k , q a k ) : k ∈ J}, where q a k , q a k represent the bounds of the interval that approximates all possible quantitative values in the abstract domain Q a . Definition 8 (Quantitative Abstraction function for Atomic Data). Given a concrete atomic datum d = { i , L i : i ∈ I}, { j , L j : j ∈ J} , { k , q k : k ∈ J} , we define an abstraction function α : ℘(D) -→ AD as:

α s (d) = { α Lab ( i ), α Lab (L i ), α Lab (L i ) : i ∈ I}, { α Lab ( j ), α Lab (L j ), α Lab (L j ) : j ∈ J} , { α Lab ( k ), α Q (q k ) : k ∈ J}
The abstraction function is then extended to sets by computing the upper bound of the point-wise application of α s to all the elements of the given set.

Abstract Semantics of Statements

Expressions are abstracted via an abstract data label and an abstract value (AD a and V a , respectively). In Figure 7 the abstract semantics of statements taking into account implicit flows is defined Then, in Figure 8 this semantics is extended with the quantitative dimension. We omit here the abstract semantics of expressions, as it does not generate any implicit flow, and we refer the interested reader to Cortesi et. al [START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF] for more details.

S a [[x := sexp]](a a , v a ) = (a a , S a v [[x := sexp]](v a )) S a [[skip]](a a , v a ) = (a a , v a ) S a [[send(sexp)]](a a , v a ) = (a a , v a ) S a [[c 1 ; c 2 ]](a a , v a ) = S a [[c 2 ]](S a [[c 1 ]](a a , v a )) S a [[if c 1 then c 2 else c 3 ]](a a , v a ) = S a e [[c 2 ]](a a , S a e [[c 1 ]](v a )) S a e [[c 3 ]](a a , S a e [[¬c 1 ]](v a )), S a i [[c 2 ]](a a , S a e [[c 1 ]](v a )) S a e [[c 1 ]](a a , v a ) S a i [[c 1 ]](a a , v a ) S a i [[c 3 ]](a a , S a e [[¬c 1 ]](v a )) S a e [[¬c 1 ]](a a , v a ) S a i [[c 1 ]](a a , v a ) S a [[while c 1 do c 2 ]](a, v) = f ix(S a [[ if (c 1 ) then (c 2 ; while c 1 do c 2 ) else skip ]](a a , v a )) Fig. 7: Abstract Semantics of Statements S a [[x := sexp]](a a , ϕ a , v a ) = (a a [x → S a A [[sexp]](a a , ϕ a , v a )], v a [x → S a S [[sexp]](v a )]) S a [[skip]](a a , ϕ a , v a ) = (a a , ϕ a , v a ) S a [[send(sexp)]](a a , ϕ a , v a ) = (a a , ϕ a , v a ) S a [[c 1 ; c 2 ]](a a , ϕ a , v a ) = S a [[c 2 ]](S a [[c 1 ]](a a , ϕ a , v a )) S a [[if c 1 then c 2 else c 3 ]](a a , ϕ a , v a ) = let (a a , ϕ a , v a ) = S a e [[c 2 ]](a a , ϕ a , S a e [[c 1 ]](v a )) S a e [[c 3 ]](a a , ϕ a , S a e [[¬c 1 ]](v a )), S a i [[c 2 ]](a a , ϕ a , S a e [[c 1 ]](v a )) S a e [[c 1 ]](a a , ϕ a , v a ) S a i [[c 1 ]](a a , ϕ a , v a ) S a i [[c 3 ]](a a , ϕ a , S a e [[¬c 1 ]](v a )) S a e [[¬c 1 ]](a a , ϕ a , v a ) S a i [[c 1 ]](a a , ϕ a , v a ) in (a a , ϕ a [( a
i , q a i , q a i )/( a i , q a i + φ a stm (c 1 ), q a i + φ a stm (c 1 )) : a i ∈ src(c 1 )], v a ) where φ stm is the quantitative function in Def. 4 We need to abstract the number of iterations of a while loop to precisely approximate the quantity of information leaked by a loop. Our approach is composed by two steps: a while interval analysis approximating the number of iterations, followed by an extended adexp collection with quantitative values.

Step (a): while interval analysis We add a counter initialized to 0 at the beginning, and we increment it by one at each loop iteration. In this way, we can apply a standard interval analysis to infer an upper bound on the number of iterations of a loop. Example Consider the following program, where i represents the counter we added:

x=-2 (i = 0) while (x<27) x= x+2 (i = i + 1) print (x)
At the end of the analysis, the interval domain can infer i → [0..15] (e.g., by applying a narrowing operator after widening [START_REF] Cortesi | Widening and narrowing operators for abstract interpretation[END_REF]). The upper bound of the interval of variable i returns the number of iterations of the loop, that is, 15. Then the upper bound on the number of iterations 15 becomes [START_REF] Arzt | Flowdroid: Precise context, flow, field, object-sensitive and lifecycleaware taint analysis for android apps[END_REF][START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF], where 4 are the number of bits leaked in 15 iterations.

Step (b): extended adexp collection with quantitative value At the end of the while interval analysis, we apply a quantitative value analysis. Example Consider the following example: secret = read(. . .) found = false while (! found) { pwd = user input() found = checkpwd(pwd, secret)} At the end of the first iteration of the analysis of the loop, we obtain:

secret 1 : 1 , ∅, ∅ , ∅ found 2 : ∅, ∅ !found 3 : ∅, ∅ pwd 4 : ∅, ∅ found 5 : 1 , {(checkpwd, )}, {(checkpwd, )} , ∅
Notice that no quantitative information has yet been released. In fact, the Boolean condition of the while loop is checked against a constant value (false) during the first iteration. However, found might be still false, and the loop would be iterated another time. Then, starting from the second iteration the implicit flow will contain the new definition of the variable found, thus each expression inside the scope of the while will be:

. . . explicit flow . . . , 1 , {(checkpwd, )}, {(checkpwd, ), (<, ), (>, }

Notice that the function checkpw(p 1 ,p 2 ) returns a Boolean value, so one bit. This means that we are accumulating a bit of information at each iteration.

As soon as the implicit flow comes into the picture, we have to consider the quantity interval computed in step (a):

. . . explicit flow . . . , 1 , {(checkpwd, )}, {(checkpwd, ), (<, ), (>, } , 1 , 1, 4

If inside a while loop there is an obfuscating operator (e.g., encryption or hashing) applied to confidential data, we need to know the quantity of information that is released by the operator. For instance, in the previous example the operator checkpwd(p 1 ,p 2 ) checks if the password given by the user is correct, and it returns a Boolean value. Thus the analysis accumulates a single bit at each iteration, and the quantitative value will depend on the number of iterations. However, other operators might release more information. In this case, we compute the product of the number of iterations and the released bits.

Applications

In this Section, we discuss the results of our analysis of some examples listed in the DroidBench application set [20], created by the Secure Software Engineering group of the Technische Universität Darmstadt. This set is open source, and it is a standard benchmark to test static and dynamic analyses. We chose the examples that specifically deal with implicit flows. An interesting comparison can be made with the work by Tripp and Rubin [START_REF] Tripp | A bayesian approach to privacy enforcement in smartphones[END_REF], as they also used DroidBench as testing environment. Their approach performs very well on the whole test set (also with respect to other tools, like TaintDroid), but it suffers from false negatives in case of implicit flows. Our analysis instead allows to cope with these particular cases, for instance the ones due to custom transformations of private data in the ImplicitFlow1 test program. This is because we adopted a different approach, that instead of looking for privacy sinks, observes the whole flow of confidential data and operations applied to them. For the sake of readability, we simplified some library functions, and we added some semantic rules to support some primitive functions contained in these examples, and that were not part of the minimal language we adopted in our formalization. For each example, we describe the results of the collecting semantics on a particular concrete state, and we then perform a two-stages static analysis. First we illustrate the results without the quantitative component qadexp, and we then discuss the results of the quantitative semantics.

ImplicitFlow1

The first example is an application that reads the device identifier (IMEI), obfuscates it, and then leaks it. The obfuscation can be performed with two functions with two different obfuscation powers (namely, low and high).

Fig. 3 :

 3 Fig. 3: Concrete Semantics of Conditional Expressions

Fig. 6 :

 6 Fig. 6: Quantitative Concrete Semantics of Control Statements

Fig. 8 :

 8 Fig. 8: Quantitative Abstract Semantics of Statements

  public class ImplicitFlow1 extends Activity { protected void onCreate(...) { // ... String imei = getDeviceId(); // device id String obfuscatedIMEI = obfuscateIMEI(imei); writeToLog(obfuscatedIMEI); obfuscatedIMEI = hardObfIMEI(imei); writeToLog(obfuscatedIMEI); } private String obfuscateIMEI(String imei){ String result = " " ; char[] imeiAsChar = imei.toCharArray(); int len = imeiAsChar.length(); int i = 0; int shift = 49; while ( i < len ){ result += (char) ((( int )imeiAsChar[i]) + shift ); // returns ' a' for '0', ' b' for '1', ... int )imeiAsChar[i]) +1 + ( i * i )%62); 40 i ++;

First of all, we extend the semantics to the new functions contained in this example. For the most part, this extension is very intuitive and straightforward.

getDeviceId returns the IMEI from the datastore, toCharArray convert the label to a char, length returns the dimension (in integer) of an array and Log writes the argument to a log file. cast(type) represents the type casting. We also add the modulo % operator to the semantics. We collect it as mod in our domain, and its behavior is similar to other arithmetic operators. As for arrays, when we refer to a single element of the array, we assume to perform a

where k 1 and k 2 are the same element and are used as a sort of index in the array.

Concrete Analysis

The device identifier IMEI is contained in the data-store and can be retrieved through getDeviceId, that behaves like a S A [[read(lexp)]](a, v). We also add a counter that allows to count the number of iterations in the loop. Trivially, at the end of each cycle this value will be equal to the dimension of the IMEI, that is, 14. As we can see from the concrete analysis, there is no noticeable difference between the two functions. Indeed, both example apply these function inside a loop, and in both the conditional expressions depend on the dimension of the secret label.

Abstract Analysis

The main differences between the concrete and abstract semantics consist in (i) considering when the loop condition holds and does not (unlike the concrete semantics that always knows a precise value), and (ii) the application of the interval analysis to over-approximate the number of iterations. Notice that since the dimension of the IMEI does not change, the corresponding label can be abstracted with full precision. The same applies to its dimension. 1 , ∅, ∅ , ∅ imeiAsChar 18 :

1 , {(toCharArray, 1 )}, {(toCharArray, 1 )} , ∅ len 19 :

1 , {(length, 1 )}, {(length, 1 )} , ∅ while cond 23 :

1 , {(length, 1 ), (>, )}, {(length, 1 ), (>, )} , ∅ result 24 :

1 , {([sub, , ], 1 ), (cast(int), 1 ), (+, ), (cast(char), 1 ), (+, )}, {([sub, , ], 1 ), (cast(int), 1 ), (+, ), (cast(char), 1 ), (+, )} ,

Quantitative Analysis

The interval analysis approximates the minimum and maximum number of iterations of the loop. Through these bounds, we compute an interval of quantities, that infers the minimum and the maximum amount of information revealed through implicit flows. However, in this particular example the number of iterations can be precisely inferred because it is performed on a fixed value (the dimension of the IMEI ). Thus, we infer that the loop is iterated 14 times. Each iteration of the loop leaks one bit of information. We now infer the number of bits using the method described in the Section 5.2:

So, in both loops, the qadexp is 1 , 4, 4 .

ImplicitFlow2

In this example, the user has to type a password. Then, this password is compared to the correct one, that comes from the data-store. After this evaluation, a message is saved to a log file. This operation leaks information through an implicit flow, since the logged message depends on the correctness of the password.

Concrete Analysis

We reuse the semantics of Log defined for the previous example (S A [[Log(sexp)]](a, v) = (a, v)). The abstract semantics is similar. We now shows the results of the concrete semantics, assuming that the password provided by the user is not correct. The concrete data-store contains only the label that corresponds to the variable superSecure, that is, 1 , ∅ .

Abstract Analysis

We now present the results of the abstract semantics. We adopt the same label of the concrete semantics. Quantitative Analysis We abstract quantities with an interval. In this case study, there is an implicit flow in the first if statement:

This value is then propagated until the Log statement that leaks it.

ImplicitFlow3

Like in the previous example, this example checks if a password provided by a user matches the correct password. However, in this case the information is leaked through the creation of objects.

Concrete Analysis

We reuse the Log semantic described in the previous example. We assume that the password typed by the user is correct. As in the previous example, the concrete data-store contains only one label { 1 , ∅ } corresponding to superSecure.

Quantitative Analysis

In this example, there is only one i f statement that generates implicit flow. This statement exposes 1 bit of quantity of information:

This value will remain the same in all the following qadexps.

Discussion

As emphasized by the examples above, the adoption of a quantitative analysis allows the evaluation of quantities of confidential data that might be released. In ImplicitFlow1, the analysis tells that an implicit flows exists, that confidential labels are contained in it, and it also estimate the potential quantities of data released. This quantity is calculated by the operations implemented in the code, so by the operations that obfuscate the confidential label. The application of given policies [START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF] will allow to establish whether the released quantities are allowed or not. Any considerations about the safeness of the analyzed application are thus referred to the type of applied policy. In particular, as for ImplicitFlow1, we are able to calculate how much the while loop affects the produced quantity of data. Indeed, it allows to understand that, given a fixed (and possibly low) number of loop iterations, the quantity of confidential data that might be released will not be high. In conclusion, this analysis is not only capable of locating implicit flows, but also to evaluate their importance. In fact, if the released values will be low, with respect to a given policy, the implicit flow will be negligible.

Conclusions

In this paper, we extended the framework for tracking explicit flows introduced in [START_REF] Cortesi | Datacentric semantics for verification of privacy policy compliance by mobile applications[END_REF] with respect to implicit flows and quantitative analysis, showing the effectiveness of this approach on significant examples. This framework can support complex hybrid policies, i.e. policies that can grant both qualitative and quantitative thresholds.

Aknowledgments Work partially supported by the Italian MIUR project "Security Horizons".