Hélène Collavizza

Claude Michel

Michel Rueher

Searching critical values for floating-point programs ⋆

Programs with floating-point computations are often derived from mathematical models or designed with the semantics of the real numbers in mind. However, for a given input, the computed path with floating-point numbers may significantly differ from the path corresponding to the same computation with real numbers. As a consequence, developers do not know whether the program can actually produce very unexpected outputs. We introduce here a new constraint-based approach that searches for test cases in the part of the over-approximation where errors due to floating-point arithmetic could lead to unexpected decisions.

Introduction

In numerous applications, programs with floating-point computations are derived from mathematical models over the real numbers. However, computations on floating-point numbers are different from calculations in an idealised semantics1 of real numbers [START_REF] Goldberg | What every computer scientist should know about floating point arithmetic[END_REF]. For some values of the input variables, the result of a sequence of operations over the floating-point numbers can be significantly different from the result of the corresponding mathematical operations over the real numbers. As a consequence, the computed path with floating-point numbers may differ from the path corresponding to the same computation with real numbers. This can entail wrong outputs and dangerous decisions of critical systems. That's why identifying these values is a crucial issue for programs controlling critical systems.

Abstract interpretation based error analysis [START_REF] Chen | A sound floating-point polyhedra abstract domain[END_REF] of finite precision implementations computes an over-approximation of the errors due to floating-point operations. The point is that state-of-the-art tools [START_REF] Delmas | Towards an industrial use of FLUCTUAT on safety-critical avionics software[END_REF] may generate numerous false alarms. In [START_REF] Ponsini | Verifying floating-point programs with constraint programming and abstract interpretation techniques[END_REF], we introduced a hybrid approach combining abstract interpretation and constraint programming techniques that reduces the number of false alarms. However, the remaining false alarms are very embarrassing since we cannot know whether the predicted unstable behaviors will occur with actual data.

More formally, consider a program P , a set of intervals I defining the expected input values of P , and an output variable x of P on which depend critical decisions, e.g., activating an anti-lock braking system. Let [x R , x R ] be a sharp approximation over the set of real numbers R of the domain of variable x for any input of P . [x F , x F ] stands for the domain of variable x in the over-approximation computed over the set of floating-point F for input values of I. The range [x R , x R ] can be determined by calculation or from physical limits. It includes a small tolerance to take into account approximation errors, e.g. measurement, statistical, or even floating-point arithmetic errors. This tolerance -specified by the userdefines an acceptable loss of accuracy between the value computed over the floating-point numbers and the value calculated over the real numbers. Values outside the interval [x R , x R ] can lead a program to misbehave, e.g. take a wrong branch in the control flow.

The problem we address in this paper consists of verifying whether there exist critical values in I for which the program can actually produce a result value of x inside the suspicious intervals [x F , x R ) and (x R , x F ]. To handle this problem, we introduce a new constraint-based approach that searches for test cases that hit the suspicious intervals in programs with floating-point computations. In other words, our framework reduces this test case generation problem to a constraint-solving problem over the floating-point numbers where the domain of a critical decision variable has been shrunk to a suspicious interval. A constraint solver -based on filtering techniques designed to handle constraints over floating-point numbers-is used to search values for the input data. Preliminary results of experiments on small programs with classical floating-point errors are encouraging.

The CPBPV FP, the system we developed, outperforms generate and test methods for programs with more than one input variable. Moreover, these search strategies can prove in many cases that no critical value exists.

Motivating example

Before going into the details, we illustrate our approach on a small example. Assume we want to compute the area of a triangle from the lengths of its sides a, b, and c with Heron's formula:

s * (s -a) * (s -b) * (s -c)
where s = (a + b + c)/2. The C program in Fig. 1 implements this formula, when a is the longest side of the triangle.

The test of line 5 ensures that the given lengths form a valid triangle. Now, suppose that the input domains are a ∈ [5, 10] and b, c ∈ [0, 5]. Over the real numbers, s is greater than any of the sides of the triangle and squared_area cannot be negative. Moreover, squared_area cannot be greater than 156.25 over the real numbers since the triangle area is maximized for a right triangle with Tools performing value analysis over the floating-point numbers [START_REF] Delmas | Towards an industrial use of FLUCTUAT on safety-critical avionics software[END_REF][START_REF] Ponsini | Refining abstract interpretation based value analysis with constraint programming techniques[END_REF] approximate the domain of squared_area to the interval [-1262.21, 979.01]. Since this domain is an over-approximation, we do not know whether input values leading to squared_area < 0 or squared_area > 156.25 actually exist. Note that input domains -here a ∈ [5,10] and b, c ∈ [0,5]-are usually provided by the user.

Assume the value of the tolerance3 ε is 10 -5 , the suspicious intervals for squared_area are [-1262.21, -10 -5 ) and (156.25001, 979.01]. CPBPV FP, the system we developed, generated test cases for both intervals: CPBPV FP could also prove the absence of test cases for a tolerance ε = 10 -3 with squared_area > 156.25 + ε.

In order to limit the loss of accuracy due to cancellation [START_REF] Goldberg | What every computer scientist should know about floating point arithmetic[END_REF], line 7 of Heron's program can be rewritten as follows:

squared_area = ((a+(b+c))*(c-(a-b))*(c+(a-b))*(a+(b-c)))/16.0f;
However, there are still some problems with this optimized program. Indeed, CPBPV FP found the test case a = 7.0755463, b = 4.350216, c = 2.72533, and squared_area equals -1.0000001•10 -5 for interval [-1262.21, -10 -5 ) of squared_area. There are no more problems in the interval (156.25001, 979.01] and CPBPV FP did prove it. This section details the framework we designed to generate test cases reaching suspicious intervals for a variable x in a program P with floating-point computations.

The kernel of our framework is FPCS [14, 13, 1, 12], a solver for constraints over the floating-point numbers; that's to say a symbolic execution approach for floating-point problems which combines interval propagation with explicit search for satisfiable floating-point assignments. FPCS is used inside the CPBPV bounded model checking framework [START_REF] Collavizza | A constraintprogramming framework for bounded program verification[END_REF]. CPBPV FP is the adaptation of CPBPV for generating test cases that hit the suspicious intervals in programs floating-point computations.

The inputs of CPBPV FP are: P , an annotated program; a critical test ct for variable x; [x F , x R ) or (x R , x F ], a suspicious interval for x. Annotations of P specify the range of the input variables of P as well as the suspicious interval for x. The latter assertion is just posted before the critical test ct.

To compute the suspicious interval for x, we approximate the domain of x over the real numbers by [x R , x R ], and over the floating-point numbers by [x F , x F ]. These approximations are computed with rAiCp [16], a hybrid system that combines abstract interpretation and constraint programming techniques in a single static and automatic analysis. The current implementation of rAiCp is based upon the abstract interpreter Fluctuat [START_REF] Delmas | Towards an industrial use of FLUCTUAT on safety-critical avionics software[END_REF], the constraint solver over the reals RealPaver [START_REF] Granvilliers | Algorithm 852: RealPaver: an interval solver using constraint satisfaction techniques[END_REF] and FPCS. The suspicious intervals for variable

x are denoted [x F , x R ) and (x R , x F ].
CPBPV FP performs first some pre-processing: P is transformed into DSAlike form 4 . If the program contains loops, CPBPV FP unfolds loops k times where k is a user specified constant. Loops are handled in CPBPV and rAiCp with standard unfolding and abstraction techniques 5 . So, there are no more loops in the program when we start the constraint generation process. Standard slicing operations are also performed to reduce the size of the control flow graph.

In a second step, CPBPV FP searches for executable paths reaching ct. For each of these paths, the collected constraints are sent to FPCS, which solves the corresponding constraint systems over the floating point numbers. FPCS returns either a satisfiable instantiation of the input variables of P , or ∅. As said before, FPCS [14, 13, 1, 12] is a constraint solver designed to solve a set of constraints over floating-point numbers without losing any solution. It uses 2Bconsistency along with projection functions adapted to floating-point arithmetic [START_REF] Michel | Exact projection functions for floating-point number constraints[END_REF][START_REF] Botella | Symbolic execution of floating-point computations[END_REF] to filter constraints over the floating-point numbers. FPCS also provides stronger consistencies like kB-consistencies, which allow better filtering results.

The search of solutions in constraint systems over floating numbers is trickier than the standard bisection-based search in constraint systems over intervals of CPBPV FP ends up with one of the following results:

a test case proving that P can produce a suspicious value for x; -a proof that no test case reaching the suspicious interval can be generated: this is the case if the loops in P cannot be unfolded beyond the bound k (See [START_REF] Collavizza | A constraintprogramming framework for bounded program verification[END_REF] for details on bounded unfolding) ; -an inconclusive answer: no test case could be generated but the loops in P could be unfolded beyond the bound k. In other words, the process is incomplete and we cannot conclude whether P may produce a suspicious value.

Preliminary experiments

We experimented with CPBPV FP on six small programs with cancellation and absorption phenomena, two very common pitfalls of floating-point arithmetic.

The benchmarks are listed in the first two columns of table 1. First two benchmarks concern the heron program and the optimized heron program with the suspicious intervals described in the section 1.

Program slope (see Fig. 2) approximates the derivative of the square function f (x) = x 2 at a given point x 0 . More precisely, it computes the slope of a nearby secant line with a finite difference quotient:

f ′ (x 0 ) ≈ f (x0+h)-f (x0-h) 2h
. Over the real numbers, the smaller h is, the more accurate the formula is. For this function, the derivative is given by f ′ (x) = 2x which yields exactly 26 for x = 13. Over the floats, Fluctuat [START_REF] Delmas | Towards an industrial use of FLUCTUAT on safety-critical avionics software[END_REF] approximates the return value of the slope program to the interval [0, 25943] when h ∈ [10 -6 , 10 -3 ] and x 0 = 13.

Program polynomial in Fig. 3 illustrates an absorption phenomenon. It computes the polynomial (a 2 +b+10 -5 ) * c. For input domains a ∈ [10 3 , 10 4 ], b ∈ [0, 1] and c ∈ [10 3 , 10 4 ], the minimum value of the polynomial over the real numbers is equal to 1000000000.01.

simple interpolator and simple square are two benches extracted from [START_REF] Goubault | Robustness analysis of finite precision implementations[END_REF]. The first bench computes an interpolator, affine by sub-intervals while the second is a rewrite of a square root function used in an industrial context.

All experiments were done on an Intel Core 2 Duo at 2.8 GHz with 4 GB of memory running 64-bit Linux. We assume C programs handling IEEE 754 compliant floating-point arithmetic, intended to be compiled with GCC without any optimization option and run on a x86 64 architecture managed by a 64bit Linux operating system. Rounding mode was to the nearest, i.e., where ties round to the nearest even digit in the required position.

Strategies and solvers

We run CPBPV FP with the following search strategies for the FPCS solver:

std: standard prune & bisection-based search used in constraint-systems over intervals : splits the selected variable domain in two domains of equal size; fpc: splits the domain of the selected variable in five intervals:

• Three degenerated intervals containing only a single floating point number: the smallest float l, the largest float r, and the mid-point m; • Two open intervals (l, m) and (m, r); -fp3s: selects 3 degenerated intervals containing only a single floating point number: the smallest float l, the largest float r, and the mid-point m. Hence, fp3s is an incomplete method that might miss some solutions.

For all these strategies, we select first the variables with the largest domain and we perform a 3B-consistency filtering step before starting the splitting process.

