P Geoffroy

O Bordron

N Mansard

M Raison

O Stasse

T Bretl

A two-stage suboptimal approximation for variable compliance and torque control

Variable-stiffness actuator is a very appealing mechatronic design that combines the efficiency of stiff actuator in free space with the consistency of elastic actuation in contact. The control of such an actuation system remains a challenge due to its non-linearity and by the fact that it doubles the number of control inputs. In this paper, we propose an original control strategy to compute the whole-body movement of a complex variable-stiffness robot during dynamic task execution. Operational space control is first used to compute both the joint torque and stiffness from operational references. A nonlinear model-predictive controller is then proposed to track at higher frequency these references on each joint separately. The effectiveness of this approach is then validated on two models of real actuator with adjustable stiffness, and finally on an explosive motion to make a humanoid robot jump.

I. INTRODUCTION

This paper deals with the control of multiple body robot with compliant actuation. This paradigm of actuation originates from the series-elastic actuator [START_REF] Pratt | Series elastic actuators[END_REF]. An example of complete series-elastic actuation is the Coman robot [START_REF] Tsagarakis | The design of the lower body of the compliant humanoid robot iCub[END_REF]. The compliance is a very positive property when the robot works in contact with its environment, but deeply complicates the control in particular when performing fast and accurate movements in free space. Variable-stiffness actuators are a nice trade-off, offering compliancy when in contact or before an impact but being stiff when accuracy is required [START_REF] English | Implementation of variable joint stiffness through antagonistic actuation using rolamite springs[END_REF].

We are interested in the capability to generate and control complex movements, e.g. a humanoid robot grasping an object while keeping its balance [START_REF] Mansard | Visually-guided grasping while walking on a humanoid robot[END_REF] or several manipulator robots moving an object collaboratively. The brute-force solution is to model the movement to execute as an optimal motion problem, and use direct solution method to obtain an approximation of the optimum [START_REF] Tassa | Synthesis and stabilization of complex behaviors through online trajectory optimization[END_REF]. However, this solution is computationally expensive: it scales in the cube of the number of actuators. It is yet prohibitive for complex variablestiffness robot that have two motors for each axis [START_REF] Enoch | Blue: A bipedal robot with variable stiffness and damping[END_REF].

A classical solution to reduce the complexity is to consider only the instantaneous linearization of the system evolution [START_REF] Whitney | Resolved motion rate control of manipulators and human prostheses[END_REF], resulting in inverse kinematics when only the geometry is considered [START_REF] Siciliano | A general framework for managing multiple tasks in highly redundant robotic systems[END_REF] or inverse dynamics when inertia and forces are considered. In particular, operational-space inverse dynamics, detailed below, proposes to compute the output motor joint torques in function of references forces and acceleration in some specific operational spaces [START_REF] Khatib | A unified approach for motion and force control of robot manipulators: The operational space formulation[END_REF]. The interest is that, when the proper operational space is chosen, the reference motion is generally very easy to specify.

Two major problems limit the generalization of operationspace inverse dynamics as the classical motion generation and method. First, joint torque is not a direct input of the motors, and a complex non-linear output as soon as reductors are introduced between the motor and the joint. Reductors are indeed difficult to properly model, which prevents feedforward control, while feedback control requires both an expensive torque sensor and a very fast (and very expensive) electronics [START_REF] Albu-Schaffer | The dlr lightweight robot: design and control concepts for robots in human environments[END_REF]. Second, there is no sense to instantaneously linearize a spring, since any force at the input of a spring would instantaneously produce zero motion at its output.

However, the spring actuation can be considered as an advantage to apply a reference torque on a real robot, by using the spring as a cheap force sensor. A first level compute the reference joint torques from the operational specification. The torques are then tracked by an optimal-motion solver for each joint, acting at higher frequency and taking care of the spring dynamics. Compared to the whole-body optimal solver described for example in [START_REF] Enoch | Blue: A bipedal robot with variable stiffness and damping[END_REF], this solution decouples the space complexity (solved by the whole-body inverse dynamics) from the temporal complexity (solved by each actuator optimal controller). The decoupled solution can be seen as a suboptimal approximation to the whole-body optimal problem.

With respect to this strategy, the paper proposes three contributions. We propose a method to compute the reference joint compliance from operation compliance specification, based on the operational-space formulation (Section II). We then propose a generic method to efficiently compute the optimal control law at the joint level (Section III). This method can be directly applied to any possibly non-linear joint model and various cost function, for tracking the output acceleration, torque or stiffness as shown in Section IV. Finally, we propose an implementation of the optimal controller, coupled with the operational-space solver, to produce complex movements. In particular, we demonstrate a wholebody jump in simulation with a modified stiffness-variable humanoid in Section V.

II. FROM WHOLE-BODY OBJECTIVES TO ACTUATOR REFERENCES

We first recall in Section II-A the generic model of a free-floating robot in contact with a known, typically rigid, environment. From this model, it is classical to deduce a torque control law based on task specifications, which is also recalled in Section II-B. Based on this model and this procedure, we propose a solution to deduce the needed whole-body compliance to meet some reference compliance expressed in given task spaces in Section II-C.

A. Dynamic model

In general, the dynamics model of the robot whole body, considering all the bodies and the actuator to be stiff, is:

A(q)q + b(q, q) = S T τ - nc k=1 J k (q) T f k (1)
where A is the generalized inertia matrix, b is the dynamic drift (sum of Coriolis, centrifugal and gravity forces), τ are the joint torques (typically, the actuator output torques), S is the matrix that selects the actuated degrees of freedom (DOF), f k are the n c contact forces exerted by the robot on the environment at the contact points p k and J k = ∂p k ∂q are the Jacobian of the contact points.

This equation represents the inverse dynamics: from a given joint acceleration given as a reference, it gives the forces that would lead to this acceleration. The three q, τ and f c = (f 1 , ..., f nc ) are variable and evolve together. Very often in robotics, we want to impose a reference q and search for a solution τ meeting this reference, while f c is explicitly needed.

It is possible to get ride of f c and then compute the needed joint torques if an interface model is given. For example, if assuming a rigid contact J k q + Jk q = 0 1 , an accelerationfree relation can be obtained from (1):

J c A -1 τ = J c A -1 J T c f c + b c
where J c = (J 1 , ..., J nc ) and b c = J c A -1 b -Jc q. When J c is full row rank, f c can be immediately deduced from τ . This leads to equivalent dynamics in contact [START_REF] Park | Contact consistent control framework for humanoid robots[END_REF]:

Aq + b c = (SN c ) T τ (2)
where

N c = I -J T c (J c A -1 J T c ) -1 J c A -1 is the projector in the null space of J alongside the direction A -1 and b c = N T c b -(J c A -1 J T c ) -1
Jc q. This equation still holds when J c is not full row rank, even if slightly less intuitively obtained [START_REF] Mansard | A dedicated solver for fast operational-space inverse dynamics[END_REF].

In this last equation, the contact forces are considered as additional actuators to compensate the underactuation expressed by S T . It is possible to separate the forces into support forces f s , used as actuators, and the other forces, which would be typically used to accomplished a given force reference. In that case, the equation is written:

Aq + b S = (SN S ) T τ + n f k=1 J k f k 1
The contact typically also imposes the forces to stay in the friction, which comes as an additional constraint expressed in fc.

B. Operational-space inverse dynamics 1) For one task: The task-function [START_REF] Samson | Robot Control: the Task Function Approach[END_REF], or operationalspace [START_REF] Khatib | A unified approach for motion and force control of robot manipulators: The operational space formulation[END_REF], approach was proposed to enable the user to define the objectives of the motion to be executed in a dedicated task, or operational, space rather than directly in the configuration space. The task is defined by a vector function e(q, Ω) ∈ R m of the robot configuration q and the rest of the universe Ω, whose image space is called the task space and whose Jacobian with respect to the configuration is denoted J = ∂e ∂q . In addition to the task function, the control in the task space is given as a reference vector field ë * in the tangent to the task space. The task acceleration ë can be linked to the control input τ by multiplying (2) by JA -1 :

ë = JA -1 (SN S ) T τ + µ
where µ is the task drift that collects the non linear terms. τ is obtained by solving this equation in the least-square sense:

τ = (JA -1 (SN S ) T ) # ë * -µ
where . # denotes any reflexive generalized inverse, typically the inverse weighted on the left by SA -1 (SN S ) T [START_REF] Park | Control strategies for robots in contact[END_REF].

2) For several tasks: This last form satisfies the task while minimizing the given norm, but the general solution is written:

τ = (JA -1 (SN S ) T ) # ë * -µ + P τ 2
The second input τ 2 can be chosen arbitrarily (τ 2 = 0 results in the least norm solution). This second input can be used to satisfy a secondary task, and recursively, any number of tasks set up in a hierarchy order. Denoting by e 1 ... e p the hierarchy of tasks with J i the task Jacobian, the general solution is:

τ = i G # i|i-1 ëi * -µ i|i-1 with G i = J i A -1 (SN S ) T , G i|i-1 = G i P i-1 , P 0 = I, ∀i > 0, P i = P i-1 -G # i|i-1 G i|i-1
and µ i|i-1 collects all the non linear terms. More details are given in [START_REF] Saab | Dynamic whole-body motion generation under rigid contacts and other unilateral constraints[END_REF]. In particular, the hierarchy can be implemented on an efficient manner and be coupled with an active-set search if some task references are given as bounds rather that equality.

C. Operational-space inverse compliance

Our objective in this section is to define a similar scheme to compute the configuration compliance, being given some reference compliance in dedicated task spaces. We first consider the fully actuated case, i.e. when SN S is invertible (typically, a fixed manipulator whose only considered contact forces are at the interface with the ground).

1) Direct compliance model: We denote by Γ the compliance of the axes, supposed constant (linear springs). A variation of the torques then induces a variation of the axis position ∆q given by ∆q = ∆ Γτ Γ can be seen both as a diagonal matrix (make explicit by the left exponent ∆ Γ) or as a vector (denoted ∨ Γ).

Consider now a slight change of configuration ∆q from the spring equilibrium. We search for the equivalent spring reflected at a given contact point. The change ∆q leads both to a change of contact position and contact forces. The change of position is directly:

∆x = J∆q
The change of force is expressed from the steady-state forceto-torque equation τ = J T f . Plugging both equations, we get:

∆x = J∆q = J ∆ Γτ = J ∆ ΓJ T f
The apparent compliance can then be defined by:

γ = J ∆ ΓJ T
where γ is a square symmetric matrix.

2) Quadratic solution: Now assume that we require a specific apparent compliance γ * . The configuration compliance that best matches this reference can be expressed as the solution of the Frobenius problem:

min ∆ Γdiagonal J ∆ ΓJ T -γ * F
where . F denotes the Frobenius norm. This is a quadratic problem, since the square Frobenius norm is the sum of square of the matrix coefficients and since J ∆ ΓJ T is linear if Γ.

We denote by ∨ . the matrix-to-vector operator stacking all the columns of the input matrix 2 . The Frobenius problem can be explicitly rewritten as a quadratic problem:

min ∨ Γ J ∨ Γ -∨ γ * 2
where J is the unique matrix such that J ∨ Γ = ∨ (J ∆ ΓJ T ). This operator has the following properties:

J ∨ Γ = J ∆ ΓJ T (3)
J T ∨ γ = ∆ (J T γ * J) (4)
where ∆ . denotes the matrix-to-vector operator that selects the diagonal elements of the input matrix. Finally, the square of J is the Hadamard square of the square of J:

J T J = [[J T J]] (5)
where

[[A]] = A • A denotes the element-wise (Hadamard) square of A.
The solution to the unconstrained quadratic problem is given by the pseudo-inverse:

∨ Γ = J + ∨ γ *
Since for any A, A + = (A T A) + A T and using [START_REF] Tassa | Synthesis and stabilization of complex behaviors through online trajectory optimization[END_REF], this last form can be rewritten:

∨ Γ = [[J T J]] + ∆ (J T γ * J) (6)
2 The operators ∨ . is abusively applied to pass from the diagonal matrix ∆ Γ to the vector of the diagonal elements ∨ Γ, to keep the notations simple.

3) Hierarchical solution: Among all the solutions that fit at best in the least-norm-2 sense the reference γ * , this last solution is the one of least norm-2 Γ. As usual for quadratic system, the redundancy can be made evident by expressing all the possible solutions using the projector on the null space of J :

∨ Γ = [[J T J]] + ∆ (J T γ * J) + P ∨ Γ 2 where P = I -[[J T J]] + [[J T J]] = ker[[J T J]]
and ∨ Γ 2 is any configuration compliance that can be used to satisfy a second objective.

Assume now that several compliance objectives γ * 1 , ... , γ * p ordered in a hierarchy are given. Using the classical redundancy scheme detailed in [START_REF] Siciliano | A general framework for managing multiple tasks in highly redundant robotic systems[END_REF], the configuration compliance matching at best in the last-square sense the hierarchy of the γ * is Γ p obtained by the following iteration:

∨ Γ k = ∨ Γ k-1 (7)
+ (P k-1 [[J T k J k ]]P k-1 ) + ∆ J T k (γ * k -J k ∆ Γ k-1 J T k )J k
with P k the projector onto the null space of the stacked k first Jacobian, that can be computed following the recurrence proposed in [START_REF] Baerlocher | Inverse kinematics techniques for the interactive posture control of articulated figures[END_REF]. 4) Constrained system: All the development above holds for a fully-actuated unconstrained system, and by direct generalization to the case when SN S S T is invertible. In the general case, the relation between a change of elastic torques τ = ∆ Γ∆q and contact force f is correlated with the support N S :

(SN S ) T τ = J T f
The displacement ∆q cope with the rigid contact and thus is such that:

∆q = N S ∆q
since N S is a projector onto the kernel of J S . The compliance relation is then written:

γ = J T (SN S ) T ∆ ΓSN S J
The same previous developments then still hold, with direct adaptations. The operational inverse compliance is then:

∨ Γ k = ∨ Γ k-1 + (P k-1|S [[J T k|S J k|S ]]P k-1|S ) + (8) ∆ J T k (k * k -J k ∆ Γ k-1 J T k )J k
with J k|S = SN S J k and P k|S the projector onto the stacked J k|S Hadamard squares.

III. MODEL PREDICTIVE CONTROL

In this section, we quickly recall the optimal control method that we used to drive the compliant actuators. A. Principles and model Consider a generic system, with state variable x and control variable u, defined by its discrete time evolution function:

x t+1 = f (x t , u t , t) (9)
where f is the system evolution function and the time variable t is considered discrete. Optimal control aims at computing the control and state trajectory by minimizing a given cost function:

min X,U T -1 t=0 l t (x t , u t ) + l T (x T )
where T is the preview interval length (fixed), U = (u 0 ...u T -1 ), X = (x 0 , ..., x T ) are the control and state trajectories and l t and l T are the running and terminal costs functions. The optimal control problem is to be solved under the constraint that (9) is satisfied. In practice, the problem is solved for X only or U only, the other variable being deduced from the dynamic equation. The solution is said explicit when computing X and implicit when computing U . The optimal solution for a linear dynamics x t+1 = F x x t + F u u t and a quadratic cost is given by Riccati equations as a linear-quadratic regulator (LQR). Model predictive control (MPC) is an advance control technique to control a given system by optimizing its predicted evolution. It relies on the systematic evaluation of the optimal control of the system with respect to a reference cost function, while only the first few steps of the optimal trajectory are actually executed by the actuators before its complete re-evaluation. The main interest of MPC is the ability of dealing with non-linear systems whose instantaneous linearization is not meaningful.

B. Differential dynamic programming

The Differential Dynamic Programming (DDP) is an iterative algorithm to solve a non-linear continuous optimal control problem using implicit formulation [START_REF] Tassa | Synthesis and stabilization of complex behaviors through online trajectory optimization[END_REF]. It is nearly equivalent to the application of a Newton descent algorithm. As in the Newton descent, the main idea is to approach a local optimum by iteratively modifying a candidate solution until stabilization of the evaluation of the cost function.

It starts with initial state and control trajectories, typically obtained from the integration of the zero control if no other prior is available. The algorithm then iterates in two stages. It first computes an approximate quadratic model of the current candidate trajectory and compute the corresponding LQR (backward loop). Then the candidate is modified following the LQR (forward loop).

IV. VARIABLE STIFFNESS ACTUATORS

The previous section recalled a generic MPC framework. We now propose a solution to implement it, to efficiently control the behavior of a variable-stiffness actuator.

A. Principles

The operational-space approach provides the reference joint behavior (torques and/or stiffness) from operational references set by the user. The computation is typically expensive, since many DOF are involved and the whole-body operations scale with the cube of the number of joints. We can expect them to be computed at a middle dynamics (e.g. 100Hz). For in contact movements, the actuators have to react much faster to track this reference behavior (typically, 1kHz is advised [START_REF] Hogan | Impedance control[END_REF], 3kHz is implemented on the LWR robot [START_REF] Albu-Schaffer | The dlr lightweight robot: design and control concepts for robots in human environments[END_REF] while 10kHz are available on the iCub [START_REF] Tsagarakis | The design of the lower body of the compliant humanoid robot iCub[END_REF]). The joint references are then tracked by a DDP-based MPC whose cost function is described below.

B. Actuator generic model

We consider electrical-based variable stiffness actuators, where two motors in parallel are connected in series with some mechanical springs. This generic hypothesis is valid for a large class of actuators [START_REF] Jafari | A novel intrinsically energy efficient development of a novel actuator with adjustable stiffness (AwAS)[END_REF], [START_REF]used for Energy Efficient Hopping Robot Chobino1D, "Vanderborght b., tsagarakis n., van ham r., thorson i., caldwell d[END_REF] (see Fig. 1). While the general approach is still valid, this precise hypothesis cannot cover for example pneumatic actuators [START_REF] Tondu | Modeling and control of mckibben artificial muscle robot actuators[END_REF], [START_REF] Tassa | Modeling and identification of pneumatic actuators[END_REF]. The state variables are then reduced to the spring positions and velocities. Typically, two motors are involved:

x = (x 1 , x 2 , ẋ1 , ẋ2 )
If assuming linear (or at least static) models of the spring, the output torques can be deduced from the state.

We additionally make the hypothesis that the motor is capable of tracking acceleration references. While the electrical motors are typically driven in electrical power (current or voltage), a first close loop is typically configured on the feedback of a output position (angular) sensor. Moreover, a mechanical reductor is often added in series with the motor, which acts as a dynamic screen preventing the motor to feel the joint dynamics. These two facts make the acceleration an easy but realistic control input. The control is then simply:

u = (ẍ 1 , ẍ2 )

C. Cost function

We consider the following terminal cost function:

l T (x T ) = w T (τ (x T ) -τ * T ) 2
The current torque is a function of the spring states, while τ * T is given by the operation-space computations. The running cost function is:

l t (x t , u t ) = w τ (τ (x t ) -τ * t ) 2 + ||u t || 2 Q + w j j(x t )
where τ * t is typically equals to τ * T , j is a barrier function enforcing the joint limits and w f , w τ , w j and Q are arbitrary gains that encompass the unit differences and the relative importance of the terms. The first term enforces the MPC to track the reference. The second term penalizes strong internal movements and regularizes the numerical solver behavior. The last term enforces any given constraints 3 . The barrier function is constructed to be positive, continuous and twice derivable, to value 0 on at from the limit and +∞ on the limits.

An additional term w Γ (Γ(x t ) -Γ * t ) 2 can be added in both l t and l T to track a reference output stiffness, also function of the state. If no good reference stiffness is available, w Γ is set to 0. The stiffness is then locally tuned by the optimal controller in answer to the actuator demanded dynamics. A comparison with and without reference stiffness is given in the next section.

D. Discussion