We compared CPBPV FP with CBMC [START_REF] Clarke | A tool for checking ANSI-C programs[END_REF] and CDFL [START_REF] Vijay | Numeric bounds analysis with conflict-driven learning[END_REF], two state-of-theart software bounded model checkers based on SAT solvers that are able to deal with floating-point computations. We also run a simple generate & test strategy: the program is run with randomly generated input values and we test whether the result is inside the suspicious interval. The process is stopped as soon as a test case hitting the suspicious interval is found.

Results

Table 1 reports the results for the other strategies and solvers. Since strategy fpc3s is incomplete, we indicate whether a test case was found or not. Column s? specifies whether a test case actually exists. Note that the computation times of CBMC and CDFL include the pre-processing time for generating the constraint systems; the pre-processing time required by CPBPV is around 0.6s but CPBPV is a non-optimised system written in java. Strategy fpc is definitely the most efficient and most robust one on all these benchmarks. Note that CBMC and CDFL could neither handle the initial, nor the optimized version of program heron in a timeout of 20 minutes whereas FPCS found solutions in a reasonable time.

Name

These preliminary results are very encouraging: they show that CPBPV FP is effective for generating test cases for suspicious values outside the range of acceptable values on small programs with classical floating-point errors. More importantly, a strong point of CPBPV FP is definitely its refutation capabilities.

Of course, experiments on more significant benchmarks and on real applications are still necessary to evaluate the full capabilities and limits of CPBPV FP.

Related and further work

The goals of software bounded model checkers based on SAT solvers are close to our approach. The point is that SAT solvers tend to be inefficient on these problems due to the size of the domains of floating-point variables and the cost of bit-vector operations [START_REF] Vijay | Numeric bounds analysis with conflict-driven learning[END_REF]. CDFL [START_REF] Vijay | Numeric bounds analysis with conflict-driven learning[END_REF] tries to address this issue by embedding an abstract domain in the conflict driven clause learning algorithm of a SAT solver. SAT solvers often use bitwise representations of numerical operations, which may be very expensive (e.g., thousands of variables for one equation in CDFL). Brain and al [START_REF] Haller | Deciding floating-point logic with systematic abstraction[END_REF][START_REF] Brain | Interpolation-based verification of floating-point programs with abstract cdcl[END_REF] have recently introduced a bit-precise decision procedure for the theory of floating-point arithmetic. The core of their approach is a generalization of the conflict-driven clause-learning algorithm used in modern SAT solvers. Their technique is significantly faster than a bit-vector encoding approach. Note that the constraint programming techniques used in our approach are better suited to generate several test cases than these SAT-based approaches. The advantage of CP is that it provides a uniform framework for representing and handling integers, real numbers and floats. A new abstract-interpretation based robustness analysis of finite precision implementations has recently been proposed [START_REF] Goubault | Robustness analysis of finite precision implementations[END_REF] for sound rounding error propagation in a given path in presence of unstable tests.

A close connection between our floating-point solvers and the two abovementioned approaches is certainly worth exploring.

A second direction for further work concerns the integration of our constraintbased approach with new abstract-interpretation based robustness analysis of finite precision implementations for sound rounding error propagation in a given path in presence of unstable tests.

1 3 floatFig. 1 .

 31 Fig. 1. Heron

-a = 5 .

 5 517474, b = 4.7105823, c = 0.8068917, and squared_area equals -1.0000001 • 10 -5 ; a = 7.072597, b = c = 5, and squared_area equals 156.25003.

Fig. 2 .Fig. 3 .

 23 Fig. 2. Approximation of the derivative of x 2 by a slope float polynomial(float a, float b, float c) { float poly = (a*a + b + 1e-5f) * c; return poly; }

Table 1 .

 1 Results of the different solvers and strategies on the benchmarksThe generate & test strategy behaves quite well on programs with only one input variable when a test case exists but it is unable to find any test case for programs with more than one input variable. More precisely, it found a test case in less than 0.008s for the 6 suspicious intervals of program slope and for program simple_interpolator. The generate & test strategy failed to find a test within 180s in all other cases.Of course, this strategy cannot show that there is no test case reaching the suspicious interval; so, it is of little interest here.

			Condition	CDFL CBMC	std	fpc	fpc3s s?
	heron		area < 10 -5	3.874s 0.280s > 180 0.705 0.022 (n) y
			area > 156.25 + 10 -5 > 180s 34.512s 22.323 7.804 0.083 (n) y
	optimized_heron	area < 10 -5	7.618s 0.932s > 180 0.148 0.022 (n) y
			area > 156.25 + 10 -5 > 180s > 180s 8.988 30.477 0.101 (n) n
	slope with	dh < 26.0 -1.0	2.014s 1.548s 0.021 0.012 0.012 (y) y
	h ∈ [10 -6 , 10 -3 ]	dh > 26.0 + 1.0	1.599s 0.653s 0.055 0.011 0.011 (y) y
			dh < 26.0 -10.0	0.715s 1.108s 0.006 0.006 0.007 (n) n
			dh > 26.0 + 10.0	1.025s 1.080s 0.006 0.006 0.006 (n) n
	polynomial	r < 10 9 +	0.170s 0.295s 0.022 0.006 0.006 (y) y
			0.0099999904 -10 -3
	simple_interpolator res < -10 -5	0.296s 0.264s 0.018 0.012 0.012 (y) y
	simple_square	S > 1.453125	--1.079s 0.012 0.012 0.012 (n) n
	5 Discussion
	5.1	Results analysis

That's to say, computations as close as possible to the mathematical semantics of the real numbers; for instance, computations with arbitrary precision or computer algebra systems.

Let's remind that absorption in an addition occurs when adding two numbers of very different order of magnitude, and the result is the value of the biggest number, i.e., when x + y with y = 0 yields x. Cancellation occurs in sa when s is so close to a that the subtraction cancels most of the significant digits of s and a.

Note that even this small tolerance may lead to an exception in statement 9.

DSA stands for Dynamic Single Assignment. In DSA-like form, all variables are assigned exactly once in each execution path

In bounded model checking, k is usually increased until a counter-example is found or until the number of time units is large enough for the application.

⋆ This work was partially supported by ANR COVERIF (ANR-15-CE25-0002)


Qualitative information flow aims at detecting information leaks, whereas the emerging quantitative techniques target the estimation of information leaks. Quantifying information flow in the presence of low inputs is challenging, since the traditional techniques of approximating and counting the reachable states of a program no longer suffice.

This paper proposes an automated quantitative information flow analysis for imperative deterministic programs with low inputs. The approach relies on a novel abstract domain, the cardinal abstraction, in order to compute a precise upper-bound over the maximum leakage of batch-job programs. We prove the soundness of the cardinal abstract domain by relying on the framework of abstract interpretation. We also prove its precision with respect to a flow-sensitive type system for the two-point security lattice.

The Cardinal Abstraction for Quantitative Information Flow Mounir Assaf * Julien Signoles † Éric Totel ‡ Frédéric Tronel ‡

I. INTRODUCTION

Secure information flow is a challenging problem in program analysis. Earlier techniques focus on enforcing qualitative security properties such as non-interference properties [START_REF] Goguen | Security Policies and Security Models[END_REF], [START_REF] Sabelfeld | Language-based information-flow security[END_REF]. Such qualitative techniques aim at detecting and avoiding information leaks by relying, for instance, on type systems [START_REF] Volpano | A Sound Type System for Secure Flow Analysis[END_REF], [START_REF] Hunt | On flow-sensitive security types[END_REF], [START_REF]From Exponential to Polynomial-Time Security Typing via Principal Types[END_REF], program logic [START_REF] Darvas | A Theorem Proving Approach to Analysis of Secure Information Flow[END_REF], [START_REF] Barthe | Secure information flow by self-composition[END_REF], [START_REF] Unno | Combining type-based analysis and model checking for finding counterexamples against noninterference[END_REF] or monitoring [START_REF] Le Guernic | Automatabased confidentiality monitoring[END_REF], [START_REF] Russo | Dynamic vs. Static Flow-Sensitive Security Analysis[END_REF].

Motivated by the observation that many programs cannot comply with strict security policies preventing information leaks, recent works propose to address the secure information flow challenges by relying on Quantitative Information Flow (QIF). These quantitative techniques propose to measure the amount of leaked information in order to decide whether it is tolerable.

Traditionally, the QIF literature defines the leakage of a program as the difference between an initial uncertainty about the secret prior to any program run, and the remaining uncertainty after attackers observe the outputs of a program: leakage = initial uncertaintyremaining uncertainty.

Denning [START_REF] Denning | Cryptography and data security[END_REF]Chapter 5] proposes the first quantitative measure of a program's leakage in terms of Shannon entropy [START_REF] Shannon | A Mathematical Theory of Communication[END_REF]. Clark et al. [START_REF] Clark | Quantitative Analysis of the Leakage of Confidential Data[END_REF] builds on Denning's work to characterize both the initial uncertainty and the remaining one in terms of Shannon entropy and conditional entropy, then defines the information leakage as the reduction of uncertainty about the secret. Clarkson et al. [START_REF] Clarkson | Belief in information flow[END_REF], [START_REF]Quantifying information flow with beliefs[END_REF] propose to define the leakage as a change in accuracy, rather than uncertainty, by defining an initial and remaining accuracy in terms of information belief [START_REF] Halpern | Reasoning about uncertainty[END_REF]. In a different approach, Smith [START_REF] Smith | On the foundations of quantitative information flow[END_REF], [START_REF]Quantifying information flow using min-entropy[END_REF] proposes to quantify information leaks wrt. min-entropy [START_REF] Rényi | On measures of entropy and information[END_REF], that is the probability of attackers guessing the secret in one try. Smith then defines both the initial uncertainty and the remaining uncertainty in terms of the probability of attackers guessing the secret.

Since both the initial uncertainty and the remaining uncertainty depend on the initial probability distribution of the secret, Denning relies on capacity -the maximum leakage measured through Shannon entropy over all distributions of the secret -, to abstract away from the assumed distribution of the secret. Similarly, Smith also relies on min-capacity, that is the maximum leakage measured through min-entropy over all distributions of the secret. Additionally, Smith [START_REF] Smith | On the foundations of quantitative information flow[END_REF], [START_REF]Quantifying information flow using min-entropy[END_REF] proves that for deterministic programs, capacity and mincapacity coincide, and they are given by the logarithm of the cardinal number of outputs a program may produce:

ML = log 2 |outputs|.
Smith's framework considers a program as a channel that accepts only high inputs. Therefore, a program c that accepts low inputs can be seen as inducing a family of channels accepting only high inputs, and the maximum leakage of c can be defined as the maximum leakage over all induced channels. Therefore, by assuming the input memories are partitioned into low input memories L0 ∈ Σ L0 and high input memories H0 ∈ Σ H0 , the maximum leakage for programs accepting both low and high inputs is given by:

ML = max L 0 ∈Σ L 0 log 2 outputs L 0 . (1)
Let us consider a command c that outputs no intermediate steps of computation. Let us also assume a set of variables v 1 ,v 2 ,...v f attackers can observe at the end of command c's execution. Thus, the outputs attackers may observe are solely determined by the final environments resulting from the execution of command c: outputs L 0 = {( (v 1 ), (v 2 ) . . . , (v f )) | ∃ H0 ∈ Σ H0 , 0 ( L0 , H0 ) and c 0 = }.

(2)

Therefore, computing the maximum leakage for deterministic batch-job programs requires maximizing the cardinality of the set introduced in Equation ( 2), over all low input memories L0 .