The obtained control scheme may be compared to the optimal controller described in [START_REF] Sardellitti | Gain scheduling control for a class of variable stiffness actuators based on lever mechanisms[END_REF]. In this paper, the authors control a torque-driven actuator to enforce an output position on an AwAS actuator [START_REF] Jafari | A novel intrinsically energy efficient development of a novel actuator with adjustable stiffness (AwAS)[END_REF]. They deployed a LQR by linearizing their actuator. This is possible since the torque-input position-output AwAS is linear for small spring deflection. For that mean, they have to separate the model between one main actuator driven the output motion and one stiffness actuator tuning the apparent stiffness. They finally proved the stability of their control scheme and proposed a theoretical study of its behavior that was used to automatically adapt the cost-function weights.

Our approach is more generic since no separation is needed and non-linear actuators may be considered, for example the MACCEPA. Moreover, if the stiffness is free, the controller will use it to reduce the oscillations of the output movement. Using the LQR formulation behind the DDP, the stability of our MPC can be derived using the same 3 The DDP is efficient partly because unconstrained. The barrier function is an efficient solution to enforce important terms to be treated as constraints. reasoning than in [START_REF] Sardellitti | Gain scheduling control for a class of variable stiffness actuators based on lever mechanisms[END_REF]. It seems more difficult to adapt the pole study for tuning the weights in general, since the poles vary with the system non-linearities. However, the same study can be directly applied when the non-linearities can be neglected (e.g. for the AwAS at steady-state).

V. RESULTS

We present in this section two set of simulations. In a first time, we checked the behavior of the MPC for a single actuator using the two actuator models AwAS and MACCEPA. The AwAS has a nearly linear dynamics, which is interesting to validate the LQR behavior, while the MACCEPA is less linear, which validates the capabilities of the DDP to handle a more complex cost landscape. We then produce a complex whole-body movement for a humanoid robot whose joint references are tracked by the MPC.

A. Single actuator 1) Set up: The simulations are made on the software Matlab. The model dimension are chosen to fit the requirements of a full size humanoid robot (for typical movements recorded on HRP-2). The control sampling frequency is 10kHz: the DDP is recomputed at 10kHz and the first sample is applied on the motor models. The preview windows lasts 2.5ms (that is to say 25 samples). The number of DDP iteration is bounded to 50 (while AwAS generally converges in less than 25). The MPC is used for tracking a smooth and a pulse-train reference without disturbance, and the behavior is then checked for external disturbances.

2) Torque reference tracking: DDP control has been tested for two scenarios : a pulse train and a polynomial. The response plot are given in Figures 2 and3.

The first reference torque is a polynomial of degree three (Fig. 2). For both actuators, output torque is properly tracked. In the absence of discontinuity, DDP provides excellent control, no matter with the complexity of cost function.

The pulse-train amplitude is set to 10 Nm (calibrated on the knee torques during humanoid dynamics locomotion task). The AwAS is very reactive, reaching quickly 97% of the desired value and is stable. MACCEPA model, results are more mixed, with slower convergence time. These differences are explained by the different level of complexity of the two dynamics, excited by the train pulse that generates singularities. It is representative of a shock during an explosive task. The MACCEPA behavior might be improved by adjusting the cost weights, for example using a deeper analysis of the close-loop system.

3) Robustness: The robustness is tested for a constant reference. We let the system converge and then apply a static force of 5 Nm at the actuator output. The result is summarized in Fig. 4. The response time before new stability of the torque generated by the spring tension is of the same order as in the case of train pulse. The system naturally comes back to the reference position after a small adaptation time. We consider a jumping movement with a model created from the HRP-2 robot [START_REF] Kaneko | Design of prototype humanoid robotics platform for hrp[END_REF]: the body specifications have been kept has the actuator dimensions, but we have replaced in simulation the stiff actuation by a set of variable stiffness actuators. The movement is defined by a sequence of tasks using the jumping methodology proposed in [START_REF] De Lasa | Feature-based locomotion controllers[END_REF]. The motion is composed of three phases: starting from a low squatting posture, the robot violently accelerates its center of mass (CoM) until the legs are stretched while keeping a controlled (typically zero) angular momentum. The robot then floats while its CoM decelerates due to the gravity. During the flight phase, only the orientations of the feet are controlled to anticipate the landing. The robot finally impacts the ground and gently decelerates its CoM to recover its rest posture. The joint references are computed at 200Hz. One MPC at each joint then tracks this reference at 10kHz following the same set-up as in the previous section.

2) Torque tracking: The motion is summarized in Figures 5 to 8. Snapshots of the movement are gathered in Fig. 5. The whole body movement is not detailed by lack of space. The joint torques are tracked by an AwAS on the hip and a MACCEPA on the knee (the choices are arbitrary). We spotted torques on joints of a humanoid robot during a simulation of jump on site. The tracking performances are displayed in Fig. 6. The explosive movement is properly tracked. The reference torque at the impact is 3 Nm for the hip, and the MPC produces 3.3 Nm (91%). At the knee, the reference torque is 10 Nm while the MPC produces 10.8 Nm (108%). The delay is 15 ms which corresponds to the spring dynamics. This result proves the interest of using the spring actuation with MPC for achieving complex wholebody dynamic movements.

3) Stiffness selection: The joint compliance is computed from the a reference operational compliance. We set up a compliance of 2000 N/m on the z-axis of each foot, with a compliance of 40000 N/m on the two lateral rotations and stiff coupling between the translation and the rotations. The obtained joint stiffness of one leg is plotted in Fig. 7. It is perfectly tracked by the MPC. When the stiffness is let free, the MPC uses this additional DOF to optimize the output torque while minimizing the input. It is evident on the singleactuator pulse train displayed in Fig. 8. In particular, the stiffness changes at each new pulse and constantly decreases (the spring position increases) when the actuator position stabilizes.

VI. CONCLUSION

In this paper, we have proposed an original approach to control the whole-body movement of complex variablestiffness robot. The operational-space approach is first used to compute the joint torques and stiffness from operational force, acceleration and compliance references. An MPC controller is then used to control the movement of each elastic actuator to track the joint references. The global approach can be seen as an efficient suboptimal to the yet untractable whole-body optimal control problem. It is very appealing to apply torque references on electrical actuators while avoid an excessive mechatronic cost.

More particularly, we have proposed an original solution to compute the joint compliance from operational references. We have proposed an efficient MPC solution to track the joint references, both torques and stiffness, using DDP. This method can be seen as a generalization to a large class of actuator and to non-linear situations of the LQR proposed in [START_REF] Sardellitti | Gain scheduling control for a class of variable stiffness actuators based on lever mechanisms[END_REF]. Finally, we have proposed a complete validation in simulation, by controlling the jump of a variable-stiffness fullsize humanoid robot. Behind the application to a physical robot, the next step of our work is to exhibit the theoretical properties of our controller, in particular its stability.

Fig. 1 .

 1 Fig. 1. Schema of the two actuator models used in the experiments.

  Fig. 2. Simulation A.1: Output torques with AwAS and MACCEPA actuators for a polynomial control

Fig. 4 .

 4 Fig. 4. Simulation A.3: Effect of 5 Nm perturbation torque at time t = 30 ms on a constant control

Fig. 5 .Fig. 6 .Fig. 7 .Fig. 8 .

 5678 Fig. 5. Simulation B: Snapshots of the jumping movement.

ACKNOWLEDGMENTS

The work has been partly supported by the grant ANR 13-CORD-002-01 Entracte.


Aurélien Vallet

Davit Catherine Bertrand

Davit Varron

Jacques Mudry

Hydrogeological threshold using effective rainfall and support vector machine (SVM) applied to a deep seated unstable slope (Séchilienne, French Alps)

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

L'article n'a plus de validité scientifique.


Yusuke Kawamoto

Thomas Given-Wilson

Quantitative Information Flow for Scheduler-Dependent Systems *

Quantitative information flow analyses measure how much information on secrets is leaked by publicly observable outputs. One area of interest is to quantify and estimate the information leakage of composed systems. Prior work has focused on running disjoint component systems in parallel and reasoning about the leakage compositionally, but has not explored how the component systems are run in parallel or how the leakage of composed systems can be minimised. In this paper we consider the manner in which parallel systems can be combined or scheduled. This considers the effects of scheduling channels where resources may be shared, or whether the outputs may be incrementally observed. We also generalise the attacker's capability, of observing outputs of the system, to consider attackers who may be imperfect in their observations, e.g. when outputs may be confused with one another, or when assessing the time taken for an output to appear. Our main contribution is to present how scheduling and observation effect information leakage properties. In particular, that scheduling can hide some leaked information from perfect observers, while some scheduling may reveal secret information that is hidden to imperfect observers. In addition we present an algorithm to construct a scheduler that minimises the min-entropy leakage and min-capacity in the presence of any observer.

Introduction

Preventing the leakage of confidential information is an important goal in research of information security. When some information leakage is unavoidable in practice, the next step is to quantify and reduce the leakage. Recently theories and tools on quantitative information flow have been developed using information theory to address these issues [START_REF] Clark | Quantitative Analysis of the Leakage of Confidential Data[END_REF][START_REF] Boreale | Quantifying information leakage in process calculi[END_REF][START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF][START_REF] Chatzikokolakis | Anonymity Protocols as Noisy Channels[END_REF][START_REF] Smith | On the Foundations of Quantitative Information Flow[END_REF][START_REF] Boreale | Asymptotic Information Leakage under One-Try Attacks[END_REF][START_REF] Chothia | Probabilistic Point-to-Point Information Leakage[END_REF][START_REF] Chothia | LeakWatch: Estimating Information Leakage from Java Programs[END_REF]. The common approach is to model systems as information-theoretic channels that receive secret input and returns observable output.

One area of interest is to quantify and estimate the information leakage of composed systems. When composing systems the manner of reasoning about their behaviour is non-trivial and is complicated by many factors. One of the first approaches is to consider the (disjoint) parallel composition, that is, simply running the component systems independently and regarding them as a single composed system. This approach provides some general behaviour and reasoning about the whole composed system, as shown in the research of quantitative information flow with different operational scenarios of attack [START_REF] Barthe | Information-theoretic Bounds for Differentially Private Mechanisms[END_REF][START_REF] Espinoza | Min-entropy as a resource[END_REF][START_REF] Kawamoto | Compositionality Results for Quantitative Information Flow[END_REF]. However, the parallel composition approach is coarse-grained and abstracts many of the channels' behaviours that may lead to changes in information leakage. Although this approach provides useful results on the bounds of possible leakage, it does so under the assumption that the component channels are executed independently and observed separately. That is, their outputs can always be linked to the disjoint component channels, and that both their outputs are observed simultaneously and without any interleaving or reflection of how the component channels achieved their outputs.