Most existing QIF analyses tackle this problem by reducing it to a reachability problem on a self-composed program [START_REF] Barthe | Secure information flow by self-composition[END_REF], [START_REF] Darvas | A Theorem Proving Approach to Analysis of Secure Information Flow[END_REF], [START_REF] Unno | Combining type-based analysis and model checking for finding counterexamples against noninterference[END_REF], [START_REF] Barthe | Secure information flow by self-composition[END_REF]. Indeed, recent techniques [START_REF] Backes | Automatic discovery and quantification of information leaks[END_REF], [START_REF] Heusser | Applied Quantitative Information Flow and Statistical Databases[END_REF], [START_REF] Klebanov | Precise quantitative information flow analysis -a symbolic approach[END_REF] rely on software model checkers [START_REF] Henzinger | Abstractions from proofs[END_REF], [START_REF] Ball | Automatic predicate abstraction of C programs[END_REF], [START_REF] Clarke | A Tool for Checking ANSI-C Programs[END_REF] in order to find symbolic witnesses of an information leak, namely two low equivalent memories that deliver different observable outputs. Since for deterministic programs, each observable output induces an equivalence class over low equivalent input memories that are indistinguishable for that output, these approaches compute the maximum leakage by synthesising and enumerating the number of all such symbolic witnesses. Köpf and Rybalchenko [START_REF] Köpf | Automation of Quantitative Information-Flow Analysis[END_REF] note that such an approach is prohibitively hard, and propose approximation-based approaches for QIF. These approaches include relying on a generic abstract interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] analysis in order to upper-bound the leakage of a program by approximating the reachable states of a program. However, observe from Equation (2) that in the presence of low inputs, one needs to approximate a set of sets of reachable states -one set of reachable states for each possible low inputs -, in order to precisely upper-bound the maximum leakage ML. This latter remark means that while we can rely on traditional abstract domains to approximate the set of final reachable states irrespective of the low inputs, such an approach would deliver an imprecise over-approximation of the leakage.

The contributions of this paper include a novel non-relational abstract domain, the cardinal abstraction, for automated QIF. This abstract domain computes directly variety -the cardinal number of values variables may take -in order to upper-bound the maximum leakage of programs accepting both low and high inputs, instead of relying on an underlying reachability analysis. Section II introduces the intuition behind the cardinal abstract domain.

Section III defines the cardinal abstract domain and introduces its abstract semantics, all the while providing intuitive arguments for its soundness. We also characterize in Theorem 1 an upper-bound over the maximum leakage, by relying on the result of the cardinal abstract domain.

The cardinal abstract domain is sound. Section IV sketches this soundness proof, and defines the collecting semantics over a set of sets of reachable states, that is over an abstraction of the more general hyperproperties [START_REF] Clarkson | Hyperproperties[END_REF], [START_REF]Hyperproperties[END_REF]. While such a collecting semantics may be termed as "non-standard" in abstract interpretation, it appears explicitly in [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF]Section 11], and implicitly in [START_REF] Amtoft | Information Flow Analysis in Logical Form[END_REF]Section 3]. We summarize how to build a Galois connection relating our concrete domain to the abstract one. We also gloss over the functional lifting of this abstraction in order to systematically derive the abstract semantics of the cardinal abstraction.

The cardinal abstract domain is also precise. Indeed, while quantitative security properties emerge as an alternative to qualitative properties, it is unclear how existing approximationbased QIF analyses fare wrt. the more robust qualitative analyses. To the best of our knowledge, the cardinal abstraction is the first approximation-based static analysis that provably computes a leakage of zero bits for programs that are "welltyped" by the traditional Hunt and Sands' [START_REF] Hunt | On flow-sensitive security types[END_REF], [START_REF]From Exponential to Polynomial-Time Security Typing via Principal Types[END_REF] flow-sensitive type system. Section V proves that the results of the cardinal abstract domain can be abstracted furthermore to yield a security labelling of variables that is at least as precise as the labelling obtained by Hunt and Sands' flow-sensitive type system for the two-point lattice. Thus, the cardinal abstraction provides an alternative to the above-mentioned flow-sensitive type system for proving non-interference, while providing additional quantitative information to guide declassification when needed.

Section VI introduces related work and Section VII concludes.

An appendix, providing detailed proofs for all results, can be found at the end of this technical report.

II. OVERVIEW

The cardinal abstraction over-approximates variety directly, that is the cardinal number of values variables may take, in order to upper-bound the maximum leakage.

a) Towards the cardinal abstraction: Consider for instance the program in Listing 1, where variable s is a high input, whereas variables input and x are low inputs. We assume these variables are integers of finite size κ, covering the range [-2 κ-1 , 2 κ-1 -1]. Let us assume that only variable x is a low output observable by attackers. Thus, the maximum leakage for this program is given by ML = log 2 (2) = 1 bit, which accounts for the intuition that only the parity bit of the secret leaks to attackers.

0 // {s → 2 κ , input → 1, x → 1} 1 x := s mod 2; // {s → 2 κ , input → 1, x → 2} 2 x := x + input; // {s → 2 κ , input → 1, x → 2} Listing 1. A

program accepting both low and high inputs

In order to analyse the program in Listing 1, let us focus only on computing variety. Such an abstraction enables the computation of an over-approximation of the maximum leakage directly.

We annotate Listing 1 with the results of an analysis computing only variety. Equation (2) requires us to compute the variety for a fixed arbitrary low input, while the secret ranges throughout all possible values in [-2 κ-1 , 2 κ-1 -1]. Therefore, our analysis initially maps variable s to a cardinal number of 2 κ values, whereas it maps both variables s and x to a cardinal number of 1 value. Assuming attackers only observe variable x, we can deduce that they make at most 2 different observations for each low input, at the end of the program. Thus, we can also deduce that the maximum leakage of the program in Listing 1 is at most 1 bit. In this example, the analysis in Listing 1 is precise: it computes a tight upper-bound over the maximum leakage. Yet, abstract interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] in general may incur a loss of precision, depending on the underlying approximate representations.

In fact, an analysis that only keeps track of variety will lose precision whenever it encounters a conditional instruction. Consider for instance the program in Listing 2 that is annotated with an analysis that only tracks variety. Let us assume that variable secret is a high input, whereas variable input is a low input. At both Lines 2 and 5, the analysis determines that variable x has only one possible value since it is assigned a constant. However, how many values can variable x have at the merge point of the conditional at Line 6?

Unlike abstract domains aiming at approximating trace properties, the cardinal abstraction cannot simply compute the union of both abstract states at the merge point of the conditional, since this would be unsound: with max as a union operator over the lattice ([0, 2 κ ], ≤, 0, 2 κ , max, min) of natural numbers, the analysis would find that variable x has at most 1 value, which is obviously not sound. Instead, the cardinal abstraction must add both abstract values for variable x, in order to soundly deduce that variable x has at most 2 different values at the merge point of the conditional at Line 6. Note also that providing the set [0, 2 κ ] with the addition operator as a join operator cannot define a proper lattice structure, since addition is not idempotent. Similarly, variable input also has 1 possible value in each branch of the conditional. Therefore, without any additional information, the analysis must treat variable input the same way it treats variable x, and must deduce that variable input has at most 2 different values at the merge point of the conditional at Line 6. In order to retain precision for variable input, the analysis must know that variable input is not modified inside the conditional branches -otherwise, the abstract value of variable input will increase whenever the analysis encounters a branching instruction. We achieve this by letting the cardinal abstraction track both the cardinal number of values variables may take, and the program points where variables may have been last assigned. We denote by pp k the program point of the command at Line k. Unlike the previous analysis in Listing 2, the cardinal abstraction retains some precision for variables that are not modified inside conditional branches. As a result, the cardinal abstraction is able to determine that, at Line 6, variable input does indeed have only 1 possible value, whereas variable x has 2 possible values.

// {secret → 2 κ , input → 1, x → 1} if (secret > input){ x := 0; // {secret → 2 κ , input → 1, x → 1} } else { x := 1; // {secret → 2 κ , input → 1, x → 1} } // {secret → 2 κ , input → 2, x → 2}
// {secret → ({pp 0 }, 2 κ ), input → ({pp 0 }, 1), x → ({pp 0 }, 1)} if (secret > input){ x := 0;// {secret → ({pp 0 }, 2 κ ), input → ({pp 0 }, 1), x → ({pp 2 }, 1)} } else { x := 1;// {secret → ({pp 0 }, 2 κ ), input → ({pp 0 }, 1), x → ({pp 5 }, 1)} } // {secret → ({pp 0 }, 2 κ ), input → ({pp 0 },
| pp id := a (assignment) | c 1 ; c 2 (sequence) | pp if (a) c 1 else c 2 (conditional) | pp while (a) c (loop)

A. Abstract Domain

The cardinal abstract domain computes an overapproximation of variety, namely the cardinal number of values variables may take when attackers provide an arbitrary low input memory.

We assume that the set of variables of analysed programs are partitioned into low and high inputs. All variables may cover the range [-2 κ-1 , 2 κ-1 -1] of integers. Therefore, initially at program point pp 0 , low input variables have only 1 possible value, whereas high input variables have 2 κ possible values as illustrated by Listing 3 for the program point pp 0 .

Definition 1 introduces the cardinal abstract domain. Abstract values are pairs of a set s pp ⊆ P of program points and a cardinal number n ∈ [0, 2 κ ]. The resulting lattice is actually the cartesian product of 2 lattices:

1) the set P (P) of all subsets of P, ordered via set inclusion ⊆, with set union ∪ as a join operator and set intersection ∩ as a meet operator, as well as 2) the set of natural numbers [0, 2 κ ], ordered via the natural order ≤ over integers, with max as a join operator and min as a meet operator.

Definition 1 (Cardinal abstract domain).

The cardinal abstract domain is defined as the lattice

(D C , ⊆ ⊗ , (∅, 0), (P, 2 κ ), ∪ ⊗ , ∩ ⊗
where:

D C P (P) × [0, 2 κ ] ⊆ ⊗ ⊆ × ≤ ∪ ⊗ ∪ × max ∩ ⊗ ∩ × min
Our analysis maps each variable id to a pair of a set s pp of program points and a cardinal number n. The set s pp represents the program points where variable id may have been last assigned, whereas n represents the cardinal number of values variable id may take.

B. Abstract Semantics of Expressions

We denote by ∈ V ar D C an abstract environment that maps each variable id to an abstract value (s pp , n) ∈ D C . We also denote by proj i () the projection onto the ith component of a pair (i = 1, 2). Figure 2 introduces the abstract semantics of expressions The abstract semantics of expressions A evaluates an expression a in an abstract environment , in order to yield a cardinal n ∈ [0, 2 κ ] representing the cardinal number of values expression a may evaluate to. Constant expressions always evaluate to a single value. Binary arithmetic operations a 1 bop a 2 yield at most the product of the cardinal of a 1 and the cardinal of a 2 , or 2 κ when this product overflows. Comparison operations a 1 cmp a 2 evaluate to at most 2 different values (true or false), and only 1 when both a 1 and a 2 evaluate to only one possible value.

A ∈ Exp → (V ar D C ) → [0, 2 κ ]. A n = 1 A id = proj 2 ( (id)) A a 1 bop a 2 = min A a 1 × A a 2 , 2 κ A a 1 mod n = min A a 1 , n A a 1 cmp a 2 = min A a 1 × A a 2 , 2
In the case where the second argument of the modulo binary operator is a literal, the cardinal abstraction tries to be more precise. Indeed, the modulo operation a 1 mod n produces at most n different values or A a 1 different values when a 1 may take less than n values.

One advantage of formalizing our analysis as an abstract interpretation approach is the possibility of refining the precision of our analysis by relying on extent abstract domains [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF], [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF], [START_REF] Mauborgne | Trace partitioning in abstract interpretation based static analyzers[END_REF], [START_REF] Miné | The octagon abstract domain[END_REF], [START_REF]Symbolic Methods to Enhance the Precision of Numerical Abstract Domains[END_REF], [START_REF] Cousot | Combination of Abstractions in the ASTR ÉE Static Analyzer[END_REF]. For instance, if a numerical abstraction determines that an expression a 2 has a maximum value of 10 for instance, then the cardinal abstraction can soundly conclude that expression a 1 mod a 2 may evaluate to at most 10 different values or A a 1 different values when a 1 may take less than 10 values. The process of combining different abstract domains in order to refine the precision of an abstraction is called a reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF]. In general, relying on reduced products using traditional abstract domains can refine most of the cardinal abstract domain definitions. Commands pp skip do not modify input abstract environments. Assignments pp id := a map the abstract value ({pp}, A a ) to variable id since id can take as many values as expression a, and is assigned at program point pp. A sequence of commands c 1 ; c 2 composes the abstract semantics of the second command c 2 with the abstract semantics of the first one c 1 .