2

Quantitative Information Flow for Scheduler-Dependent Systems Here we take a more fine-grained approach where we consider that channels may provide a sequence of observable actions. Thus, a channel may be observed to output a sequence of actions, or the passage of time may be observed to pass between the initiation of the channel and a final output. This captures more mechanics of real world systems and allows for greater refined reasoning about their behaviour.

Such sequences of observable actions also allow a more subtle approach to combining channels in parallel. Rather than simply taking both outputs to appear together at the termination of their operations, observations can be made of the sequence in which the outputs appear. Such a combination of channels becomes parametrised by a scheduler, that informs on how to combine the observable sequences of actions into a single sequence. This can then represent very direct behaviour such as scheduling properties of a shared CPU, or abstract behaviours such as routing properties, vote counting, etc.

The other novel approach presented here is the refinement of the attacker's capability of observing the outputs of systems. We model attackers that may have imperfect observability: they may not accurately detect differences in outputs, or may do so only probabilistically. This captures, for example, the situation where the attacker may be blind to some internal behaviour that other agents can detect. In this paper such imperfect observations are modeled using what we call observer channels. This formalisation enables us to consider a large class of observers, including probabilistic observers, which have never been considered in the previous studies on quantitative information flow.

These refinements to composing information-theoretic channels allow us to reason about behaviours that may be obvious, but not captured by previous approaches. In this paper we present three kinds of results regarding the effect of leakage properties due to the considering of schedulers and observers. First, since scheduled composition can alter the leakage relative to the parallel composition, we present theorems for detecting when a scheduled composition does not alter the relative information leakage. This means some preliminary analysis may be sufficient to determine when scheduled composition may be worthy of further consideration. Second, scheduled composition can leak more or less information than the parallel composition depending on the properties of the channels and the power of the observer. Although the potential effect on leakage is dependent upon many factors, we present results that determine an upper bound for the leakage of a schedule-composed channel. Third, we present results for finding a scheduler that minimises the min-entropy leakage and min-capacity in the presence of any observer. We present how to construct such a scheduler by solving a linear programming problem.

In addition we evaluate our model and results with some simple yet intuitive examples, such as mix networks for voter anonymity, and side-channel attacks against cryptographic algorithms. We provide an implementation that can be used to calculate the behaviours of information-theoretic channels, schedulers, and observers as presented here. The implementation is available online [1], which requires the libraries leakiEst tool [START_REF] Chothia | A Tool for Estimating Information Leakage[END_REF] and the linear programming system lp solve [2].

The rest of the paper is structured as follows. Section 2 recalls the definitions of information-theoretic channels and measures of information leakage. Section 3 defines traces, systems and channel compositions, and shows examples of schedulers. Section 4 introduces the notion of generalised observers and defines the observed leakage. Section 5 presents our main results in a general manner. Section 6 applies these results to well known problems. Section 7 discusses some related work. Section 8 draws conclusions and discusses future work. All proofs can be found in Appendix of the paper.

Preliminaries

Information-Theoretic Channel

Systems are modeled as information-theoretic channels to quantify information leakage using information theory. A channel K is defined as a triple (X , Y ,C) consisting of a finite set X of secret input Y. Kawamoto & T. Given-Wilson 3 values, a finite set Y of observable output values, and a channel matrix C each of whose row represents a probability distribution; i.e., for all x ∈ X and y ∈ Y , 0 ≤ C[x, y] ≤ 1 and ∑ y ′ ∈Y C[x, y ′ ] = 1. For each x ∈ X and y ∈ Y , C[x, y] is a conditional probability p(y|x) of observing y when the secret of the system is x. We assume some secret distribution π on X , which is also called a prior. Given a prior π on X , the joint distribution of having a secret x ∈ X and an observable y ∈ Y is defined by p(x, y)

= π[x]C[x, y].

Quantitative Information Leakage Measures

In this section we recall the definitions of two popular quantitative information leakage measures.

Mutual information is a leakage measure based on the Shannon entropy of the secret distribution.

Definition 1 Given a prior π on X and a channel K = (X , Y ,C), the mutual information I (π, K ) w.r.t. π and K is defined by:

I (π, K ) = ∑ x∈X ,y∈Y π[x]C[x, y] log ( C[x, y] ∑ y ′ ∈Y C[x, y ′ ]
)

.

Then the Shannon's channel-capacity S C (K ) of a channel K is given by max π I (π, K ) where π ranges over all distributions on X .

Min-entropy leakage quantifies information leakage under single-attempt guessing attacks [START_REF] Braun | Quantitative Notions of Leakage for One-try Attacks[END_REF][START_REF] Smith | On the Foundations of Quantitative Information Flow[END_REF].

Definition 2 Given a prior π on X , and a channel K = (X , Y ,C), the prior vulnerability V (π) and the posterior vulnerability V (π, K ) are defined respectively as

V (π) = max x∈X π[x] and V (π, K ) = ∑ y∈Y max x∈X π[x]C[x, y].
Then the min-entropy leakage L (π, K ) and the min-capacity M C (K ) are defined by:

L (π, K ) = -logV (π) + logV (π, K ) and M C (K ) = sup π L (π, K ).
3 Information Leakage of Scheduler-Dependent Systems

Traces and Systems

In general the output of an information-theoretic channel can be defined in many different ways. In this work we consider traces, or sequences of actions, as observable values. Assume a countable set of names denoted m, m ′ , m 1 , m 2 , . . . and a countable set of values v, v 1 , v ′ , . . .. We define an action by µ, α, β ::= τ | m⟨v⟩ . Here τ denotes the traditional silent or internal action that contains no further information. The output action m⟨v⟩ can be considered to exhibit some value v via some named mechanism m. In concurrency theory the output action typically refers to the the named mechanism as a channel name, which is distinct from the notion of information-theoretic channel used here. Here the output action is used in a more general sense, in that m⟨v⟩ exhibits some value v such as runtime measured via mechanism m. For example, v could be runtime, electronic power usage or other value determined by the input, and m could be via direct communication/circuitry, indirect side effects, or any other means.

A trace is defined to be a sequence of actions of the form µ 1 .µ 2 . . . . .µ i . The notation α ∈ µ 1 .µ 2 . . . . .µ i denotes that there exists a j ∈ {1, 2, . . . , i} such that µ j = α. Similarly a sequence of i actions µ can be denoted µ i , and an empty sequence of actions by / 0. A system is modeled as an information-theoretic channel (X , Y ,C) where |X | is finite and the set Y of observables is a finite set of traces.

Quantitative Information Flow for Scheduler-Dependent Systems

C 1 ×C 2 C 1 C 2 - - - - X 1 X 2 Y 1 Y 2 (a) Parallel composition Comp S (C 1 ,C 2 ) C 1 C 2 S Obs - - - - - - X 1 X 2 Y 1 Y 2 Y Z (b) Observation of a scheduled composition

Scheduled Composition

In this section we model scheduler-dependent systems by introducing the notion of a scheduled composition of information-theoretic channels, which interleaves outputs from different channels.

In [START_REF] Kawamoto | Compositionality Results for Quantitative Information Flow[END_REF] the parallel composition K 1 × K 2 of two component channels K 1 and K 2 is defined as a channel that outputs ordered pairs consisting of the outputs of the two component channels. That is, given two component channels

K 1 = (X 1 , Y 1 ,C 1 ) and K 2 = (X 2 , Y 2 ,C 2 )
, the outputs of their parallel composition range over the ordered pairs (y 1 , y 2 ) for all y 1 ∈ Y 1 and y 2 ∈ Y 2 . This composition can be modeled using a scheduler that allows K 1 to perform the whole sequence y 1 of actions and some action sep ̸ ∈ Y 1 ∪ Y 2 (for separating y 1 from y 2 ) before K 2 performs the actions in y 2 . 1 In this setting we can recognise which component channel each output of the composed channel came out of.

In this paper we consider more fine-grained schedulers that may allow K 2 to perform some actions before K 1 completes the whole sequence of actions. To model such schedulers, we define the set of possible interleaving of two traces that preserves the orders of occurrences of actions in the traces.

Definition 3 (Interleaving of traces) Let us consider two traces y 1 of the form α 1 .α 2 . . . . .α k and y 2 of the form β 1 .β 2 . . . . .β l . The interleaving Int(y 1 , y 2 ) of y 1 and y 2 is the set of all traces of the form µ 1 .µ 2 . . . . .µ k+l s.t., for two sequences of distinct integers 1 ≤ i 1 < i 2 < . . . < i k ≤ k + l and 1 ≤ j 1 < j 2 < . . . < j l ≤ k + l, we have µ i m = α m for all m = 1,2, . . . , k and µ j m = β m for all m = 1, 2, . . . , l. Although the interleaving defines all possible combinations of the sets of traces, they do not define the probability of their appearance. To reason about this, we define a scheduler that takes two sets of traces and probabilistically schedules their actions to form each possible trace in their interleaving.

Definition 5 (Scheduler) A scheduler S on Y 1 and Y 2 is a function that, given two traces y 1 ∈ Y 1 and y 2 ∈ Y 2 , produces a probability distribution over all the possible interleaving Int(y 1 , y 2 ). We denote by S (y 1 , y 2 )[y] the conditional probability of having an interleaved trace y given y 1 and y 2 .

We define a deterministic scheduler as one that produces the same output for any given two traces.

Definition 6 (Deterministic scheduler) A scheduler S is deterministic if for any two traces y 1 and y 2 , there exists y ∈ Int(y 1 , y 2 ) such that S (y 1 , y 2 )[y] = 1. This provides the basis for composing channels in general, however this requires some delicacy since the interleaving of different traces may produce the same result. For example, given y 1 = τ.m⟨s⟩ and y 2 = τ then one of the possible traces produced is τ.τ.m⟨s⟩. However, given y 3 = m⟨s⟩ and y 4 = τ.τ then the same trace τ.τ.m⟨s⟩ could also be produced. Let p(y 1 , y 2 ) be the joint probability that two component channels output two traces y 1 and y 2 . Then the probability that S produces an interleaved trace y is given by: p

observable m 1 ⟨0⟩ τ.m 1 ⟨0⟩ m 1 ⟨1⟩ τ.m 1 ⟨1⟩ 0 0.5 0 0 0.5 secret 1 0 0.5 0.5 0 Table 1: Channel matrix C 1 observable m 2 ⟨0⟩ τ.m 2 ⟨0⟩ m 2 ⟨1⟩ τ.m 2 ⟨1⟩ 0 0 0.5 0.5 0 secret 1 0.5 0 0 0.5
(y) = ∑ y 1 ∈Y 1 ,y 2 ∈Y 2 p(y 1 , y 2 ) • S (y 1 , y 2 )[y]. By [20] we obtain C 1 [x 1 , y 1 ]C 2 [x 2 , y 2 ] = p(y 1 , y 2 |x 1 , x 2 ).
Hence we can define scheduled composition of channels as follows.

Definition 7 (Scheduled composition of channels) The scheduled composition of two channels

K 1 = (X 1 , Y 2 ,C 1 ) and K 2 = (X 2 , Y 2 ,C 2 ) with respect to a scheduler S is define as the channel (X 1 × X 2 , Int(Y 1 , Y 2 ),C) where the matrix element for x 1 ∈ X 1 , x 2 ∈ X 2 and y ∈ Int(Y 1 , Y 2 ) is given by: C[(x 1 , x 2 ), y] = ∑ y 1 ∈Y 1 , y 2 ∈Y 2 C 1 [x 1 , y 1 ]C 2 [x 2 , y 2 ]S (y 1 , y 2 )[y].
We denote this scheduled composition by Comp S (K 1 , K 2 ). Note that the scheduled composition of n channels can be defined by adapting the scheduler S to operate over n traces in the obvious manner.

Examples of Scheduled Composition

This section presents some example channels and schedulers that illustrate the main results of this paper. For simplicity they shall all limit their secrets to the set X B = {0, 1}, and their outputs to the set Y m = {m⟨0⟩, τ.m⟨0⟩, m⟨1⟩, τ.m⟨1⟩} for a parameter m.

Consider the channel

K 1 = (X B , Y m 1 ,C 1 )
where C 1 is given by Table 1. This channel can be considered as one that half the time simply outputs the secret via m 1 ⟨s⟩ and half the time outputs the exclusive-or ⊕ of the secret with 1 as in τ.m 1 ⟨s ⊕1⟩, with the τ representing the calculation effort. Note that this channel leaks 100% of the information about the secret. Also consider the channel

K 2 = (X B , Y m 2 ,C 2 )
where C 2 is given by Table 2. This channel is similar to K 1 , except that the internal action τ is observable when disclosing the secret rather than its exclusive-or. Again this channel leaks all the secret information.

When combining channels the rôle of the scheduler is very significant with respect to the information leakage. This section defines three types of simple schedulers for illustrating the results here.

The simplest scheduler is one that outputs the first and second observable outputs concatenated, i.e. given y 1 and y 2 outputs y 1 .y 2 .

Definition 8

The (left-first) deterministic sequential scheduler S DS is defined as follows:

S DS (y 1 , y 2 )[y] is 1 if y = y 1 .y 2 and 0 otherwise where y 1 ∈ Y 1 , y 2 ∈ Y 2 and y ∈ Y . Example 1 The scheduled composition Comp S DS (K 1 , K 2 ) w.

r.t. S DS has the same information leakage as the parallel composition

K 1 × K 2 .
This can be shown since it follows from the definition of S DS that, for each y ∈ Y , S DS uniquely identifies a pair (y 1 , y 2 ) of outputs. For instance, let us consider the prior distribution π on X 1 × X 2 defined by (0.15, 0.20, 0.30, 0.35). Then, for both of the composed channels, the mutual information is about 1.926 and the min-entropy leakage is about 1.515.

Next is the fair sequential scheduler S FS that fairly chooses between the first or second observable and produces that in its entirety before producing the other.

Definition 9

The fair sequential scheduler S FS is defined by Quantitative Information Flow for Scheduler-Dependent Systems

S FS (y 1 , y 2 )[y] def =      1 if y 1 = y 2 ∧ y = y 1 .y 2 0.5 if y 1 ̸ = y 2 ∧ (y = y 1 .y 2 ∨ y = y 2 .y 1 ) 0 otherwise.
Similar to the deterministic sequential scheduler, the information leakage can be proven to be equal to that of the parallel composition of channels for this example.

Example 2 The scheduled composition Comp S FS (K 1 , K 2 ) w.r.t. S FS has the same information leakage as the parallel composition K 1 × K 2 . This can be shown similarly to Example 1.

Note that the leakage preservation does not hold in general as illustrated in the following example.

Example 3 Consider when Y 1 = {τ, τ.τ} and Y 2 = {m⟨0⟩, τ.m⟨0⟩}. The observed output τ.τ.m⟨0⟩ can arise from S (τ, τ.m⟨0⟩) and S (τ.τ, m⟨0⟩), where S can be S DS or S FS . Thus, both the schedulers S DS and S FS may allow less information leakage than the parallel composition.

The third example scheduler is the fair interleaving scheduler S FI that evenly chooses the next action from the two observables.

Definition 10

The fair interleaving scheduler S FI is recursively defined as

S FI (y 1 , y 2 )[y] def =                0.5S FI (y ′ 1 , y 2 )[y ′ ] if y = α.y ′ ∧ y 1 = α.y ′ 1 ∧ y 2 = β .y ′ 2 ∧ α ̸ = β 0.5S FI (y 1 , y ′ 2 )[y ′ ] if y = β .y ′ ∧ y 1 = α.y ′ 1 ∧ y 2 = β .y ′ 2 ∧ α ̸ = β 0.5S FI (y ′ 1 , y 2 )[y ′ ] + 0.5S FI (y 1 , y ′ 2 )[y ′ ] if y = α.y ′ ∧ y 1 = α.y ′ 1 ∧ y 2 = α.y ′ 2 1 if (y = y 1 ∧ y 2 = / 0) ∨ (y = y 2 ∧ y 1 = / 0) 0 otherwise.
The fair interleaving scheduler S FI turns out to often have impact on the leakage compared to the parallel composition of channels. This can occur in a variety of ways and shall be explored in detail later. 4 Information Leakage to Observers

Observers

Many kinds of capabilities of observing systems have been considered; e.g. an observer for strong bisimulation ∼ s can recognise the internal action: τ.m⟨v⟩ ̸ ∼ s m⟨v⟩, while one for weak bisimulation ∼ w cannot: τ.m⟨v⟩ ∼ w m⟨v⟩. To model different kinds of capabilities of observation, we define an observer's views Z as the set of values recognised by the observer. For example, τ.m⟨v⟩ and m⟨v⟩ fall into two different views to an observer for strong bisimulation, but to the same view to an observer for weak bisimulation. We formalise the notion of an observer using a matrix that defines relationships between observable outputs of systems and the observer's views. In particular, we allow for probabilistic accuracy in observation; that is the observer may not be perfectly accurate in identifying an output.

Definition 11 (Generalised observer) An observer O is defined as a triple (Y , Z , Obs) consisting of a finite set Y of observables, a finite set Z of observer's views and an observer matrix Obs each of whose row represents a probability distribution; i.e., for all y ∈ Y we have ∑ z∈Z Obs[y, z] = 1. Each matrix element Obs[y, z] represents the probability that the observer has the view z when the actual output is y.

The observation matrix Obs describes the capability of the attacker to distinguish between traces. This capability of observation has been formalised as an equivalence relation between states of a system in prior work [START_REF] Biondi | Quantifying Information Leakage of Randomized Protocols[END_REF]. In fact, an equivalence relation ∼ between traces characterises a class of observers.

Definition 12 (∼-observer) Given an equivalence relation ∼ on Y , an observer (Y , Z , Obs) is called a ∼-observer if, for all y 1 , y 2 ∈ Y , y 1 ∼ y 2 is logically equivalent to Obs[y 1 , z] = Obs[y 2 , z] for all z ∈ Z.

For instance, we can consider the ∼ s -observer for strong bisimulation ∼ s and the ∼ w -observer for weak bisimulation ∼ w . Observe that ∼ s is the identity relation on traces here. Further, note that for every observer O, there exists an equivalence relation ∼ between traces such that O is a ∼-observer. This equivalence relation ∼ is defined by the following:

∼ def = {(y 1 , y 2 ) ∈ Y × Y | for all z ∈ Z, Obs[y 1 , z] = Obs[y 2 , z]}.
On the other hand, the observation matrix is not uniquely determined by the equivalence relation and therefore can express a wider range of observers' capabilities than the equivalence relation.

Among ∼-observers, we often consider observers that always have the same view on the same trace. Various kinds of bisimulations, or relations on observables, have been proposed and can be represented by various deterministic observers. Indeed, other kinds of relations can also be represented; consider an observer that cannot distinguish which source m i a value is output upon. This can be formalised by using the equivalence relation ∼ ch on traces that cannot distinguishes m 1 from m 2 .

The last example observer here effectively ensures no leakage by seeing all outputs as the same: Example 6 (Unit observer) An observer O = (Y , Z , Obs) is called a unit observer if Z is a singleton. It has the same view regardless of the outputs of the channel, thus can detect no leakage of the channel.

Observed Information Leakage

The amount of observed information leakage depends on the capability of the observer. To quantify this we introduce the notion of observed information leakage. Definition 14 (Observed information leakage) Let K = (X , Y ,C) be a channel and O = (Y , Z , Obs) be an observer. For each leakage measure L ∈ {I , L } and any prior π on X , we define observed information leakage by

L O (π, K ) = L(π, K • O) where K • O = (X , Z ,C • Obs) is the cascade com- position [18] of K and O. Similarly, for each L ∈ {S C , M C }, we define L O (K ) = L(K • O).