C. Abstract Semantics of Commands

Recall that the cardinal abstract domain computes the cardinal number of values variables may take, when attackers provide an arbitrary low input memory. Recall also that we assume a partition of the set of variables into low and high input variables, so that all variables are initialized at the initial program point pp 0 . Therefore, initially at the entry program point pp 0 , low input variables have only 1 possible value. On the opposite, high input variables range over the interval [-2 κ-1 , 2 κ-1 -1] of integers. Therefore, high input variables have 2 κ possible values at the entry program point pp 0 .

When the cardinal abstraction determines that a variable id has at most 1 possible value, it also implicitly determines that variable id may only depend on low input variables. Indeed, if variable id depended on high input memories, then there would exist two low equivalent input memories that yield two different values for variable id. Therefore, the cardinal abstraction would determine that variable id has a cardinal number of values greater or equal to 2, since it over-approximates the cardinal number of values variables may take, for a fixed arbitrary low input. This remark will shortly prove useful when defining the abstract semantics of conditionals.

a) Conditional instructions: The abstract semantics of conditional commands considers two different cases depending on the abstract value of the conditional guard.

First, if the conditional guard has only one possible value, then it may only depend on low inputs. Hence, the concrete evaluation of the conditional always executes the same conditional branch for each fixed low input. Therefore, the join operator ∪ ⊗ lifted over environments soundly over-approximates the semantics of conditionals, by computing the set union over the set of program points where each variable may be last assigned, as well as the maximum cardinal over both branches for each variable. Indeed, if a variable id can take at most n 1 values (resp. n 2 values) in the 'then' branch (resp. the 'else' branch), and assuming low inputs are fixed, the cardinal abstract domain soundly concludes that variable id can take at most max(n 1 , n 2 ) values after the conditional.

Second, if the conditional guard has more than one value, then it may depend on high inputs. Hence, the concrete evaluation of the conditional may execute both conditional branches for each fixed low input. Assuming that variable id can have at most n 1 values (resp. n 2 values) in the 'then' branch (resp. the 'else' branch), the cardinal abstract domain may soundly conclude that variable id can take at most n 1 +n 2 values after the conditional, or 2 k values if the latter sum overflows. However, the abstract semantics uses the operator ∪ add(c1,c2) to retain precision for the variables V that are assigned neither in c 1 nor in c 2 , by computing the join ∪ ⊗ over their abstract values. Therefore, for variables V , the cardinal abstract domain simply computes the set union over sets of program points, where these variables may be last assigned, and the maximum over both their cardinals.

In order to determine which variables may be modified within an instruction c, the cardinal abstract domain relies on the set of program points where variables may be last assigned as well as the operator P P (c), that we define as the set of program points appearing in command c. Hence, instruction c does not modify variable id if P P (c) ∩ s pp = ∅, supposing s pp over-approximates the set of program points where id may be last assigned. Note that this condition is only a sufficient one since s pp is an over-approximation of the set of program points where variable id may be last assigned.

pp skip pp id := a [id → ({pp}, A a )] c 1 ; c 2 c 2 ( c 1 ) pp if (a) c 1 else c 2 let n = A a in let 1 = c 1 in let 2 = c 2 in λid. 1 (id) ∪ ⊗ 2 (id) if n = 1 1 (id) ∪ add(c1,c2) 2 (id) otherwise pp while (a) c let F λ . 0 ∪⊗ pp if (a) c else pp skip in lfp ⊆⊗ F (s pp , n) ∪ add(c1,c2) (s pp , n ) (s pp , n) ∪ ⊗ (s pp , n ) if P P (c 1 ; c 2 ) ∩ (s pp ∪ s pp ) = ∅ s pp ∪ s pp , min(n + n , 2 κ
In general, abstract domains retain precision in conditional branches by relying on the conditional guard to reduce the abstract environments entering both the 'then' branch and the 'else' branch. For instance, let us assume that an interval analysis determines that variable x ranges over the interval [0, 9], whereas variable y ranges over the interval [START_REF] Sabelfeld | Language-based information-flow security[END_REF][START_REF]From Exponential to Polynomial-Time Security Typing via Principal Types[END_REF]. Then, in the case of a conditional guard (x == y) testing the equality of variables x and y, the interval analysis can soundly reduce both abstract values mapped to x and y in the 'then' branch to the intersection [2, 5] of both intervals. For simplicity of presentation, the cardinal abstract semantics of conditionals presented in Figure 3 does not attempt to leverage on such reductions. We leave this improvement as future work. b) Loop instructions: Let us denote by ⊆⊗ (resp. by ∪⊗ ) the pointwise lifting of the partial order relation ⊆ ⊗ (resp. of the join operator ∪ ⊗ ) over environments: Partial order:

1 ⊆⊗ 2 ⇐⇒ ∀id, 1 (id) ⊆ ⊗ 2 (id) Join operator:

1 ∪⊗ 2 = λid. 1 (id) ∪ ⊗ 2 (id).
The abstract semantics of loops requires computing an abstract environment that is a loop invariant ⊆⊗ -greater than the initial abstract environment 0 . This loop invariant satisfies the following fixpoint equation:

= 0 ∪⊗ pp if (a) c else pp skip .
Therefore, we can define the abstract semantics of loops as the least fixpoint of F , where F is defined by:

F λ . 0 ∪⊗ pp if (a) c else pp skip .
The least fixpoint of F exists, since F is monotonic and the lattice of abstract environments is complete. Additionally, this least fixpoint can be computed iteratively [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF], [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF] by defining a sequence (x n ) n≥0 as follows:

x 0 = 0 x n+1 = 0 ∪⊗ pp if (a) c else pp skip x n .
The least fixpoint of F is therefore equal to the limit x ∞ of the sequence (x n ) n≥0 .

D. Over-approximating the Maximum Leakage

The cardinal abstract domain computes an overapproximation of the number of values variables may take, when attackers provide a low input memory. Hence, we can upper-bound the cardinal number of outputs attackers may observe when providing an arbitrary low input memory, in order to obtain an over-approximation of the maximum leakage.

Equation (2) characterizes the observations attackers make for batch-job programs c after providing a low input memory as follows :

outputs L 0 = {( (v 1 ), (v 2 ) . . . , (v f )) | ∃ H0 ∈ Σ H0 , 0 ( L0 , H0 ) and c 0 = }. (2)
Recall that we denote by v 1 ,v 2 ,...v f the variables that attackers may observe at the end of the program's execution. Notice also that the partition of variables into low and high outputs may be completely different from the partition of variables into low and high inputs.

Let us denote by R the set of sets of final reachable states for each fixed low input memory, for a batch-job program c:

R

{ | ∃ H0 ∈ Σ H0 , 0 ( L0 , H0 ) and

c 0 = } | L0 ∈ Σ L0 .
Then, we can prove that the maximum cardinal number of outputs attackers may observe, when providing a low input memory, can be over-approximated by relying on the cardinal abstraction. Indeed, assuming that ⇓ is the final abstract environment computed for the program c, the cardinal number of outputs attackers may observe is given by the product of cardinals computed by ⇓ , over all low observable variables v 1 ,v 2 ,...v f :

2 ML = max r∈R |{( (v 1 ), (v 2 ) . . . , (v f )) | ∈ r}|
≤ (by loosing relations in each set r)

max r∈R 1≤i≤f |{ (v i ) | ∈ r}| ≤ (by loosing relations in R) 1≤i≤f max r∈R |{ (v i ) | ∈ r}| ≤ (by soundness of the cardinal abstraction) 1≤i≤f proj 2 ( ⇓ (v i ))
The latter proof yields Theorem 1 which provides an overapproximation of the maximum leakage for batch-job programs by relying on the cardinal abstract domain.

Theorem 1 (Over-approximation of ML for batch-job programs). For deterministic batch-job programs, the maximum leakage ML is upper-bounded by:

ML ≤ log 2   1≤i≤f proj 2 ( ⇓ (v i ))  
where ⇓ denotes the abstract environment computed at the end of the program, and v 1 ,v 2 ,...v f denote the low output variables attackers are allowed to observe.

Note that the proof of Theorem 1 relies on the assumption that the cardinal abstract domain is sound. This same proof sets the stage for the proof of soundness of the cardinal abstraction:

1) define a semantics over a set R of sets of reachable states for each fixed low input memory, then 2) define an abstraction that ignores relations between variables in each set r ∈ R 3) define an abstraction computing the cardinal number of values. Therefore, the next section will sketch a soundness proof of the cardinal abstract domain.

IV. SOUNDNESS

Abstract interpretation generally requires defining a standard semantics for the considered language, describing the result of executing a command over a concrete environment. Then, abstract interpretation focuses on defining a collecting semantics [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] describing the details that are relevant to the properties of interest. These properties are in general not computable. Therefore, abstract interpretation frameworks introduce abstract representations aimed at approximating them. Finally, by linking the properties of interest to the abstract representations through a Galois connection, a sound abstract semantics can be systematically [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF] derived in order to tractably compute approximations of the properties of interest.

The denotational semantics of the While language of Figure 1 is fairly standard. Thus, we omit it for concision. We make explicit only the denotational semantics of assignments. Indeed, since the cardinal abstract domain tracks the set of program points where variables may have been last assigned, we instrument the denotational semantics for assignments in order to track these program points as well:

pp id := a = [id → (pp, A a )]
Therefore, concrete environments ∈ V ar P × V map a variable id to a pair of a program point pp ∈ P and an integer value v ∈ V of size κ. The denotation c yields an environment . Additionally, we also denote by A a the evaluation of an expression a in an environment , that yields a value v ∈ V. Notice that the instrumentation of assignments to track the program points where variables are last assigned does not modify the semantics over values. An erasure of the program points yields the standard denotational semantics of a While language [START_REF] Winskel | The formal semantics of programming languages: an introduction[END_REF].

A. Collecting Semantics

The choice of a collecting semantics depends on the problem of interest. Indeed, a collecting semantics must at least describe program behaviours that are relevant. Ideally, the collecting semantics should also abstract away from the details that are not relevant to the studied problem. Therefore, how should we define the collecting semantics to prove the soundness of the cardinal abstraction?

To answer this question intuitively, let us assume the simpler case of an abstract memory m {x → 2} determining that a variable x may take at most 2 different values. What would be the concrete memories m ∈ V ar V that are represented by m ? Since variable x may take at most 2 different values, the possible values x may take are given by a set of sets of values v ∈ V:

{V ∈ P (V) : |V | ≤ 2} ∈ P (P (V)) .
Therefore, the concrete memories represented by m are also given by a set R ∈ P (P (V ar V)) of sets of memories m ∈ V ar V:

R = r ∈ P (V ar V) : |{m(x) : m ∈ r}| ≤ 2 .
Intuitively, in each set r of memories, the memories m ∈ r map a variable x to at most 2 different values. Thus, we are going to define the collecting semantics over a set of sets of environments. Interestingly, if we consider a program c that accepts both low and high inputs, such a collecting semantics also enables us to describe the set of sets of final reachable states, one set of final reachable states for each low input memory, in accordance with Equations ( 1) and (2). Such structures implying an additional level of sets over environments naturally arise when dealing with security policies such as information flow policies. Indeed, Clarkson and Schneider [START_REF] Clarkson | Hyperproperties[END_REF], [START_REF]Hyperproperties[END_REF] note that important classes of security policies are best described by hyperproperties which they define as sets of legal sets of traces -legal wrt. a security policy -, in contrast to properties that are defined as sets of legal traces.

a) Forward collecting semantics of commands: Equation (3) defines the forward collecting semantics for commands. This collecting semantics computes the set R of sets of final reachable environments when a command c is executed over a set R of sets of initial environments.

c c ∈ P (P (V ar P × V)) → P (P (V ar P × V)) c c R {{ c | ∈ r} | r ∈ R}. (3)
Notice that our collecting semantics c c is defined over an abstraction of hyperproperties. Indeed, Clarkson and Schneider [START_REF] Clarkson | Hyperproperties[END_REF], [START_REF]Hyperproperties[END_REF] define a hyperproperty as a set of sets of traces, where each trace is a sequence of states. They also define a relational hyperproperty as a set of sets of relational traces, where each relational trace is a pair of an initial state and a final state. Relational hyperproperties are an abstraction of the more general hyperproperties, since they forget about the intermediate states and keep only the initial and final states. Similarly, our set of sets of reachable states abstracts relational hyperproperties, by forgetting about the initial states and keeping only the final states. One can also compose an element-wise abstraction [START_REF] Midtgaard | A Calculational Approach to Control-Flow Analysis by Abstract Interpretation[END_REF] with the reachability abstraction [START_REF] Bertrane | Static Analysis and Verification of Aerospace Software by Abstract Interpretation[END_REF] in order to directly abstract a hyperproperty into a set of sets of reachable states.

Cousot and Cousot [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF]Section 11] stress down that the notion of a collecting semantics "is relative to a set of questions. It defines exactly which questions can be answered about programs". They also define a collecting semantics over a set of sets of states, similar to the one we define in Equation (3), while observing that this collecting semantics is more general than the basic collecting semantics defined over a set of states. Such a collecting semantics with an additional level of sets also implicitly appears in Amtoft and Banerjee's [32, Section 3] work, since the Galois connection they introduce relates a set of sets of relational traces to their abstract domain computing independences between variables.

b) Forward collecting semantics of expressions: Similarly to Equation (3), Equation (4) defines the forward collecting semantics for expressions over a set of sets of environments. This semantics then yields a set of sets of values v ∈ V.

A c a ∈ P (P (V ar P × V)) → P (P (V))

A c a R {{A a | ∈ r} | r ∈ R} . (4)

B. Sketch of the Soundness Proof

Once we define a collecting semantics for commands, we need to construct a Galois connection that relates the lattice of concrete objects R ∈ P (P (V ar → P × V)) to the lattice of abstract ones ∈ V ar → D C . With such a Galois connection, we can derive [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF] a sound abstract semantics c for commands as well as a sound abstract semantics for expressions A a . For the sake of pedagogical presentation, let us for now postulate the existence of such a Galois connection ( α, γ):

P (P (V ar P × V)) ; ⊆, ∅, P (V ar P × V) , ∪, ∩ ---→ ← --- α γ (5)
V ar P (P) × [0, 2 κ ] ; ⊆⊗ , λx.(∅, 0), λx.(P, 2 κ ), ∪⊗ , ∩⊗ Then, in order to derive a sound abstract semantics for commands, we can consider the functional abstraction α com defined in Equation ( 6), in order to transpose functions c c of the concrete collecting semantics to functions c of the abstract semantics. Note that Equation ( 6) denotes by Env the set V ar P × V of concrete environments, and by Env the set V ar D C of abstract environments.

α com ∈ (P (P (Env)) → P (P (Env)))

→ Env → Env α com ( c c ) α • c c • γ (6)
Finally, note that α com ( c c ) provides the best abstraction of the collecting semantics of commands. However, this abstraction might not be computable in general. Therefore, soundness only requires that the abstract semantics c of commands over-approximates the functional abstraction α com ( c c ) of the collecting semantics:

α com ( c c ) ⊆⊗ c .
Similarly, we also construct a functional abstraction α exp in order to derive a sound abstract semantics for expressions. The functional abstraction α exp transposes functions A c a of the concrete collecting semantics of expressions to functions A a of the abstract semantics of expressions:

α exp ∈ P (P (Env)) → P (P (V)) → Env → [0, 2 κ ] .
Additionally, the abstract semantics of expressions A a is sound if it verifies the following condition:

α exp (A c a ) ≤ A a .
Figure 4 summarizes the steps towards building the Galois connection ( α, γ) assumed in Equation ( 5). We mainly rely on the fact that composing Galois connections yields a new Galois connection. Thus, composing a non-relational abstraction (α r , γ r ) with the pointwise abstraction (α c , γ c ) of values yields the desired Galois connection ( α, γ). The complete details can be found in the appendix.

Theorems 2 and 3 state the soundness of the cardinal abstract domain.

Theorem 2 (Soundness of the abstract semantics A a ). The abstract semantics of expressions in Figure 2 is sound:

α exp (A c a ) ≤ A a .
Theorem 3 (Soundness of the abstract semantics c ). The abstract semantics of commands in Figure 3 is sound:

α com ( c c ) ⊆⊗ c .
Both proofs can be found in the appendix.

P (P (V ar P × V))

P (V ar P (P × V))

V ar P (P (P × V))

α @ γ @ α γ
Non-relational element-wise abstraction [START_REF] Midtgaard | A Calculational Approach to Control-Flow Analysis by Abstract Interpretation[END_REF] Non-relational abstraction [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF] P (P (V ar

P × V)) ; ⊆ ---------→ ← --------- αr α •α @ γr γ @ •γ
V ar P (P (P × V)) ; ⊆ Non-relational abstraction of a set of sets of environments P (P (P × V))

P (P (P)) × P (P (V))

P (P) × [0, 2 κ ] α × • α @× γ @× • γ × α ⊗ γ ⊗

Attribute independent abstraction [43]

Component-wise abstraction [START_REF] Midtgaard | A Calculational Approach to Control-Flow Analysis by Abstract Interpretation[END_REF]

P (P (P × V)) ; ⊆ ------------→ ← ------------ α α⊗•αוα @ × γ γ @ × •γ × •γ ⊗ P (P) × [0, 2 κ ] ; ⊆ ⊗

Abstraction of values

V ar P (P (P × V))

V ar