Quantitative Information Flow for Scheduler-Dependent Systems

We present properties of observed information leakage as follows. The first remark is that, for each equivalence relation ∼ on traces, all deterministic ∼-observers give the same observed leakage values. Proposition 1 Let π be any prior on X and K = (X , Y ,C) be any channel. For any equivalence relation ∼ on Y and any two deterministic

∼-observers O 1 , O 2 , we have L O 1 (π, K ) = L O 2 (π, K ) for L ∈ {I , L } and L O 1 (K ) = L O 2 (K ) for L ∈ {S C , M C }.
The following states that the deterministic ∼ s -observers and unit observers respectively have the maximum and minimum capabilities of distinguishing traces. That is, the deterministic ∼ s -observer can detect every behaviour of the channel accurately and does not alter the leakage of the channel in any manner, while the unit observers cannot detect any leakage of the channel.

Proposition 2 For each L ∈ {I , L }, 0 ≤ L O (π, K ) ≤ L(π, K ). For each L ∈ {S C , M C }, 0 ≤ L O (K ) ≤ L(K ).
In these inequations, the left equalities hold when O is a unit observer, and the right ones hold when O is a deterministic ∼ s -observer.

Next we compare the capabilities of generalised observers. Recall the composition-refinement relation ⊑ • on channels [START_REF] Mário | Measuring Information Leakage Using Generalized Gain Functions[END_REF][START_REF] Mciver | Abstract Channels and Their Robust Information-Leakage Ordering[END_REF]: A channel K 1 is composition-refined by another K 2 , written as K 1 ⊑ • K 2 , iff there exists a channel K ′ such that K 1 = K 2 • K ′ . Since the generalised observers are also channels, we can consider this ordering ⊑ • on observers. For example, the unit observer is composition-refined by ∼ w -observers, and the deterministic ∼ w -observer is by the deterministic ∼ s -observer. For another example, any probabilistic ∼ a -observer is composition-refined by the deterministic ∼ a -observer:

Proposition 3 Given any equivalence relation ∼ a on Y let O 1 = (Y , Z , Obs 1 ) and O 2 = (Y , Z , Obs 2 ) be two ∼ a -observers. If O 2 is deterministic then O 1 ⊑ • O 2 .
The composition-refined observer will observe less information leakage. Theorem 4 Let O 1 and O 2 be two observers such that O 1 ⊑ • O 2 . Then, for any prior π and any channel

K , we have L O 1 (π, K ) ≤ L O 2 (π, K ) for L ∈ {I , L } and L O 1 (K ) ≤ L O 2 (K ) for L ∈ {S C , M C }.
These results imply that no probabilistic ∼-observer detect more leakage than deterministic ones.

Examples of Deterministic Observers

Theorem 4 implies that the deterministic ∼ s -observer does not observe less information leakage than the deterministic ∼ w -observer.

Example 7 Let us consider the scheduled compositions in Examples 1 and 2 in Section 3.3. Both the composed channels leak all secrets without considering observers; i.e., they do so in the presence of ∼ s -observer. On the other hand, they leak no secrets to a weakly-bisimilar observer. For example, for each i ∈ {1, 2}, we define the deterministic ∼ w -observer O i as

({m i ⟨0⟩, τ.m i ⟨0⟩, m i ⟨1⟩, τ.m i ⟨1⟩}, {[m i ⟨0⟩] ∼ w , [m i ⟨1⟩] ∼ w }, Obs)
where Obs is the matrix given in Table 3. Applying the ∼ w -observer O i to both K 1 and K 2 yields the same matrix presented in Table 4. Then both channels leak no information to the ∼ w -observer. Therefore, the deterministic ∼ s -observer observes more information leakage than the deterministic ∼ w -observer also in this example.

The scheduled composition can also leak more information than the parallel composition (and even than each component channel) in the presence of imperfect observers. Example 8 (Observer dependent) Consider the scheduled composition of the channels K 1 and K 2 w.r.t. the fair interleaving scheduler S FI . By Example 4, the leakage of the scheduled composition w.r.t. S FI is less than that of the parallel composition in the presence of the deterministic ∼ s -observer.

However, the leakage of the scheduled composition is more than that of the parallel composition (and even than that of each component channel) when the ∼ w -observer O is being considered; e.g.,

L O (π, Comp S FI (K 1 , K 2 )) = 0.215 > 0 = L O (π, K 1 ×K 2 ) = L O (π, K 1 ) for π = (0.15, 0.20, 0.30, 0.35). view [m i ⟨0⟩] ∼ w [m i ⟨1⟩] ∼ w m i ⟨0⟩ or τ.m i ⟨0⟩ 1 0 output m i ⟨1⟩ or τ.m i ⟨1⟩ 0 1

Example of Probabilistic Observers

The notion of deterministic ∼-observers is useful to model various observers, but they may not cover all realistic settings. For example, when the internal action τ represents time to perform internal computation, observers may recognise it only probabilistically, for instance with probability 0.7. Then such probabilistic observers cannot be modeled as deterministic observers but as generalised observers, which quantify the capabilities of probabilistic observation. As far as we know, no previous work on quantitative information flow analyses have considered probabilistic observers.

Relationships between Scheduling and Observation

This section generalises the previous examples to show three kinds of results. First, we identify conditions on component channels under which leakage cannot be effected by the scheduled composition. Second, we show that scheduled composition can leak more or less information than the parallel composition, including results on the bounds of the information leaked. Third, we present an algorithm for finding a scheduler that minimises the min-entropy leakage/min-capacity under any observer

Information Leakage Independent of Scheduling

This section presents results for determining when the leakage is independent of the scheduler. Regardless of the scheduler and observer, the leakage of the scheduled composition is equivalent to that of the parallel composition under certain conditions on component channels that are detailed below.

Theorem 5 Let K 1 = (X 1 , Y 1 ,C 1 ) and K 2 = (X 2 , Y 2 ,C 2 ) be channels. Assume that, for any y 1 , y ′ 1 ∈ Y 1 and y 2 , y ′ 2 ∈ Y 2 , if Int(y 1 , y 2 ) ∩ Int(y ′ 1 , y ′ 2 ) ̸ = / 0 then y 1 = y ′ 1 and y 2 = y ′ 2 .
Then, for every scheduler S and observer O, the leakage of the scheduled composition is the same as that of the parallel composition.

By adding a stronger requirement to Theorem 5, we obtain the following corollary.

Corollary 6 Let K 1 = (X 1 , Y 1 ,C 1 ) and K 2 = (X 2 , Y 2 ,C 2 ) be channels. Assume that, for all (y 1 , y 2 ) ∈ Y 1 × Y 2 ,
α ∈ y 1 and β ∈ y 2 , we have α ̸ = β . Then, for every scheduler S and observer O, the leakage of the scheduled composition is the same as that of the parallel composition.

Quantitative Information Flow for Scheduler-Dependent Systems

Schedulers for Altering Information Leakage

This section considers when schedulers can alter the leakage of a scheduled composition. This is distinct from prior results where it has been shown that the composition cannot leak more information than the component channels [START_REF] Barthe | Information-theoretic Bounds for Differentially Private Mechanisms[END_REF][START_REF] Espinoza | Min-entropy as a resource[END_REF][START_REF] Kawamoto | Compositionality Results for Quantitative Information Flow[END_REF], since here more information can be leaked to imperfect observers.

In general scheduled composition can yield more or less leakage than the individual component channels or their parallel composition. This is illustrated by Example 8. Unfortunately heuristics for determining when more information is leaked end up being rather complicated and dependent on many relations between traces, interleavings, equivalences, and then subject to generalities about both schedulers and observers. Ultimately it is easier to show by examples that, for some channels, prior, and ∼-observer, there is a scheduler by which the scheduled composition leaks strictly more information than the parallel composition. Since this clearly holds by example, we consider a class of schedulers under which the scheduled composition does not leak more information than the parallel composition.

To define this we extend an equivalence relation ∼ on traces to probability distributions of traces: We say that two distributions D and D ′ on a set Y are ∼-indistinguishable (written as D ∼ D ′ ) if the deterministic ∼-observer cannot distinguish D from D ′ at all, i.e., for all equivalence class t ∈ Y /∼, we have

∑ y∈t D[y] = ∑ y∈t D ′ [y].
Using ∼-indistinguishability we define a scheduler that does not leak any behaviour of the system that the ∼-observer cannot detect.

Definition 15 Let ∼ be an equivalence relation on

Y 1 ∪ Y 2 ∪ Int(Y 1 , Y 2 ). A scheduler S on Y 1 and Y 2 is a ∼-blind scheduler when, for any two pairs (y 1 , y 2 ), (y ′ 1 , y ′ 2 ) ∈ Y 1 × Y 2 , we have y 1 ∼ y ′ 1 and y 2 ∼ y ′ 2 iff we have S (y 1 , y 2 ) ∼ S (y ′ 1 , y ′ 2 ).
For instance, the deterministic sequential scheduler S DS and the fair sequential scheduler S FS are ∼ wblind while the fair interleaving scheduler S FI is not. Note that ∼-blind schedulers do not leak any behaviour that would not be visible to the deterministic ∼-observers. Thus they do not gain more information from the scheduled composition w.r.t. ∼ than the parallel composition.

Theorem 7 Let π be a prior, K 1 and K 2 be two channels, O be a deterministic ∼-observer, and S be a ∼-blind scheduler. For each L ∈ {I , L } we have L O (π,

Comp S (K 1 , K 2 )) ≤ L O (π, K 1 × K 2 ). For each L ∈ {S C , M C } we have L O (Comp S (K 1 , K 2 )) ≤ L O (K 1 × K 2 ).
When S is also deterministic, the leakage relations become equalities.

For instance, since S DS and S FS are ∼ w -blind schedulers, the deterministic ∼ w -observers do not gain more information from the scheduled composition w.r.t. ∼ w than the parallel composition. In fact, they have the same leakage in Example 7.

The following result is about a heuristic for when leakage can be changed by the properties of the scheduler. This is presented here to clarify the properties.