P (P) × [0, 2 κ ] α c λf.λx.α(f (x)) γ c λf .λx.γ(f (x))
Pointwise abstraction [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF] P (P (V ar V. PRECISION Throughout our developments of the cardinal abstraction, we consider some optimizations in order to enhance the precision of our analysis, while we leave out some others for future work. For instance, the cardinal abstract domain tracks the program points where variables may have been last assigned, in order to improve its precision in the case of branching instructions. However, we leave off optimizations such as reducing abstract environments by relying on conditional guards, or combining the cardinal abstraction with numerical abstract domains [START_REF] Granger | Static analysis of arithmetical congruences[END_REF], [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. These choices are motivated by making the precision of the cardinal abstraction reach a first checkpoint; indeed, the cardinal abstraction is at least as precise as a flow-sensitive type system [START_REF] Hunt | On flow-sensitive security types[END_REF], [START_REF]From Exponential to Polynomial-Time Security Typing via Principal Types[END_REF] for the two point lattice {L, H}; , L, H, , .

P × V)) ; ⊆ --------→ ← -------- α αc•αr γ γr•γc V ar P (P) × [0, 2 κ ] ; ⊆⊗
Intuitively, abstracting further the results of cardinal abstract domain, by mapping variables having a cardinal number of at most 1 to a low security level L and mapping variables having a cardinal number strictly greater than 1 to a high security level H, yields an analysis that is at least as precise as Hunt and Sands' type system.

Let us first introduce an abstraction operator @ LH mapping a cardinal number n to a security label L or H:

@ LH ∈ [0, 2 κ ] → {L, H} @ LH (n) L if n ≤ 1 H otherwise
This abstraction can be lifted to abstract environments through a pointwise abstraction [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF] as well as a projection that forgets about the program points:

α @ LH ∈ (V ar D C ) → (V ar {L, H}) α @ LH ( ) λx.@ LH proj 2 ( (x))
Lemma 1 proves that the abstract semantics of expressions is as precise as the type labelling of expressions. A proof of Lemma 1, by structural induction on expressions, is presented in the appendix.

Lemma 1 (The abstract semantics of expressions is at least as precise as the type labelling of expressions). For all expressions a, for all abstract environments ∈ V ar D C , for all type environments Γ ∈ V ar {L, H}, such that: A a = n and Γ a : t. It holds that:

α @ LH ( ) Γ =⇒ @ LH (n) t
Theorem 4 proves that the abstract semantics of commands is at least as precise as the type labelling of commands. We let the partial order ˙ denote the pointwise lifting of the partial order over security labels to type environments. A proof of Theorem 4 is presented in the appendix. This proof is by structural induction on commands and relies on Lemma 1.

Theorem 4 (The abstract semantics of commands is at least as precise as the type labelling of commands). For all commands c, for all abstract environments 0 , , and type environments Γ 0 , Γ such that: c 0 = and L Γ 0 {c}Γ.

It holds that:

α @ LH ( 0 ) Γ 0 =⇒ α @ LH ( ) ˙ Γ
The cardinal abstraction is almost exactly as precise as Hunt and Sands flow-sensitive type system. The only case that stands out is the following expression secret mod 1 that we uncovered while trying to prove that the cardinal abstraction is exactly as precise as Hunt and Sands' flow-sensitive type system. Indeed, assuming that variable secret may take more than 2 values, the cardinal abstraction still determines that this expression has at most 1 possible value, whereas the typing judgement for expressions reasons on the free variables of that expression, and labels the expression secret mod 1 as high H. Another corner case is the expression secret mod 0 where the cardinal abstraction determines as having 0 value, which is still sound considering that this expression is undefined. This also warrants one of our design decisions to formalize our analysis as an abstract domain, since we can rely on reduced products [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] to not only enhance the precision of the cardinal abstract domain, but also to prove the absence of runtime errors in analysed programs.

As a direct result of Theorem 4, Corollary 1 states that the cardinal abstraction computes a leakage of zero bits for programs that are "well-typed" by Hunt and Sands' flowsensitive type system. By "well-typed", we mean that the final typing environment computed by the flow-sensitive type system labels as low all output variables v 1 ,v 2 ,...v f that attackers may observe.

Corollary 1 (Zero leakage for well-typed programs). For all commands c, for all abstract environments 0 , , and type environments Γ 0 , Γ such that: c 0 = , and L Γ 0 {c}Γ, and for all i ∈ [1, f ], proj 2 ( (v i )) = 0.

It holds that:

α @ LH ( 0 ) Γ 0 and (∀i ∈ [1, f ], Γ(v i ) = L) =⇒ log 2   1≤i≤f proj 2 ( (v i ))   = 0.
Since the cardinal abstraction is at least as precise as a flowsensitive type system for the two point lattice, it is appealing to rely on this abstract domain even when interested in proving that a program complies with a qualitative security policy such as termination-insensitive non-interference [START_REF] Sabelfeld | Language-based information-flow security[END_REF]. Indeed, in addition to labelling variables as low or high, the cardinal abstraction also provides quantitative information that may assist in making better informed decisions when declassification is necessary.

Unlike Hunt and Sands' [START_REF] Hunt | On flow-sensitive security types[END_REF], [START_REF]From Exponential to Polynomial-Time Security Typing via Principal Types[END_REF] type system, the cardinal abstraction quantifies information flow only for the two-point lattice. Future work includes a generalization of the cardinal abstract domain to handle the case of arbitrary multilevel security lattices.

VI. RELATED WORK

Clark, Hunt and Malacaria [START_REF] Clark | Quantitative Information Flow, Relations and Polymorphic Types[END_REF] build on Denning's [START_REF] Denning | Cryptography and data security[END_REF] work in order to propose a measure of information leakage, based on Shannon entropy [START_REF] Shannon | A Mathematical Theory of Communication[END_REF] and mutual information. In particular, they prove in the deterministic setting that the leakage of a program can be measured by the conditional Shannon entropy of the observable outputs, knowing the public inputs. They also prove that this latter quantity equals zero in the case of a deterministic program iff. the program is noninterferent. Clark et al. [START_REF]A static analysis for quantifying information flow in a simple imperative language[END_REF] also propose a type system to quantify information flow for deterministic batch-job programs with low inputs. They also prove that if attackers can observe non-termination, their analysis under-estimates the leakage by at most one bit. The same argument can be used to prove that the cardinal abstraction also under-estimates the leakage by at most one bit if attackers can observe non-termination. Indeed, the observation of non-termination by attackers can be modelled as an additional observable output ⊥, which means that the upper-bound computed by the cardinal abstraction is under-estimated by at most 1 bit.

Clarkson et al. [START_REF] Clarkson | Belief in information flow[END_REF], [START_REF]Quantifying information flow with beliefs[END_REF] propose a quantitative measure, based on information belief [START_REF] Halpern | Reasoning about uncertainty[END_REF]. This measure reasons on attackers' belief, namely the probability distribution of the confidential input that attackers may assume. Clarkson et al. model how attackers revise their belief after observing outputs of a program. The revised attackers' belief as well as the initial belief provide a way to measure the improvement in the accuracy of attackers' belief. Clarkson et al. also propose to measure this improvement in accuracy by relying on relative entropy [START_REF] Cover | Elements of Information Theory 2nd Edition[END_REF], a pseudo-metric defined over probability distributions.

Smith [START_REF] Smith | On the foundations of quantitative information flow[END_REF] notes that Shannon entropy and mutual information are unsuitable metrics for estimating information flow leakage in particular scenarios. Indeed, Shannon entropy of a random variable can be arbitrarily high despite being highly vulnerable to being guessed in one try [START_REF] Espinoza | Min-entropy as a resource[END_REF]. Smith then proposes the use of min-entropy as a measure for quantifying information flow. This measure estimates the probability that attackers guess the confidential inputs in one try, after observing a program run. Additionally, Smith proves that the maximum leakage over all a priori distributions measured either with min-entropy (namely, min-capacity) or Shannon entropy (namely, capacity) coincide for deterministic programs, and conjecture that min-capacity upper-bounds capacity for probabilistic programs [START_REF]Quantifying information flow using min-entropy[END_REF].

Braun, Chatzikokolakis and Palamidessi [START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF] propose an additive notion of information leakage based on the probability that attackers guess the wrong confidential inputs. They also investigate how to compute supremums for their additive notion as well as for min-entropy [START_REF] Smith | On the foundations of quantitative information flow[END_REF]. Particularly, they prove that the supremum for min-entropy is reached when the confidential inputs are uniformly distributed [START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF], [START_REF]Quantifying information flow using min-entropy[END_REF].

Alvim et al. [START_REF] Alvim | Measuring Information Leakage Using Generalized Gain Functions[END_REF] propose a generalization of min-entropy using gain functions. Gain functions model a variety of scenarios for attackers, such as the advantage attackers gain from guessing part of the secret or making a set of guesses. They also prove in the probabilistic setting that min-capacity is an upper bound on both Shannon capacity and capacity defined using gain functions. Hence, min-capacity offers a way to abstract from a priori distributions of the confidential inputs and to bound various entropy-based information flow metrics. Note however that different quantitative information flow metrics are appropriate for modelling different attacks scenarios [START_REF] Smith | On the foundations of quantitative information flow[END_REF].

Backes, Köpf and Rybalchenko [START_REF] Backes | Automatic discovery and quantification of information leaks[END_REF] propose to synthesize the equivalence classes induced by outputs over low equivalent memories by relying on software model checkers. Their approach characterizes the maximum leakage ML by counting the number of such equivalence classes. Additionally, they also estimate the size of such equivalence classes in order to compute other quantitative information flow metrics such as Shannon entropy [START_REF] Shannon | A Mathematical Theory of Communication[END_REF] and the Guessing entropy [START_REF] Massey | Guessing and entropy[END_REF]. Heusser and Malacaria [START_REF] Heusser | Applied Quantitative Information Flow and Statistical Databases[END_REF] also rely on a similar technique to quantify information flow for database queries. Köpf and Rybalchenko [START_REF] Köpf | Approximation and Randomization for Quantitative Information-Flow Analysis[END_REF] note that the exact computation of information-theoretic characteristics is prohibitively hard, and propose instead to rely on approximation-based analyses.

In particular, Köpf and Rybalchenko [START_REF] Köpf | Approximation and Randomization for Quantitative Information-Flow Analysis[END_REF] rely on both abstract interpretation and model checking to compute overapproximations and under-approximations of the equivalence classes over the low equivalent memories. Therefore, they can compute an upper-bound and a lower-bound over the maximum leakage ML. Additionally, they propose a randomization technique based on sampling in order to bound Shannon entropy [START_REF] Shannon | A Mathematical Theory of Communication[END_REF]. Their abstract interpretation approach relies on over-approximating the set of reachable states, which delivers an imprecise upper-bound of the leakage for programs accepting both low and high inputs. Köpf and Rybalchenko also propose to rely on self-composition [START_REF] Darvas | A Theorem Proving Approach to Analysis of Secure Information Flow[END_REF], [START_REF] Barthe | Secure information flow by self-composition[END_REF], [START_REF] Unno | Combining type-based analysis and model checking for finding counterexamples against noninterference[END_REF], [START_REF] Barthe | Secure information flow by self-composition[END_REF] to model a scenario where attackers may refine their knowledge by influencing the low inputs. Klebanov [START_REF] Klebanov | Precise quantitative information flow analysis -a symbolic approach[END_REF] relies on a similar technique to handle programs with low inputs, and uses two different approaches to quantify information leaks. The first approach computes a functional specification of programs using user-supplied invariants, and the second one relies on selfcomposition to automatically compute the equivalence classes over low input memories. Klebanov also proposes the use of polyhedra to synthesize linear constraints over variables. He then relies on symbolic procedures to compute both the number and size of the equivalent classes over low input memories. However, this approach does not support programs with arbitrary expressions.

VII. CONCLUSION

This paper proposes a novel analysis, the cardinal abstraction, for QIF in batch-job programs. 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 formalize the cardinal abstract domain and prove its soundness.

Unlike previous approaches aimed at QIF, our approach does not rely on an underlying reachability analysis. Instead, the cardinal abstraction approximates variety directly to precisely upper-bound the maximum leakage. We also prove the precision of our analysis by proving that the cardinal abstraction computes a maximum leakage of zero for programs that are "well-typed" wrt. a traditional flow-sensitive type system [START_REF] Hunt | On flow-sensitive security types[END_REF], [START_REF]From Exponential to Polynomial-Time Security Typing via Principal Types[END_REF].

We also propose an implementation of the cardinal abstraction 1 by modifying an existing prototype abstract interpreter 2 for an imperative While language. This implementation enhances the precision of the cardinal abstraction by relying 1 https://github.com/moun/Fhamator 2 http://www.irisa.fr/celtique/teaching/PAS/while analyser.tgz on a reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] of both the cardinal abstract domain and an interval abstract domain [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF]. Indeed, one advantage of formalizing our analysis as an abstract interpretation approach is the possibility of improving its precision by combining it with existing domains [START_REF] Cousot | Combination of Abstractions in the ASTR ÉE Static Analyzer[END_REF], [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF], [START_REF] Mauborgne | Trace partitioning in abstract interpretation based static analyzers[END_REF], [START_REF] Miné | The octagon abstract domain[END_REF], [START_REF]Symbolic Methods to Enhance the Precision of Numerical Abstract Domains[END_REF]. In particular, we plan on building on the cardinal abstraction and Miné's [START_REF]Symbolic Methods to Enhance the Precision of Numerical Abstract Domains[END_REF] previous work in order to enhance the cardinal abstraction with relational constraints, while still supporting arbitrary non-linear expressions.

Future work also includes generalizing the cardinal abstraction for QIF in the case of a multilevel security lattice. By doing so, we also hope to gain more insights towards understanding abstract interpretation-based verification methods for hyperproperties. The cardinal abstraction is but a first step towards that goal. Indeed, we are aware that the bounding problem in QIF the cardinal abstraction targets is not a ksafety property, but a hypersafety [START_REF] Clarkson | Hyperproperties[END_REF], [START_REF]Hyperproperties[END_REF], [START_REF] Yasuoka | On Bounding Problems of Quantitative Information Flow[END_REF], [START_REF]Quantitative Information Flow -Verification Hardness and Possibilities[END_REF], [START_REF]On bounding problems of quantitative information flow[END_REF] one.

Additionally, we would also like to extend our approach to deal with real-world programs. In ongoing work, we are extending the restricted batch-job computation model to a more general one [START_REF] Askarov | Termination-Insensitive Noninterference Leaks More Than Just a Bit[END_REF], and will move from there to target richer programming languages. If we recall the example set R 0 of sets of environments defined in Equation [START_REF] Barthe | Secure information flow by self-composition[END_REF], then α r (R 0 ) ignores all relationships among variables: α r (R 0 ) = x → {(pp 0 , 0)}, {(pp 0 , 1)} ; y → {(pp 0 , 2), (pp 0 , 3)}, {(pp 0 , 4), (pp 0 , 5)} As we have defined a non-relational abstraction (α r , γ r ) over hyperproperties, we can now focus on defining an abstraction over sets of sets of values as shown in Section IV-B. This latter abstraction can then be lifted over environments as illustrated by Section IV-B.

B Abstraction of Values

Similarly to the previous section, where we lift a non-relational abstraction to a set of sets of environments, we can also lift an attribute independent abstraction [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF], that forgets about relationships between components of pairs, to a set of sets of pairs through an element-wise abstraction.

B0a Attribute independent abstraction: The attribute independent abstraction function @ × is given by: @ × ∈ P (P × V) → P (P) × P (V)

@ × (p) (Π 1 (p), Π 2 (p)) Π i (p) {proj i (x) | x ∈ p}
Therefore, we define an element-wise abstraction α @× over a set of sets of pairs as follows:

α @× (P ) {@ × (p) | p ∈ P } = {(Π 1 (p), Π 2 (p)) | p ∈ P } γ @× (Q) {p | @ × (p) ∈ Q}
Therefore, (α @× , γ @× ) defines a Galois connection:

P (P (P × V)) ; ⊆, ∅, P (P × V) , ∪, ∩ -----→ ← ----- α @ ×
γ @ × P (P (P) × P (V)) ; ⊆, ∅, P (P) × P (V) , ∪, ∩

Let us assume that P 0 is a set of sets of pairs defined as follows:

P 0 {(pp 0 , 2), (pp 0 , 3)}, {(pp 0 , 4), (pp 0 , 5)}

Then α @× (P 0 ) is given by: α @× (P 0 ) = ({pp 0 }, {2, 3}), ({pp 0 }, {4, 5})

In this latter set, we can further ignore relationships among values through an additional attribute independent abstraction:

α × (Q) (Π 1 (Q), Π 2 (Q)) γ × ((X, Y )) X × Y
Therefore, we obtain a Galois connection [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF]:

P (P (P) × P (V)) ; ⊆, ∅, P (P) × P (V) , ∪, ∩ ----→ ← ----α× γ× P (P (P)) × P (P (V)) ; ⊆ × , (∅, ∅), P (P) × P (V) , ∪ × , ∩ × [START_REF] Denning | Cryptography and data security[END_REF] with the component-wise ordering, join and meet:

⊆ × ⊆ × ⊆ ∪ × ∪ × ∪ ∩ × ∩ × ∩
For instance, if we recall the example set P 0 defined in Equation ( 10), then α × • α @× (P 0 ) is given by:

α × • α @× (P 0 ) = α × ({pp 0 }, {2, 3}), ({pp 0 }, {4, 5}) = {pp 0 } , {2, 3}, {4, 5} B0b
Component-wise abstraction: Finally, let us assume two Galois connections (α v , γ v ) and (α pp , γ pp ) such that:

P (P (V)) ; ⊆, ∅, P (V) , ∪, ∩ ---→ ←--- αv γv
[0, 2 κ ]; ≤, 0, 2 κ , max, min P (P (P)) ; ⊆, ∅, P (P) , ∪, ∩ ----→ ← ---αpp γpp P (P) ; ⊆, ∅, P, ∪, ∩ Then, a component-wise abstraction [START_REF] Midtgaard | A Calculational Approach to Control-Flow Analysis by Abstract Interpretation[END_REF] (α ⊗ , γ ⊗ ) defined as follows:

α ⊗ (S pp , S v ) α pp (S pp ), α v (S v ) γ ⊗ (s pp , n) γ pp (s pp ), γ v (n)
yields a Galois connection:

P (P (P)) × P (P (V)) ; ⊆ × , (∅, ∅), P (P) × P (V) , ∪ × , ∩ × ----→ ← ---- α⊗ γ⊗ P (P) × [0, 2 κ ] ; ⊆ ⊗ , (∅ × 0), (P × 2 κ ), ∪ ⊗ , ∩ ⊗ (12)
Consequently, the abstraction of values (α, γ) can be defined as the composition of the 3 Galois connections defined previously in Equations ( 9), ( 11) and ( 12):

P (P (P × V)) ; ⊆, ∅, P (P × V) , ∪, ∩ ------------→ ← ------------ α α⊗•αוα @ × γ γ @ × •γ × •γ ⊗ P (P) × [0, 2 κ ] ; ⊆ ⊗ , (∅, 0), (P, 2 κ ), ∪ ⊗ , ∩ ⊗ (13)
Let us focus now on defining both Galois connections (α v , γ v ) and (α pp , γ pp ).

B0c Abstraction of program points: The abstraction α pp merges all the sets of program points:

α pp (S pp ) s∈Spp s γ pp (s pp ) P (s pp )
Therefore, we obtain a Galois connection:

(P (P (P)) ; ⊆, ∅, P (P) , ∪, ∩) ----→ ← ---αpp γpp (P (P) ; ⊆, ∅, P, ∪, ∩)

Indeed, let us prove that (α pp , γ pp ) is a Galois connection:

α pp (S) ⊆ s pp ⇐⇒ s∈S s ⊆ s pp ⇐⇒ ∀s ∈ S, s ∈ P (s pp ) ⇐⇒ S ⊆ P (s pp ) ⇐⇒ S ⊆ γ pp (s pp )
B0d Abstraction of concrete values: The abstraction α v computes the maximum cardinal of values over the sets s v ∈ S v :

α v (S v ) max sv∈Sv |s v | γ v (n) = {V ∈ P (V) | |V | ≤ n}
Therefore, (α v , γ v ) is a Galois connection:

P (P (V)) ; ⊆, ∅, P (V) , ∪, ∩ ---→ ←--- αv γv [0, 2 κ ]; ≤, 0, 2 κ , max, min
Indeed, let us prove that (α v , γ v ) is a Galois connection:

α v (S v ) ≤ n ⇐⇒ max sv∈Sv |s v | ≤ n ⇐⇒ ∀s v ∈ S v , s v ∈ P n (V) ⇐⇒ S v ⊆ γ v (n)

C Abstraction of Environments

As illustrated by Section IV-B, the abstraction (α, γ) of values -defined in Equation ( 13) -can be lifted through a pointwise abstraction [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF], in order to abstract a set valued environment ∈ V ar P (P (P × V)). Indeed, let us define a pointwise abstraction (α c , γ c ) as follows:

α c λf.λx.α f (x) γ c λf .λx.γ f (x)
Then, (α c , γ c ) yields a Galois connection:

V ar P (P (P × V)) ; ⊆, λx.∅, λx.P (P × V) , ∪, ∩ ---→ ←--αc γc

V ar P (P) × [0, 2 κ ] ; ⊆⊗ , λx.(∅, 0), λx.(P, 2 κ ), ∪⊗ , ∩⊗ Therefore, by composing both the non-relational abstraction over environments and the pointwise abstraction of values defined in Equations ( 8) and ( 13), we can build the abstraction ( α, γ):

α α c • α r γ γ r • γ c
Thus, the pair ( α, γ) yields a Galois connection:

P (P (V ar P × V)) ; ⊆, ∅, P (V ar P × V) , ∪, ∩ ---→ ← --- α γ
V ar P (P) × [0, 2 κ ] ; ⊆⊗ , λx.(∅, 0), λx.(P, 2 κ ), ∪⊗ , ∩⊗

As mentioned in Section IV-A, once we construct a Galois connection relating concrete objects to abstract one, we can define functional abstractions in order to soundly approximate functions over concrete objects by functions over abstract ones.

In order to approximate the collecting semantics A c a of expressions, we can define the following functional abstraction [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF]:

α exp ∈ P (P (Env)) → P (P (V)) → Env → [0, 2 κ ] α exp (φ) α v • φ • γ
Therefore, the abstract semantics A a of expressions is sound wrt. the collecting semantics A c a of expressions if:

α exp (A c a ) ≤ A a (15)
Theorem 2 (Soundness of the abstract semantics A a ).

The abstract semantics of expressions in Figure 2 is sound:

α exp (A c a ) ≤ A a .
Let us derive an abstract semantics A a R for expressions:

-Case a = n:

α exp (A c n ) α v • A c n • γ( ) = α v {v ∈ V | ∃ ∈ r, A n = v} | r ∈ γ( ) = α v ({{n}}) = 1 A n -Case a = id: α exp (A c id ) α v • id • γ( ) = α v {v | ∃ ∈
v 1 bop v 2 | ∃ 1 ∈ r 1 , A a 1 1 = v ∧ 2 ∈ r 2 , A a 2 2 = v 2
≤ (values v ∈ V are finite, of size 2 κ ) min 2 κ , max r1,r2∈ γ( )

v 1 | ∃ 1 ∈ r 1 , A a 1 1 = v 1 × v 2 | ∃ 2 ∈ r 2 , A a 2 2 = v 2 = min 2 κ , max r1∈ γ( ) v 1 | ∃ 1 ∈ r 1 , A a 1 1 = v 1 × max r2∈ γ( ) v 2 | ∃ 2 ∈ r 2 , A a 2 2 = v 2
≤ (By induction hypothesis in Equation ( 15))

min 2 κ , A a 1 × A a 2
A a 1 bop a 2

-Case a = a 1 cmp a 2 : this case is similar to the previous case, apart that expression a 1 cmp a 2 may evaluate to only 2 different boolean values. The abstract semantics of commands in Figure 3 is sound:

α com ( c c ) ⊆⊗ c .
Similarly to expressions, we define the functional abstraction α com in order to soundly approximate the collecting semantics c c of commands.

α com ( c c ) ⊆⊗ c (16)
Theorem 3 (Soundness of the abstract semantics c ).

The abstract semantics of commands in Figure 3 is sound:

α com ( c c ) ⊆⊗ c .
Let us derive an abstract semantics for instructions:

-Case c = pp skip: 16))

α com ( pp skip c ) = α • pp skip c • γ( ) = α • γ( ) ⊆ ⊗ ( α • γ is reductive)
c 1 ∪⊗ c 0
Second, if A a > 1, then for variables x that are modified in neither c 1 nor c 0 , we have:

(α com ( c c ) )(x) = c 1 ∪⊗ c 0 (x)
Finally, for variables that are modified in either c 1 or c 0 :

(α com ( c c ) )(x) = α { | ∃ ∈ r, ∃v ∈ {0, 1}, A a = v ∧ c v = } | r ∈ γ( ) (x) = α { | ∃ ∈ r, A a = 1 ∧ c 1 = } ∪ { | ∃ ∈ r, A a = 0 ∧ c 0 = } (x) ⊆ ⊗ α { | ∃ ∈ r 2 , A a = 1 ∧ c 1 = } ∪ { | ∃ ∈ r 1 , A a = 0 ∧ c 0 = } | r 1 , r 2 ∈ γ( ) (x) ⊆ ⊗ α { | ∈ r 1 } ∪ { | ∈ r 2 } | r 1 ∈ c 1 c • γ( ),
r 2 ∈ c 0 c • γ( ) (x)
⊆ ⊗ ( γ • α is extensive, and α is monotone)

α { | ∈ r 1 } ∪ { | ∈ r 2 } | r 1 ∈ γ • α • c 1 c • γ( ),
r 2 ∈ γ • α • c 0 c • γ( ) (x)
⊆ ⊗ (By hypothesis in Equation ( 16) and monotony of α)

α { | ∈ r 1 } ∪ { | ∈ r 2 } | r 1 ∈ γ( c 1 ), r 2 ∈ γ( c 0 ) (x)
⊆ ⊗ (By definition of ( α, γ))

proj 1 ( c 1 (x)) ∪ proj 1 ( c 0 (x)),

Listing 2 .

 2 An analysis keeping track of only the cardinal number of values b) The cardinal abstraction: Listing 3 annotates the program in Listing 2 with the results of the cardinal abstraction.

Fig. 1 .

 1 Fig. 1. Abstract syntax of While

Fig. 2 .

 2 Fig. 2. Abstract semantics of expressions

Figure 3

 3 Figure 3 introduces the forward abstract semantics of commands. This abstract semantics c ∈ (V ar D C ) → (V ar D C ) evaluates a command c in an abstract environment , then yields a new abstract environment.Commands pp skip do not modify input abstract environments. Assignments pp id := a map the abstract value

Fig. 3 .

 3 Fig. 3. Abstract semantics of commands

Fig. 4 .

 4 Fig. 4. Building the Galois connection ( α, γ)