Theorem 8 Let K 1 = (X 1 , Y 1 ,C 1 ) and K 2 = (X 2 , Y 2 ,C 2 ) be two channels. Assume that there exist y 1 , y ′ 1 ∈ Y 1 and y 2 , y ′ 2 ∈ Y 2 such that Int(y 1 , y 2 ) ∩ Int(y ′ 1 , y ′ 2 ) ̸ = / 0.
Then it is possible for the scheduledcomposition of K 1 and K 2 to alter the mutual information and min-entropy leakage for some prior.

Schedulers for Minimising Information Leakage

This section presents results for finding a scheduler that minimises the min-entropy leakage and mincapacity in the presence of any observer.

Theorem 9 Given any prior π, two channels K 1 , K 2 and any observer O, there is an algorithm that computes a scheduler S that minimises the observed min-entropy leakage L O (π, Comp S (K 1 , K 2 )) of the scheduled composition.

Proof: To find a scheduler S that minimises the observed min-entropy leakage L O (π, Comp S (K 1 , K 2 )), it is sufficient to find S that minimises the observed posterior vulnerability V (π,

Comp S (K 1 , K 2 ) • O). For (x 1 , x 2 ) ∈ X 1 ×X 2 and (y 1 , y 2 ) ∈ Y 1 ×Y 2 , let p(x 1 , x 2 , y 1 , y 2 ) = π[x 1 , x 2 ](C 1 ×C 2 )[(x 1 .x 2 ), (y 1 , y 2 )]. For each z ∈ Z let v z =max (x 1 ,x 2 )∈X 1 ×X 2 ∑ y 1 ,y 2 ,y p(x 1 , x 2 , y 1 , y 2 )S (y 1 , y 2 )[y]Obs[y, z] where (y 1 , y 2 ) and y range over Y 1 × Y 2 and Int(Y 1 , Y 2 ) respectively. Let Pos(y 1 , y 2 )[y] be the (|Y 1 | × |Y 2 |, |Int(Y 1 , Y 2 )|)-
matrix defined by the following: Pos(y 1 , y 2 )[y] = 1 if y can be obtained by interleaving y 1 and y 2 , and Pos(y 1 , y 2 )[y] = 0 otherwise.

To find a scheduler matrix S that minimises the observed posterior vulnerability, it suffices to solve the linear program that minimises ∑ z∈Z v z , subject to

• for each (x 1 , x 2 , z) ∈ X 1 ×X 2 ×Z , ∑ y 1 ,y 2 ,y p(x 1 , x 2 , y 1 , y 2 )S(y 1 , y 2 )[y]Obs[y, z] ≤ v z • for each (y 1 , y 2 ) ∈ Y 1 × Y 2 , ∑ y Pos(y 1 , y 2 )[y]S (y 1 , y 2 )[y] = 1.
Note that the second constraint means that each row of the scheduler matrix S must sum to 1. In this linear program, the scheduler matrix element S (y

1 , y 2 )[y] for each (y 1 , y 2 ) ∈ Y 1 × Y 2 and y ∈ Int(Y 1 , Y 2 )
and v z for each z ∈ Z are variables. We can solve this problem using the simplex method or interior point method. (In practice, we can efficiently solve it using a linear programming solver such as lp solve [2].) Hence we obtain a scheduler matrix S that minimises ∑ z∈Z v z . 2

In the above linear program the number of variables is

|Y 1 | × |Y 2 | × |Int(Y 1 , Y 2 )| + |Z |, and the number of constraints is |X 1 | × |X 2 | × |Z | + |Y 1 | × |Y 2 |.
Since the number of interleaved traces grows exponentially in the number of traces, the time to compute a minimising scheduler is exponential in the number of component traces. When the observer O is imperfect enough for |Z | to be very small, then the computation time improves significantly in practice. On the other hand, when the number of traces is very large, we may heuristically obtain a scheduler with less leakage by results in the previous section.

To obtain a scheduler that minimises the worst-case leakage value, it suffices to consider a scheduler that minimises the min-capacity.

Corollary 10 Given two channels K 1 , K 2 and any observer O, there is an algorithm that computes a scheduler S that minimises the observed min-capacity of the scheduled composition.

These two results give the minimum amount of leakage that is possible for any scheduling.

Example 10 Consider the channels K 1 , K 2 defined in Section 3.3. By Theorem 9, the minimum observed min-entropy leakage w.r.t. the prior (0.15, 0.20, 0.30, 0.35) is 1.237 under the deterministic ∼ s -observer, and 0.801 under the probabilistic observer defined in Example 9. By Corollary 10, the minimum observed min-capacity is 1.585 under the deterministic ∼ s -observer, and 1.138 under the probabilistic observer.

Since the channel capacity will not exceed the min-capacity [START_REF] Smith | Quantifying Information Flow Using Min-Entropy[END_REF], the minimum observed mincapacity obtained by the above algorithm gives an upper bound on the minimum channel capacity.

6 Case Studies

Sender Anonymity

In e-voting sender anonymity can be summarised as the issue of collecting votes from a number of voters and being able to expose the aggregate vote information while revealing as little as possible about how each voter voted. This can be solved by a general application of a mix network [START_REF] Chaum | Untraceable electronic mail, return addresses, and digital pseudonyms[END_REF] where all the votes are sent via mixing systems that output the votes in a manner that should not reveal how each voter voted. This can be represented here by each voter being an information-theoretic channel that outputs their vote. For example, consider a simple voting in which possible votes are 0 and 1 and each voter outputs the chosen vote via m⟨0⟩ or m⟨1⟩, respectively. Then each voter (indexed by i) can be represented by the channel K i = ({0, 1}, {m⟨0⟩, m⟨1⟩},C i ) where C i [k, m⟨k⟩] = 1 for k ∈ {0, 1} and each voter has a prior π i on {0, 1}. Observe that each such voter channel alone fully reveals the prior for the channel.

K 1 K 2 K 2 K 4 K 5 K A K S1 K B K S2 - - - - - - - 6 Y S2 Composed votes - π 1 π 2 π 3 π 4 π 5 Y 1 Y 2 Y 3 Y A Y 4 Y 5 Y S1 Y B
The scheduled composition of the voters represents the mix network with the schedulers representing the mixing algorithm and thus providing the ability to reason over their effect on information leakage. Consider the following problem with five voters K 1 to K 5 . As illustrated in Figure 2, the ballot of each voter is sent via intermediate severs (schedulers) K A , K B , K S1 that mix the order of ballots. The final system K S2 combines K S1 and K B to output all the votes according to some mixing.

Using the deterministic sequential scheduler S DS for all compositions reveals all information on how each voter voted. That is, the leakage is considered to be 5-bits (as each vote is 0 or 1). On the other hand, using the fair sequential scheduler S FS for all compositions leaks less information than S DS . When π is uniform and K is the composed channel in Figure 2 with the appropriate scheduling, we obtain L (π, K ) = 3.426 and I (π, K ) = 2.836. Observe that here the third voter's output can only appear in the 1st, 3rd, or 5th position in the final trace. This is repaired by using the fair interleaving scheduler S FI for all compositions that leaks even less information: L (π, K ) = 2.901 and I (π, K ) = 2.251.

A more interesting case is when different compositions use different schedulers. Since the votes do not contain any information about the system they came from, let alone voter. Using the fair sequential scheduler for K A and K B , and the fair interleaving scheduler for K S2 , along with a specially constructed scheduler for K S1 can reduce the information leakage to a minimum. Then the min-entropy leakage is 2.824 and the mutual information is 2.234. Note that when there is only one scheduler that receives all 5 ballots, the minimum min-capacity of the composed system (over all possible schedulers) is 2.585.

The example can be extended further by adding τ steps before votes to indicate time taken for some parts of the process. For a simple example, consider when voters 1 and 2 have a τ step before their vote to represent the time taken, e.g. as indicative of voting order, or the time taken for the extra mixing step. In the presence of all fair interleaving schedulers, the observed min-entropy leakage and the mutual information are respectively 3.441 and 2.785 under the perfect observer. However, these shift to 3.381 and 2.597, respectively, under the deterministic ∼ w -observer.

Side-Channel Attacks

Consider the small program shown in Figure 3, where an observable action is repeated in a loop. This program captures, for instance, some aspects of decryption algorithms of certain cryptographic schemes, such as RSA. Intuitively, X[ ] is the binary array representing a 3-bit secret (e.g. 011), which corresponds to secret decryption keys. The timing of the algorithm's operation reveals which bit of the secret key is 1, since the observable-operation m⟨1⟩ can be detected, perhaps as power consumption, response time, or some other side-effect of the algorithm [START_REF] Paul | Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems[END_REF]. We denote by K the channel defined by this program.

for(i = 0; i < 3; i++) { tau; if(X[i] = 1) { m<1>; //observable-operation } } Consider composition of K with itself, e.g., when applying the algorithm to different parts of the message in parallel. Clearly if the parallel composition is taken then both instances of K will leak all their information about the key. On the other hand, the scheduled composition may have less leakage.

We first consider the case each instance of the component channel K receives a different secret bit string independently drawn from the uniform prior. This captures the situation in which each decryption operation uses different secret keys. When the fair interleaving scheduler mixes the two traces, the min-entropy leakage and the mutual information are respectively 4.257 and 3.547 in the presence of the perfect observer, and 2.807 and 2.333 in the presence of the deterministic ∼ w -observer.

Next we consider the case where both instances of K share the same secret key which has been drawn from the uniform prior. When the fair interleaving scheduler mixes the two traces, the minentropy leakage and the mutual information are respectively 3.000 and 3.000 (all 3 bits of the secret key are leaked) under the perfect observer, and 2.000 and 1.811 under the deterministic ∼ w -observer.

More interesting is to consider the case where the observer is only able to detect approximate information through the side-channel. Consider the observer O that only probabilistically observes actions according to the matrix in Figure 4. Here / 0 indicates that nothing is detected by the attacker not even a τ. For example, applying this observer to the trace τ.τ.τ may yield τ.τ when one τ is not observed (represented / 0 in the matrix). Such an observer is less effective even when applied to the parallel composition of channels. However, this applies even further when applied to any scheduled composition since the loss of information through poor detection cannot even be limited to one channel or the other. Thus, a trace of length 5, even from a leaky scheduler such as the (left-first) sequential scheduler, would leak less than the parallel composition (since it would be clear which composite channel had been poorly observed).

For instance, let us consider the case each instance of K independently receives a secret from the uniform prior and the fair interleaving scheduler is used. Then the min-entropy leakage and the mutual information are respectively 3.306 and 1.454 under this probabilistic observer. If we consider the case both instances of K shares the same secret, then the leakage values are respectively 2.556 and 1.924.

Related Work

Regarding schedulers there are a variety of studies on relationships between schedulers and information leakage [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF][START_REF] Andres | Information Hiding in Probabilistic Concurrent Systems[END_REF]. In [START_REF] Canetti | Analyzing Security Protocols Using Time-Bounded Task-PIOAs[END_REF] the authors consider a task-scheduler that is similar to our schedulers, albeit restricted to the form of our deterministic scheduler. The schedulers in this paper are also similar to the admissible schedulers of [START_REF] Andres | Information Hiding in Probabilistic Concurrent Systems[END_REF]. Both are defined to depend only upon the observable outputs, that is the traces they schedule. This avoids the possibility of leakage via the scheduler being aware of the intended secret directly and so leaking information. Differently to admissible schedulers, here the scheduler can be probabilistic, which is similar in concept to the probabilistically defined (deterministic) schedulers of [START_REF] Zhang | Model Checking Interactive Markov Chains[END_REF], although they explore scheduling and determinism of Markov Chains and not information leakage.

Most work on schedulers has focused on preventing any leakage at all, indeed the problem is typically defined to prevent any high/secret information leaking. This in turn sets extremely high requirements upon the scheduler, and so proves to be difficult to achieve, or even impossible. Here we take an approach to scheduling that allows for probabilistic schedulers and so reasoning about the quantitative information Quantitative Information Flow for Scheduler-Dependent Systems leakage, rather than total leakage. Thus we permit schedulers that can be daemonic or angelic, as well as many in between that may closer resemble the behaviour of real world systems.

Regarding observers there is little prior work in quantitative information flow and quantifying the capability of the observer. [START_REF] Biondi | Quantifying Information Leakage of Randomized Protocols[END_REF] has some similarity where they formalise an equivalence of system states similar in style to the deterministic ∼-observers here. However, this does not model observers as part of information-theoretic channels, hence does not allow the probabilistic behaviour of observers.

Conclusions and Future Work

We have introduced the notion of the scheduled composition of channels and generalised the capabilities of the observers to reason about more systems. Then we have presented theories that can be used as heuristics to detect when scheduled composition may have an effect on the information leakage. This determines when scheduled composition is a potential risk/benefit to a scheduler-dependent system. Scheduling can both leak more information, or less information to an observer depending on many factors, while some leakage bounds can be obtained for schedule-composed channels. Further, we have shown an algorithm for finding a scheduler that minimises the leakage of the scheduled composition.

The work here provides a foundation for continuing research into concurrent behavior, including interactive systems. Here we have limited the systems to finite sets of secrets and observables since this aligns with the discrete version of leakage calculations. By shifting to continuous domains we can investigate some systems with infinite secrets or observables. Similarly the schedulers here assume finite traces and are typically defined over the entire possible traces. However, many do not require this, and can be defined only upon the next action in the trace. This allows for alternate definitions without changing the results, and easier applicability to infinite settings.

Figure 1 :

 1 Figure 1: Parallel composition and scheduled composition

Definition 13 (

 13 Deterministic observer) We say that an observer (Y , Z , Obs) is deterministic if each probability in Obs is either 0 or 1; i.e., for all y ∈ Y , there exists a unique z ∈ Z such that Obs[y, z] = 1.For any deterministic ∼-observer (Y , Z , Obs) and any y 1 , y 2 ∈ Y , we have y 1 ∼ y 2 iff, for all z ∈ Z , we have Obs[y 1 , z] = Obs[y 2 , z] ∈ {0, 1}. Then this observer always detects the equivalence class [y] ∼ of the output y from any given view z. For this reason, when defining a deterministic ∼-observer, we typically take the set Z of views as the quotient set of Y by ∼, and for any y ∈ Y and z ∈ Z , Obs[y, z] = 1 iff z = [y] ∼ . For example, consider the deterministic observers corresponding to ∼ s . Example 5 (Deterministic ∼ s -observer) A deterministic ∼ s -observer (Y , Z , Obs) satisfies the property that, for any distinct y 1 , y 2 ∈ Y , there exists a z ∈ Z such that either Obs[y 1 , z] = 0 and Obs[y 2 , z] = 1 or Obs[y 1 , z] = 1 and Obs[y 2 , z] = 0. Therefore this observer always detects the output y of the channel from any given view z. For this reason we call a deterministic ∼ s -observer a perfect observer.

Figure 2 :

 2 Figure 2: Structure of composed channels for voters

Figure 3 Figure 4 :

 34 Figure 3: Decryption algorithm

  Definition 4 For two sets Y 1 , Y 2 of observables, the interleaving Int(Y 1 , Y 2 ) over Y 1 and Y 2 is defined by Int(Y 1 , Y 2 ) = Int(y 1 , y ′ ). For n sets Y 1 , Y 2 , . . . , Y n of observables, the interleaving Int(Y 1 , Y 2 , . . . , Y n ) is defined analogously.

	∪ y 1 ∈Y 1 ,y 2 ∈Y 2 Int(y 1 , y 2 ). The definition of interleaving is extended from two traces to n ∪ traces as follows: Int(y 1 , y 2 , . . . , y n ) = y ′ ∈Int(y 2 ,...,y n )

Table 2 :

 2 Channel matrix C 2

Table 3 :

 3 Observer matrix Obs view [m i ⟨0⟩] ∼ w [m i ⟨1⟩] ∼ w

	secret	0 1	0.5 0.5	0.5 0.5

Table 4 :

 4 Composed matrix C i • Obs

Formally, we introduce K sep = ({sep}, {sep}, (1)) to consider the sequential execution of K 1 , K sep and K

in this order.

* This work has been partially supported by the project ANR-12-IS02-001 PACE, by the INRIA Equipe Associée PRINCESS, by the INRIA Large Scale Initiative CAPPRIS, and by EU grant agreement no. 295261 (MEALS). The work of Yusuke Kawamoto has been supported by a postdoc grant funded by the IDEX Digital Society project.

Quantitative Information Flow for Scheduler-Dependent Systems

A Omitted Proofs

In this section we present proofs that are omitted in the main sections.

Proposition 1 Let π be any prior on X and K = (X , Y ,C) be any channel. For any equivalence relation ∼ on Y and any two deterministic

Proof: The two observer matrices of O 1 and O 2 are identical when removing the columns with all zeros and reordering the other columns. Therefore the observed leakage values with O 1 and O 2 coincide. 2

In these inequations, the left equalities hold when O is a unit observer, and the right ones hold when O is a deterministic ∼ s -observer.

Similar for the case L = S C . If L = L , then it follows from a property of the cascade composition [START_REF] Espinoza | Min-Entropy Leakage of Channels in Cascade[END_REF] that

When O is a unit observer, the cascade

When O is a deterministic ∼ s -observer, we obtain an identity matrix from Obs by removing the column with all zeros and by sorting the order of columns. Therefore, for each L ∈ {I , L }, we have

Proof: For L ∈ {I , S C }, we obtain the claim from the data processing inequality. For L ∈ {S C , M C }, the claim follows from a result for cascade composition [START_REF] Espinoza | Min-Entropy Leakage of Channels in Cascade[END_REF]. 2

Then for every scheduler S on Y 1 and Y 2 and every observer O,

yields the interleaved trace y. That is, given any output y of the scheduled composition, the observer uniquely identifies the component traces (y 1 , y 2 ). Thus the leakage of the scheduled composition is equivalent to that of the parallel composition.

2 ) be two channels. Assume that, for all (y 1 , y 2 ) ∈ Y 1 × Y 2 , α ∈ y 1 and β ∈ y 2 , we have α ̸ = β . Then, for every scheduler S on Y 1 and Y 2 and for every observer O,

Proof: Since there are no actions shared between the traces of Y 1 and Y 2 , we have that, for any

By Theorem 5 the claim follows. 2

Theorem 7 Let π be a prior, K 1 and K 2 be two channels, O be a deterministic ∼-observer, and S be a ∼-blind scheduler. For each L ∈ {I ,

When S is also deterministic, the leakage relations become equalities.

Proof: By Definition 15, the cascade

Hence the information leakage of the scheduled composition w.r.t. ∼ is upper-bounded by that of the parallel composition.

When S is also deterministic, then the cascade S O is a deterministic ∼-observer. By Proposition 1 the leakages under the observers S O and O are equivalent.

2

Then it is possible for the scheduledcomposition of K 1 and K 2 to alter the mutual information and min-entropy leakage for some prior.

Proof: By assumption, we have either y 1 ̸ = y ′ 1 or y 2 ̸ = y ′ 2 . Consider when y 1 ̸ = y ′ 1 and y 2 = y ′ 2 . We have that there exists y ∈ Int(y 1 , y 2 ) ∩ Int(y ′ 1 , y 2 ) and so any scheduler S where S (y 1 , y 2 )[y] > 0 and S (y ′ 1 , y 2 )[y] > 0 will yield a matrix where observable y does not uniquely identify y 1 or y ′ 1 , yet each row of the matrix for Y 1 × Y 2 does uniquely identify each y 1 ∈ Y 1 . Then conclude by observing that this creates an inequality on the information leakage of Comp S (K 1 , K 2 ) compared to (K 1 × K 2 ). 2

Corollary 10 Given two channels K 1 , K 2 and any observer O, there is an algorithm that computes a scheduler S that minimises the observed min-capacity M C O (Comp S (K 1 , K 2 )) of the scheduled composition.

Proof: The min-capacity is obtained when the prior π is uniform. Therefore we obtain a minimizing scheduler S by the algorithm in Theorem 9 using the uniform prior π.