- 1 ∧ A a 2 = 1 ∧ A a 2 2 =

 1212 r, A id = v} | r ∈ γ( ) = α v {proj 2 ( (id)) | ∃ ∈ r} | r ∈ γ( ) = (By definition of γ) α v • γ v ( (id)) ≤ (α v • γ v is reductive) Case a = a 1 mod n : α exp (A c a ) α v {v 1 mod n | ∃ ∈ r, A a 1 = v 1 } | r ∈ γ( ) = min α v {v 1 | ∃ ∈ r, A a 1 = v 1 } | r ∈ γ( ) , n = min(α v • A c a 1 • γ( ), n) ≤ (By induction hypothesis) min(A a 1 , n) A a 1 mod n -Case a = a 1 bop a 2 : α exp (A c a 1 bop a 2 ) α v ({{v 1 bop v 2 | ∃ ∈ r, A a 1 = v v 2 } | r ∈ γ( )≤ (by loosing relationships among variables in r)α v {v 1 bop v 2 | ∃ 1 ∈ r 1 , ∃ 2 ∈ r 2 , A a 1 1 = v v 2 } | r 1 , r 2 ∈ γ( )= (by definition of α v ) max r1,r2∈ γ( )

α 1 × A a 2 A a 1 cmp a 2 Theorem 3 (

 1223 exp (A c a ) ≤ min 2, A a Soundness of the abstract semantics c ).

α

  com ∈ P (P (Env)) → P (P (Env))→ Env → Env α com ( c c ) α • c c • γTherefore, the abstract semantics of commands c is sound wrt. the collecting semantics c c of commands if:

-= 1 ,

 1 For instruction c = pp id := a:α com (c) = α • pp id := a c • γ( ) = α { | ∃ ∈ r, id := a = } | r ∈ γ( ) = α { [id → (pp, v)] | ∃ ∈ r, A a = v} | r ∈ γ( )Hence, for all x ∈ V ar such that x = id:(α com ( pp id := a c ) )(x) ⊆ ⊗ (x)Additionnally, for x = id:(α com (c) )(id) = r ∈ c c • γ( ) Π 1 (@(r )(id)), max r ∈ c c • γ( ) |Π 2 (@(r )(id))| = {pp}, max r ∈ c c • γ( ) |Π 2 ({ (id) : ∈ r })| = {pp, max r∈ γ( ) |{A a : ∈ r}|} = {pp}, α v • A c a • γ( ) ⊆ ⊗ {pp}, A a Hence, α com ( pp id := a) ⊆ ⊗ [id → (pp, A a )]pp id := a -For conditional instructions c = pp if (a) c 1 else c 0 :α com ( c c ) = α { | ∃ ∈ r, c = } | r ∈ γ( ) = α { : ∃ ∈ r, ∃v ∈ {0, 1}, A a = v ∧ c v = } | r ∈ γ( )First, if A a then expression a evaluates to at most one value in each set r ∈ γ( ):∀r ∈ γ( ), ∃v ∈ {0, 1}, ∀ ∈ r, A a = vTherefore, the sets r ∈ γ( ) can be partitioned into sets r 1 (resp. r 0 ) where expression a evaluates to 1 (resp. evaluates to 0):α com ( c c ) = α { | ∃ ∈ r 1 , c 1 = } | r 1 ∈ γ( ) ∪ { | ∃ ∈ r 0 , c 0 = } | r 0 ∈ γ( ) ⊆⊗ ( α preserves joins) α { | ∃ ∈ r 1 , c 1 = } | r 1 ∈ γ( ) ∪⊗ α { | ∃ ∈ r 0 , c 0 = } | r 0 ∈ γ( ) = α • c 1 c • γ( ) ∪⊗ α • c 0 c • γ( )⊆⊗ (by induction hypothesis Equation (

proj 2 ( c 1 1 1 1 = 2 } : r 1 ∈ γ c 1 } ⊆⊗ c 2 c 1 -

 1112111 (x)) + proj 2 ( c 0 (x))Hence, the abstract semantics of conditionals is sound:pp if (a) c 1 else c 2 let n = A a in let 1 = c 1 in let 2 = c 2 in λid. 1 (id) ∪ ⊗ 2 (id) if n = (id) ∪ add(c1,c2) 2 (id) otherwise -For sequences c 1 ; c 2 : α com (c 1 ; c 2 ) = α {{ 2 : ∃ ∈ r, c 1 ; c 2 = 2 } : r ∈ γ( )} = α {{ 2 : ∃ 1 ∈ r 1 , c 2 1 = 2 } : r 1 ∈ c 1 c γ( )} ⊆⊗ α {{ 2 : ∃ 1 ∈ r 1 , c 2 1 = 2 } : r 1 ∈ γ • α c 1 c γ( ) } ⊆⊗ α {{ 2 : ∃ 1 ∈ r 1 ,c 2 For while loops pp while (a) c: α com ( pp while (a) c) = α • pp while (a) c c • γ( ) = (By characterizing the collecting semantics for loops as a least fixpoint with F X0 = λX.X 0 ∪ pp if (a) c else pp skip c ) α lfp ⊆ γ( ) F ⊆⊗ (By the fixpoint transfer theorem) lfp ⊆⊗ pp if (a) c else pp skip

APPENDIX

This section builds the Galois connection assumed in Equation ( 5): P (P (V ar P × V)) ; ⊆, ∅, P (V ar P × V) , ∪, ∩ ---→ ← --α γ

V ar P (P) × [0, 2 κ ] ; ⊆⊗ , λx.(∅, 0), λx.(P, 2 κ ), ∪⊗ , ∩⊗

The steps towards building such a Galois connection are summarized in Figure 4.

A Non-relational Abstraction of Environments

The cardinal abstraction is a non-relational abstraction. Thus, we start by defining a first Galois connection that ignores the relationships among variables.

In the case of environment properties, the following abstraction function [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF] ignores relations between variables: @ ∈ P (V ar P × V) → (V ar P (P × V))

Since our collecting semantics is defined over hyperproperties -sets of environment properties -, we lift the previous abstraction @ over sets of properties through an element-wise abstraction [START_REF] Midtgaard | A Calculational Approach to Control-Flow Analysis by Abstract Interpretation[END_REF] denoted by α @ :

Therefore, we obtain a Galois connection:

The abstraction α @ only forgets relationships among variable in each set r ∈ R of environments. For instance, let us assume a set R 0 of sets of environments defined as:

{[x → (pp 0 , 1); y → (pp 0 , 4)], [x → (pp 0 , 1); y → (pp 0 , 5)]} Then, the abstraction α @ (R 0 ) yields:

[x → {(pp 0 , 1)}; y → {(pp 0 , 4), (pp 0 , 5)}]

In this latter set, we can further ignore relationships among variables through an additional non-relational abstraction:

Therefore, (α , γ ) yields a Galois connection [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF]:

V ar P (P (P × V)) ; ⊆, λx.∅, λx.P (P × V) , ∪, ∩ Since composing Galois connections yields a Galois connection, we define (α r , γ r ) (α • α @ , γ • γ @ ) to obtain a non-relational abstraction over hyperproperties:

We prove that the cardinal abstraction refines a flow-sensitive type system labelling variables as either low or high.

Let us first introduce an abstraction mapping a cardinal number n to a security label L or H:

Let us consider a flow-sensitive type system such as the one presented in [START_REF]From Exponential to Polynomial-Time Security Typing via Principal Types[END_REF]. Such a type system considers a type environment Γ ∈ V ar {L, H} as well as a security label pc. Let us denote by the join operator over security labels, and by the partial order over security labels.

Derivation rules for expressions have the form:

Γ(x).

Derivation rules for instructions have the form:

where pc is a security label attached to the program counter, Γ 0 is an input type environment, and Γ is an output type environment.

D Precision of the Abstract Semantics of Expressions

Lemma 1 proves that the abstract semantics of expressions is as precise as the type labelling of expressions.

Lemma 1 (The abstract semantics of expressions is at least as precise as the type labelling of expressions). For all expressions a, for all abstract environments ∈ V ar D C , for all type environments Γ ∈ V ar {L, H}, such that: A a = n and Γ a : t. It holds that:

Proof. By structural induction on expressions:

-Case a = n:

The abstract semantics of expressions evaluates constants to 1. The type labelling evaluates constants to L. Therefore:

-Case a = a 1 bop a 2 :

Let n 1 = A a 1 and n 2 = A a 2 . Let also t 1 and t 2 such that Γ a 1 : t 1 , and Γ a 2 : t 2 . By induction on a 1 and a 1 , assumption α @ LH ( ) = Γ implies that:

-Cases a = a 1 cmp a 2 and a = a 1 mod n are both similar to case a = a 1 bop a 2 .

E Precision of the Abstract Semantics of Instructions

Theorem 4 proves that the abstract semantics of instructions is as precise as the type labelling of commands. We let ˙ denote the pointwise lifting the partial order over security labels to type environments.

Theorem 4 (The abstract semantics of commands is at least as precise as the type labelling of commands). For all commands c, for all abstract environments 0 , , and type environments Γ 0 , Γ such that: c 0 = and L Γ 0 {c}Γ. It holds that:

Proof. By structural induction on instructions:

-Case c = pp skip:

and Γ 0 = Γ. Therefore, assumption

-Case c = pp id := a: Let n = A a 0 and t such that Γ 0 a : t. By Lemma 1:

and Γ = Γ 0 [id → t], we have:

Let n = A a and t such that Γ 0 a : t. Let 1 = c 1 0 , and 2 = c 2 0 . Let Γ 1 and Γ 2 such that L Γ 0 {c 1 }Γ 1 and L Γ 0 {c 2 }Γ 2 . By induction on both c 1 and c 2 , we have:

• If n = 1 and t = L, we have = λid. 1 (id) ∪ ⊗ 2 (id) and Γ = λid.Γ 1 (id) Γ 2 (id). Therefore, since the union operator ∪ ⊗ computes the maximum over cardinal values, Equation ( 17) implies that

is the resulting type environments, and Γ 1 ˙ Γ 1 and Γ 2 ˙ Γ 2 . Therefore, by Equation ( 17) we have:

Let also Γ such that Γ = λid.Γ 1 (id) Γ 2 (id). Note that the only difference between Γ 1 and Γ 1 (resp. Γ 2 and Γ 2 ) is that variables that may be modified inside instruction c 1 (resp. instruction c 2 ) are set to H. Therefore the only difference between Γ and Γ is that variables that may be modified in either conditional branches are set to H. Thus, assuming α @ LH ( 0 ) = Γ 0 , for variables id that are not modified inside the conditional branches, Equation [START_REF] Smith | On the foundations of quantitative information flow[END_REF] yields:

@ LH ( (id)) Γ(id) = Γ (id)

Moreover, for variables id that may be modified inside the conditional branches, since Γ maps them to H, it holds that @ LH ( (id)) Γ (id)

Finally, by noting that Γ = Γ is the resulting type environments in the case where A a ≥ 1 , it holds that:

By a first induction on c 1 , then a second induction on c 2 , we obtain:

-Case pp while (a) c: Let us assume α @ LH ( 0 ) = Γ 0 . The output abstract environment is given by:

Additionally, the output type environment is given by:

Or, rewritten differently:

Let the sequences ( n ) and Γ n be defined as follows:

Then we prove by recurrence over n that ∀n, α @ LH ( n ) ˙ Γ n :

• For the initial case n = 0, it holds by assumption that α @ LH ( 0 ) = Γ 0 .

• Let us assume α @ LH ( n ) ˙ Γ n , and prove α @ LH ( n+1 ) ˙ Γ n+1 . By the same proof that is presented in the case of conditionals, we prove that:

α @ LH pp if (a) c else pp skip n ˙ Γ Additionally, since α @ LH ( 0 ) = Γ 0 , and the join operator ∪⊗ compute the maximum over cardinals, we have:

Therefore α @ LH ( n+1 ) ˙ Γ n+1 . This concludes our proof for the case of loops, since both sequences converge, and their limit satisfy α @ LH ( ∞ ) ˙ Γ ∞ .