Thibaut Le Naour
email: tlenaour@gmail.com

Nicolas Courty
email: courty@univ-ubs.fr

Sylvie Gibet
email: sylvie.gibet@univ-ubs.fr

Sylvie Gibet 2018 Kinematic

Hal

Kinematic driven by distances

Keywords: Character Animation, Kinematic, Inverse kinematic, Motion editing, Geometrical constraints

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

I. INTRODUCTION

Traditionally, a character's animation is represented by a series of skeletons over time. A skeleton is a hierarchy of joints between which distances are fixed. In inverse kinematics problem, the aim is to move an effector (typically the end of the chain) to a point x. The animated chain is represented by a vector q of positions and orientations of the joints which describes the skeleton. In a direct kinematic problem, for a chain with n joints, we define the function f : SO(3) n → R 3n such that :

x = f (q). (1)
Inversely, in a problem of inverse kinematic, we obtain :

q = f -1 (x), (2)
where f is the set of transformations to apply to the chain q to move the effector to bmx. We note some observations about the classic inverse kiniematic :

• the expression of the task is given by the definition of a point x in the space to reach ; • the previous equation 2 is highly non linear ;

• the systems are generally redundant in relation to the problem to be solved. Indeed, the number of constraints is often considerably lower than the number of unknowns ; • although treated and solved in the literature, inverse kinematics is limited concerning its resolution in the case of multiple effectors. As stated, the problem reaches limits in terms of complexity to satisfy several target constraints. Thus, to be accomplished, the task is rarely expressed in a global way on the whole skeleton but rather introduced by a set of tasks between which priorities must be expressed. In our approach, our aim is to characterize a posture not by q, but by a set of distances. In this case, the motion of an articulated system is driven by the specification of distance relationships between points of the system. By characterizing motion in the distance space, the skeleton chain is represented by a vector w describing a set of positions associated with these distances. Considering n joints associated with m distances, we can express the problem of direct kinematic with a new function h : R m → R 3n :

x = h(w).

(

Inversely, in a problem of inverse kinematic, we use the notation :

w = h -1 (x). (4)
Advantages of the method. As the traditional inverse kinematic, the formulated problem is highly non linear. Our approach will therefore be a variational approach. However, the advantage of the proposed formulation is related to the manner of defining tasks through distances. We will see through a set of tests that this new way of expressing tasks greatly simplifies the work dedicated to animation control, notably by providing an implicit specification of contacts (in opposition to an explicit spatial definition of contact zones). The latest studies in this domain [START_REF] Ho | Character motion synthesis by topology coordinates[END_REF], [START_REF] Ho | Spatial relationship preserving character motion adaptation[END_REF], shows the interest of the community for this problem. Moreover, our system allows to animate all of the skeleton in an unified way, so the the resolution of one or more tasks simultaneously is simple. Finally, we will see that through a decoupling of the invariant information (distances which represent fixed lengths of the skeleton segments) and the information which change over time (the other distances), we give priorities between constraints and thus give a style to the animation.

Outline of this paper. First, we define the problem from the expression of the distances (section 3). In this context, a skeleton is characterized by a set of points, each point expressing itself in relation to the others in terms of distances. Then, we propose a method to solve the problem of direct kinematic and highlight how with this spatial representation of the skeleton, we formulate the problem of inverse kinematic (sections 4 et 5). Finally, we propose a set of tests to validate our method (section 6).

II. RELATED WORK

Inverse kinematic and applications Inverse kinematic techniques have been widely studied in recent decades, in a graphic context [START_REF] Welman | Inverse Kinematics and Geometric Constraints for Articulated Figure Manipulation[END_REF], [START_REF] Zhao | Inverse kinematics positioning using nonlinear programming for highly articulated figures[END_REF] but especially robotic [START_REF] Wolovich | A computational technique for inverse kinematics[END_REF], [START_REF] Nakamura | Inverse kinematics solutions with singularity robustness for robot manipulator control[END_REF]. These methods give rise to powerful tools, both to generate new motions, and also as components of more specific methods: adaptation of motions to new constraints [START_REF] Gleicher | Retargetting motion to new characters[END_REF], [START_REF] Choi | Online motion retargetting[END_REF], [START_REF] Baerlocher | Using an intermediate skeleton and inverse kinematics for motion retargetting[END_REF], [START_REF] Kulpa R | Morphologyindependent representation of motions for interactive humanlike animation[END_REF], [START_REF] Callennec | Interactive motion deformation with prioritized constraints[END_REF], [HRE * 08], reconstitution of postures based on virtual markers [START_REF] Varona | Adding image constraints to inverse kinematics for human motion capture[END_REF], [START_REF] Hauberg | Predicting articulated human motion from spatial processes[END_REF], or the reconstruction of motions partially acquired from capture methods [START_REF] Grochow | Style-based inverse kinematics[END_REF], [START_REF] Aristidou | Fabrik: A fast, iterative solver for the inverse kinematics problem[END_REF]. The best known approaches have been the subject of comparative studies as part of the reconstruction of different classes of movement [START_REF] Unzueta | Fullbody performance animation with sequential inverse kinematics[END_REF].

However, the difficulty to constraint this kind of problem and the redundancy of the considered articulated chain (due to the hierarchical imbrication of several joints), implies the use of secondary tasks which over-constraint the problem [START_REF] Boulic R | A robust approach for the control of the center of mass with inverse kinetics[END_REF], [START_REF] Yamane | Natural motion animation through constraining and deconstraining at will[END_REF], [START_REF] Baerlocher | An inverse kinematics architecture enforcing an arbitrary number of strict priority levels[END_REF], [START_REF] Sentis | Synthesis of whole-body behaviors through hierarchical control of behavioral primitives[END_REF]. Among these constraints, we can note the angular limits [START_REF] Courty | Through-theeyes control of a virtual humanod[END_REF], the control of the balance of the character [START_REF] Boulic R | A robust approach for the control of the center of mass with inverse kinetics[END_REF]. Recent studies focused on the imbrication of several levels of constraints [START_REF] Baerlocher | An inverse kinematics architecture enforcing an arbitrary number of strict priority levels[END_REF], [START_REF] Callennec | Interactive motion deformation with prioritized constraints[END_REF], [START_REF] Sentis | Synthesis of whole-body behaviors through hierarchical control of behavioral primitives[END_REF] using priority levels. Here, the difficulty is to propose a system which couples some antagonist tasks without having a priori ideas on the global realization of the instructions.

From the point of view of the resolution of the inverse problem, most of the time, the existing algorithms are based on a descent of gradient exploiting an inversion of a Jacobian numerically evaluated. One of the most effective methods consists in calculating the Moore-Penrose pseudo-inverse matrix associated with a dumping function [START_REF] Maciejewski | Dealing with the ill-conditioned equations of motion for articulated figures[END_REF]. However, there are several alternatives to this operation: sensorimotor approaches [START_REF] Gibet | A self-organised model for the control, planning and learning of nonlinear multivariable systems using a sensori-feedback[END_REF], probabilistic approaches [START_REF] Grochow | Style-based inverse kinematics[END_REF] or Bayesian inference [START_REF] Courty | Inverse kinematics using sequential Monte Carlo methods[END_REF]. Note also the possibility of using information collected from movements captured used as reference poses in the processes of optimisation [START_REF] Grochow | Style-based inverse kinematics[END_REF], [START_REF] Carvalho | Interactive Low-Dimensional Human Motion Synthesis by Combining Motion Models and PIK[END_REF], [TWC * 09], [START_REF] Raunhardt | Motion constraint[END_REF]. These approaches do not work directly in the space of the poses but rather in latent spaces (obtained by methods as the principal components analysis), which induces an over-constrained problem and gives in an implicit way the correlations which can exist between certain articulations. Note here that in the proposed method, the use of reference poses, defined as a set of distances to be respected, plays a similar role to these given-based approaches.

Other methods propose to solve the problem of inverse kinematics by using, not the space of orientations but that of positions (Euclidean space). Thus, the FABRIK [START_REF] Aristidou | Fabrik: A fast, iterative solver for the inverse kinematics problem[END_REF] method proposes a new algorithm of inverse kinematics, by traversing the chain forwards and backwards in a finite number of iterations. The main interest of this approach lies in the possibility of controlling multi-effector systems but also in its speed of execution. This method, which is expressed as a sequence of local geometric constructions, does not guarantee the optimality of the solution obtained.

In the method called "Particle IK Solver" citehecker08, the character is represented by a set of 3D particles (joint positions). The proposed method is a method of iterative resolution under constraints, which is based on a set of ad hoc preconditions and operates in two distinct phases applied successively to the different parts of the body to be animated. This problem decomposition allows local control and provides flexible and customizable solutions that preserve the style of movement. Ho et al [START_REF] Ho | Spatial relationship preserving character motion adaptation[END_REF] are also interested in a skeleton and mesh representation in the form of a point cloud. But contrary to the two previous approaches, the problem of adaptation of movement (in particular morphological adaptation) is formalised as a global problem of spatio-temporal optimisation. The position variations are calculated from the minimization of a sum of energy quantities (deformation, acceleration, energy stress). Finally, a new IK resolution method, based on distance constraints is proposed in robotics [HR06]. This geometric method consists in parameterizing the system by inter-joints distances, and in reformulating the problem from the resolution of a system of linear inequalities.

Similar to previous approaches, our method represents the animated character from a set of Cartesian positions. As in [START_REF] Aristidou | Fabrik: A fast, iterative solver for the inverse kinematics problem[END_REF] and [HR06], our method allows to manage multiple effectors and graph with cycles. However, our method differs essentially in the IK resolution method. It is an iterative, global, and non-linear optimization process. A set of distances (intra-skeleton and distances to the environment) is separated into two distinct subsets of constraints (primary and secondary) that are directly exploited in the optimization process. In addition, secondary constraints are projected into the kernel of the main task, which is an interesting contribution of the method.

Distances, topologies The originality of our method is based on the use of distance information as a relevant representation space from the point of view of the definition of inverse kinematics tasks. This formulation is inspired by existing work in the field of computational biology, and more particularly in the calculation of molecular conformations [START_REF] Havel | Distance geometry: Theory, algorithms, and chemical applications[END_REF]. In this context, only the information of distances between the different atoms of the molecules is known (in particular thanks to magnetic resonance techniques). This information allows to deduce the global topology of the molecule. Many methods exist. Either, they are based on a progressive construction of the molecule [START_REF] Wu Z | A geometric build-up algorithm for solving the molecular distance geometry problem with sparse distance data[END_REF], or on operational research methods such as separation and evaluation [START_REF] Mucherino | A parallel version of the branch & prune algorithm for the molecular distance geometry problem[END_REF]. A recent state of the art of these methods is given in [START_REF] Liberti | Molecular distance geometry methods: from continuous to discrete[END_REF]. Note here that we differentiate our study from these studies through the use of a human skeleton, where the number of rigid distances between two joints is much less than the number of couples of joints. In these studies, the general trend is rather reversed in the case of molecules (highly over-constrained problem), this requires more complex optimization procedures integrating uncertainty on distance knowledge.

Geometrical Methods Other approaches, such as spectral analysis of the metric matrix of the point cloud [START_REF] Sippl | Solution of the embedding problem and decomposition of symmetric matrices[END_REF], are used to determine the coordinates of the points. However, this method requires knowledge of all the exact distances (respect for triangular inequalities). Finally, the methods introduced in the field of computer-aided design propose solving sytems with geometric constraints such as the distances between two points or the angle between two vectors. The resolution of such systems has given rise to several methods presented by Jermann et al [START_REF] Jermann | Modélisation géométrique par contraintes[END_REF]. We note that those using gradient descents (Newton, by homotopy), have the advantages of being fast and give approximate results in the absence of a solution.

III. KINEMATIC DRIVEN BY DISTANCES : FORMALIZATION

A. Distance definitions

Our study focuses on the animation of a skeleton in the metric space. Each joint is geometrically represented by a point in R 3 . By using distances, we want to describe the 'gap' of a joint with the others joints of the skeleton or with points of the space. More precisely, a skeleton is represented by a graph G = (V , E, d) where V is the set of points (center of joints), E the set of edges which link the points of V and d the set of distances of V × V → R + . We note that d ij is the Euclidean distance between the point x i and the point x j , for all (x i , x j ) ∈ E. We define the spatial structure of this graph by the set of equations :

∀(x i , x j ) ∈ E, x i -x j = d ij , (5)
where . is the Euclidean norm. To simplify the notation, we will use in the remain of the paper indifferently the notation x i to represent the point of V or the vector --→ Ox i . Our problem can be formulated as follows : from a sufficient set of distances, the aim is to find the positions of the points (and therefore joints) in the space R 3 .

Each point of V is potentially associated with a number of distances, which depends of the topology of the graph at this point. Note that to infer a point x i in the space, it is sufficient to dispose of four known points which are distinct two by two, associated with their respective distances with the point x i . This means that in some cases we can simplify the problem posed in equation (5).

Numerically, solve such equations is hard. As we saw before, there are several methods. The methods using a spectral approach respond well at this problem but are practical only when all distances are known and accurate (respect of triangular inequalities). We choose to use optimization methods that enable to have close results in the cases where the distances are not accurate, or to reduce the space of solutions if all of distances are not known.

B. Formulation par un problme de minimisation

To solve the previous problem using optimization methods, we reformulate the equation (5) by a minimization problem of energy W such that :

W = arg min X E ( x i -x j 2 -d 2 ij ) 2 , (6)
where X = (x 1 , x 2 , ..., x n ) is the vector of unknown to determine, with n = |V | and m = |E|.

Note that in the equation ( 6), we perform a quadratic penalization of the error. The advantage is to guarantee a positive error for each equation, which implies that several errors can not cancel each other. This point improve the stability of our algorithm.

We note also that the equation (6) is a system of equation non linear.

We will call in the remain of this paper constraints, the rules that the system has to follow We will call in the following article constraints, the rules that must satisfy feasible solutions of the problem. Among these rules, the preservation of distance 5 (constraint of distance) or the equality between a point and an other (g(x) = x T ). Apply to a skeleton, the aim of the problem is to associate for each joint a sufficient count of constraints.

In order to describe more precisely the optimization method, we discuss in the next section only about the distance constraints concerning the points {x 1 , ..., x n }. These constraints can be written by a system of equations F of m objectives functions where each function takes equal distance between two points x i and x j as :

f ij (x i , x j ) = ( x i -x j 2 -d 2 ij ) 2 = 0. (7)
Thus, we want to solve the system of equations F (X) = 0, where F = (f 11 , ..., f 1n , ..., f mn ) T is the vector of objectives functions and X = (x 1 , x 2 , ..., x n ) T is the vector of unknown variable.

IV. METHODS OF OPTIMIZATION DEDICATED TO THE RESOLUTION OF SYSTEM OF EQUATIONS

The system of equations being not linear so we use a gradient descent approach as the Newton method. This method has the advantage to be fast and sufficient stable for our problem. Indeed, this technique introduce small change from a posture to another between each iteration of the algorithm. This is an advantage to produce animation which requires a temporal continuity. Newton's formula applied to our problem is written:

X k+1 = X k -J F (X k ) -1 F (X k ), (8)
where X k is the vector X obtained at the iteration of the optimization k and J F (X k ) is the Jacobian matrix of F (X k ) for the point X k . The Jacobian matrix J stacks the partial derivatives of all constraints of the problem F . The size of J is m × n (m × n constraints for n × 3 unknown) : We note that the previous equation gives us a general definition of the problem and hat it does not necessarily lead to a number of functions equal to the number of unknown variables. Indeed, the size of the system depends on the number of constraints given by the user. So we can obtain underdetermined problems similar to standard inverse kinematics, with more unknowns than constraints to respect. In contrast, our method simply adds distance constraints reducing the space of solution, until obtaining over-constrained problems (more constraints than unknowns) . Mathematically, these situations lead to Jacobian matrices that are not necessarily square , or of full rank . We use the pseudo-inverse matrix (or inverse of Moore-Penrose ) J + which is a generalization of the inverse matrix characterizing any matrix m × n(m > n) such that J + = (J T J ) -1 J T . The calculation of the pseudoinverse is performed by the method of singular values decomposition ( SVD ), and the evaluation of the Jacobian matrix is performed through the analytical expression of the gradient of the distance constraint between two points. So for a matrix element J evaluated at points x i and x j in R 3 , the gradient is written:

J (x 1 , . . . , x n ) =   
∂f ij ∂x j (x i , x j ) = -4.(x i -x j ).f ij (x i , x j ) (10)

V. MOTION ADAPTATION AND INVERSE KINEMATIC

To solve problems of pure inverse kinematics, the model described above is fully satisfactory. If we consider an articulated chain fixed at one end, knowing the initial posture and a target to be reached by the other end, it is enough to give the system the constraints of distance between the adjacent joints of the skeleton.

The problem thus formulated allows us to replay a movement or to solve the inverse kinematics by minimizing iteratively at each key position of the animation the various constraints of distance. In order to adapt a movement, it is necessary to introduce new concepts and improve the previous optimization method. We can differentiate two types of distance constraints (figure reffig:constraintsHardSoft):

• Hard constraints: these are the constraints that must be imperatively respected. For example, they may be invariant distances over time which are the distances between adjacent joints in the skeletal hierarchy. They correspond to the segments. These are also the target constraints of inverse kinematics, such as the contact of a foot with the ground represented by a zero distance between the foot and a plane. For these constraints the functions must be null at the end of the iteration of the optimization loop. • Soft constraints: these are the other distances in the graph. In the context of direct kinematics, they change over time and characterize the animation. The introduction of these constraints is motivated by the need to give priority to certain constraints over others. In the context of motion adaptation, we rely on a reference motion calculated in the space of distances to which we add a task via hard constraints. This induces a conflict between the constraints: the length of the segments as well as the task added are constraints to be satisfied in priority (hard constraints), whereas the distances which characterize the spatial positioning of the joints of the reference posture constitute properties, that we want to preserve at best (soft constraints). Thus, the system defined is finally over-constrained. We therefore propose a modification of the Newton algorithm which consists in adding a secondary task (soft constraints) which is projected in the solutions space of the main task (hard constraints). Similarly to the formulation proposed by Boulic et al [START_REF] Callennec | Interactive motion deformation with prioritized constraints[END_REF], this allows incorporating hard and soft constraints into the same algorithm, by taking account of the priorities between constraints. Our algorithm becomes:

X k+1 = X k -J + 0 F (X k ) + (I -J + 0 J 0 )J + 1 G(X k ) (11
) whre X k is the vector of positions of joints to determined. To simplify the notations, J + F0 (X k ) and J + F1 (X k ) are written J + 0 and J + 1 . F (X k ) and G(X k ) respectively represent the objective functions associated with hard and soft constraints, and J + 0 and J + 1 are the pseudo-inverse of the associated Jacobians. (I -J + 0 J 0 ) is an operator of projection that guaranteesthe realization of G(X k ) will not affect the realization of F (X k ).

VI. RESULTS

In order to validate our method, we test it on several case studies. Thus, we highlight the convergence of the method and the importance of defining the tasks to be accomplished. First of all we are interested in the task of motion tracking which has for objective to replay an animation. In a second step, we experiment our method on inverse kinematic situations, notably by comparing the results with those obtained by a traditional kinematic method. Finally we test our method on a motion adaptation experiment. Our tests are all performed in real time (10 frames per second for the slowest animation). They are performed by a single process with a processor running at 2.3 GHz. We tested and used two mathematical libraries ( [START_REF] Davies R | Newmat c++ matrix library[END_REF]), [GJ * 10]) to validate our results.

A. Replay

In order to validate the ability of our method to calculate an animation in distance space, our first test is an example of replay, which represents the reproduction of a S source motion (captured data) to a C target motion for identical skeletons. We define four points two by two distinct in 3d space (canonical basis and origin). For each time step, after calculating the joint positions of S, we extract for each skeletal joint S the distances with these four points. Finally we incorporate these distances into our system. More precisely, for a skeleton with n joints, we define a problem of 4n constraints for 3n unknown. Our test is performed on a walking motion stored in bvh format from the CMU database.

In order to validate our method, we evaluate the convergence of the algorithm, and we show (figure 3) the real-time followup of the target animation. The figure 2 clearly shows the success of convergence. More precisely, we can deduce that the minimization of errors for each constraint at the end of 10 iterations is equal to zero (remember that the minimization was squared). This results correspond to zero distance between the joints of S and C, and visually by an identical follow-up of the animation C on S (figure 3). This experiment also shows the robustness of the method: indeed, as illustrated in figure 3, the optimization algorithm can adapt to large variations in initial values (posture very different from the reference posture). Character animation has the advantage of having a reference pause (bind pose) that introduces an initial vector into the iteration of Newton already very close to the solution.

B. Inverse kinematic

1) Rich a target with an articulated chain: Our second test (figure 4) concerns a simple example of inverse kinematics. The goal is that the extremity of an articulated chain bme 1 reaches a target bmc, the other extremity bme 2 being attached to another point bmp. For this experiment, we construct an articulated chain consisting of 10 joints, each of them spaced with the same distance from the adjacent joint. The problem is: we give to the system the 9 constraints specific to the articulated chain plus 2 constraints: the distances between bme 1 and bmc and between bme 2 and bmp are zero. The question here is to highlight the good respect of the constraints (11 constraints for 3 × 10 unknown). The results show first the success of the experiment with constraints respected (the error is zero after 18 iterations). Beyond the respect of these constraints, the experience shows that our method is able, illustrated on a simple example, to solve the same tasks as those solved by the traditional inverse kinematics.

However, our method has the disadvantage of being slower than standard inverse kinematics methods. Indeed, as illustrated in the figure 5, we compared the average calculation times of an iteration relatively to the number of articulations of a chain for our method and for the standard inverse kinematics. The time differences between the methods are explained by the fact that our remote based on the Jacobian matrix presents with this implementation, a dimension higher than the classical Jacobian matrix (orientation based. This results induce a longer inversion calculation time. Note however that our matrix is strongly sparse and that we can plan, to accelerate the inversion of this type of matrix, to use methods such as the one proposed by M. Berry [START_REF] Berry | Large scale sparse singular value computations[END_REF]. The acceleration of our method in this context is implemented and discussed in the section 6.3. Also note some irregularities in the distance-based curve, due to variations in processor load.

In the case of standard inverse kinematics, singularity problems lead to the use of a damping matrix. The results obtained are highly dependent on the correct estimation of the coefficients in this matrix. It is interesting to note that our method gives a regular configuration of the chain without damping parameter (see figure 6). This is explained by the fact that the minimization is calculated in the space of distances, which is equivalent to expressing variations across the Jacobian along the axis between two constrained points, unlike the standard inverse kinematics which applies these variations on the 3 axes of rotation of each joint.

2) Application of the contact between a hand and a sphere: Through this experience, we want to highlight the method's ability to simply express tasks in the form of distances, as well as to implicitly manage a large number of constraints associated with a certain level of priority.

With traditional inverse kinematics, it is also possible to specify complex tasks in the form of multiple goals to be achieved, characterized by geometric constraints of different kinds [START_REF] Phillips | Interactive real-time articulated figure manipulation using multiple kinematic constraints[END_REF]. This type of approach can be broken down into two phases:

• First, the constraints must be converted into goals to be achieved, • then to solve the inverse kinematic in the angular coordinate space.

Our method does not need the conversion phase. It allows to specify the task directly in the form of a set of properties to respect. These properties are implicitly integrated in the Jacobian matrix, and the optimization algorithm seeks to find a convergent solution in the Cartesian coordinate space.

To illustrate this approach, we implemented an experiment (see figure 7) involving the right hand of a skeleton that reaches a sphere. This action is defined from the simple specification of a set of distances, without knowing precisely the points to reach. The experiment is performed with a skele-ton including detailed hands. Starting from a key reference posture, the objective is to bring all the joints of the right hand to touch the sphere placed in the 3D scene. Beyond the lengths of the segments, we considered hard constraints that express the task through the contacts between the 26 joints of the hand and the sphere. Thus, any articulation of the hand in contact with the sphere leads to a distance constraint that is expressed as an objective function of the same type as (7).

This example shows the advantage of incorporating priorities between constraints, through hard and soft constraints (secondary tasks). Without priorities between constraints, the problem is over-constraint, with the risk that there will be no solution. It is thus possible, by adding or removing constraints, to influence the solutions to the inversion problem. If, for example, the secondary task is removed, it gives the system more latitude to reach the target, but can lead to a potentially unrealistic hand posture.

C. Motion edition (target to be reached during walking)

Here we highlight the method's ability to modify original movements, by introducing additional tasks. We also show two phases in the animation process. The first concerns the achievement of the objective (positioning of a constraint), the second the relaxation of the constraint which is accompanied by the return of the skeleton towards the initial posture. This experimentation raises the problem of competition between tasks, which requires priority management between constraints.

For this example, we use the same walking motion as in the motion tracking experiment. During his walk, we give as directive to the character to reach successively by the right hand, the left hand and again the right targets that are on his way. Using the same constraints as in the first experiment, we consider the segment lengths as hard constraints and the others as soft constraints (secondary task). The objective of reaching targets during animation is expressed by the temporary addition of hard constraints that take priority over the secondary task.

The figure 9 highlights the conflict between the constraints through an increase in the error of the secondary task. this happens when the targets are reached and the good respect of the hard constraints throughout the animation. Numerical stability First, it is important to note that, contrary to the standard inverse kinematics where the orientation of a joint is dependent on all the parent joints, working on a cloud of points makes it possible to express a point in relation to two neighbours in the simplest case and rarely to more than four or five points for a skeleton (six for a regular mesh). This implies a very low dependence between the points and therefore a more local and more specific distribution of the error related to the objective function. This makes our algorithm more stable. Note, however, that this method leads to a slower convergence. Moreover, over-constraining the problem leads to the possibility of no solution and can therefore lead to a non-continuity between two iterations.

Finally, we added a parameter to Newton's iteration to limit the involvement of the secondary task at the end of the iteration, the secondary task thus serving as a guide towards a solution during the iteration.

Performance The soft constraints are all expressed in relation to four static reference points (which are not part of the unknown vector), which also means that there is no dependence between the three coordinates of a point with all the other coordinates of the unknown vector. This induces that our Jacobian matrix of soft constraints is a diagonal matrix by blocks. However the inverse of such matrix is a diagonal matrix by blocks of the inverses of the blocks. We can thus simplify and finally accelerate the inversion speed of our jacobian by calculating independently the pseudo-inverts of each sub-matrix. If bmx a , bmx b , bmx c and bmx d are the reference points and bmx i is an unknown point to be determined based on these four reference points, the expression of the Jacobian becomes:

J (x 1 , . . . , x n ) =      J 1 0 . . . 0 0 J 2 . . . 0 . . . . . . . . . . . . 0 0 . . . J n      , (12)
avec les matrices diagonales (4 × 3)

J i (x i , x a , x b , x c , x d ) = 4     f ia (x i , x a )(x i -x a ) T f ib (x i , x b )(x i -x b ) T f ic (x i , x c )(x i -x c ) T f id (x i , x d )(x i -x d ) T     . ( 13
)
This optimization allows us to obtain significant results: for 31 points to be determined (93 unknown) associated with 124 (4×31) soft constraints and 30 hard constraints, we obtain a rate of 110 frames per second in the optimized case for 51 frames per second in the non-optimized case.

D. Application to a graph with cycles

The last experiment proposes to extend the solution to larger problems such as graphs containing cycles. For this category of applications we used a graph consisting of twenty vertices, which corresponds to twenty hard distances corresponding to the segments between adjacent vertices. We also added two hard distances representing the contact between two targets and two vertices of our graph. Finally, we contrasted two experiments with and without soft constraints in order to visualize the importance of these in the spatial deformation of our graph. As illustrated by the figure 10, the method works well for cycle graphs and allows us to contrast the results with and without soft constraints. This demonstration highlights the fact that through the manner of defining soft constraints, in addition to guaranteeing reference states during the manipulation, it is possible for us to give a style to the deformation of the chain. In particular it is possible to define a style relative to the rigidity of the structure considered. The results obtained demonstrate the ability of the distancebased method to solve kinematic motion control problems. This for diverse tasks from simple tracking of motion captured to solving reverse kinematics problems and modifying motion. The originality of the method lies essentially in the possibility of defining tasks in the form of a set of geometric constraints that express in a simple and relevant way the function to be performed (for example adapting the hand to the object to be grasped). These constraints are expressed in particular in the form of distances which characterize the proximity of the points of the skeleton (distances between joints), or from effectors to effectors or to other points of the environment. Thus, the formulation of the motion control that we propose makes it possible to implicitly take into account a set of constraints (including those related to the task). Incorporating these constraints into optimization methods provides optimal and consistent solutions that are relatively robust with regard to initial conditions and tasks. The general method is extended, in order to separate the contribution of hard distances (main task) and soft distances (secondary task), allowing to introduce a form of priority between constraints. In addition, projecting the solutions of the secondary task onto the kernel of the main task ensures that the main task is respected while reducing the space of the solutions.

The method easily performs motion adaptation tasks from captured data. However, limitations of the method are observed when the specified constraints are too different from those of the original motion, which can lead to a non-convergence of the algorithm, or even to instabilities. The method presented does not deal with the temporal aspects of animations either. Significant improvements would be possible by coupling to spatial functions temporal functions modelling joint synergies[AJG09]. The method could also be extended to handle point clouds from meshes or captured data.

  ∂zj ) T , x j , y j and z j being the coordinates of the point x j .

Fig. 1 .

 1 Fig. 1. The dotted segments represent the soft distance constraints while the other segments represent the hard distance constraints.

Fig. 2 .

 2 Fig. 2. Convergence results by Newton iteration (transition from the reference pose to the first pose of the movement)

Fig. 4 .

 4 Fig. 4. Illustration of the articulated arm test. The added constraints are illustrated by the red spheres.

  calculation of the time of an iteration related to the number of articlulations time for one iteration number of joints

Fig. 5 .

 5 Fig. 5. Average calculation time of an iteration relatively to the number of joints for distance-based methods (in green) and traditional inverse kinematics methods (in red).

Fig. 6 .

 6 Fig. 6. Illustration for two identical chain. Bottom: calculated by the standard inverse kinematics with an arbitrary damping factor. Above: calculated by our method.

Fig. 7 .

 7 Fig. 7. Sphre atteindre avec la main droite. A gauche la pose de rfrence. A droite le mouvement compos.

Fig. 8 .

 8 Fig. 8. Illustration de l'adaptation de mouvement. A droite le mouvement rfrence, gauche le nouveau mouvement.

Fig. 9 .

 9 Fig.9. Evolution of the errors of the main and secondary tasks during the animation. In blue, the error generated by the main task. In red, the one for the secondary task.

Fig. 10 .

 10 Fig. 10. Application to a cycle graph. Without soft constraint (left figure) and with soft constraints (right figure) : these constraints are represented by the blue dotted lines


Narjes Jomaa

David Nowak

Gilles Grimaud

Samuel Hym Cristal

Formal Proof of Dynamic Memory Isolation Based on MMU

Keywords: Formal proof, Memory isolation, Micro-kernel, Coq

For security and safety reasons, it is essential to ensure memory isolation between processes. The memory manager is thus a critical part of the kernel of an operating system. It is common for kernels to ensure memory isolation through a piece of hardware called memory management unit (MMU). However an MMU by itself does not provide memory isolation. It is only a tool the kernel can use to ensure this property.

In this paper we show how a proof assistant such as Coq can be used to model a hardware architecture with an MMU, and an abstract model of microkernel supporting preemptive scheduling and memory manager. We proceed by making formally explicit the consistency properties that must be preserved in order for memory isolation to be preserved.

I. INTRODUCTION

Modern operating-system kernels allow to share computer resources between untrusted processes, and to rapidly deal with external events, e.g., arrival of a network packet that would be lost if not dealt with immediately. In this context, for both safety and security reasons, it is important to respectively prevent accidental and malevolent access by a process to an address outside its own address space. On modern computers, kernels ensure memory isolation with the help of a piece of hardware called memory management unit (MMU). An MMU is a hardware component which all memory accesses must go through. It translates a virtual memory address to a physical address if there is indeed a corresponding one for the current setting. It also checks whether in the current setting accessing this address is allowed. It is indeed a common design to have the kernel space always mapped for efficiency but not accessible while in user mode. For this to work properly, the kernel has to maintain page tables which encode for each process the mapping between virtual addresses and physical addresses, and the access rights. It is important to note here that an MMU does not ensure memory isolation by itself, but it is only a tool the kernel can use to ensure it. A bug in the code of the kernel that deals with memory management (i.e., the memory manager) may lead to serious security and safety issues.

Since a kernel is executed in the so-called kernel mode (i.e., the privileged mode of the hardware), it is better from a security point of view to keep it as minimal as possible. This stems from the general principle that the trusted computing base (TCB) should be kept minimal. This is the reason why we focus in this paper on an abstract model of a microkernel [START_REF] Liedtke | On micro-kernel construction[END_REF] which supports preemptive scheduling and ensures memory isolation.

Contributions: Our main contribution is a formal proof in the Coq proof assistant of dynamic memory isolation based on the MMU. More precisely, it consists of:

• A formal model of a hardware architecture as a monad: the parts that are important for memory isolation (e.g., the MMU) are modeled in all their relevant minutiae, while less relevant parts are abstracted away. • A formal model of a microkernel supporting preemptive scheduling and memory management at an appropriate abstraction level so that it remains a realistic model without being linked to a particular implementation. • An explicit description of the consistency properties that must be preserved by a microkernel dealing with an MMU in order for the memory isolation to be preserved. Related work: There have been many efforts to make formal proofs of security for kernels. Below, we compare our work with those that appear most closely related to ours.

One of the most significant is the formal proof in the Isabelle/HOL proof assistant of the functional correctness and security properties of the microkernel seL4 [START_REF] Klein | Comprehensive formal verification of an OS microkernel[END_REF]. There is also CertiKOS which is a hypervisor dedicated to cloud computing that is formally verified [START_REF] Gu | Certikos: a certified kernel for secure cloud computing[END_REF]. In particular, its memory manager BabyVMM is constructed in layers so as to allow for formal verification by a series of refinements that are formalized in the Coq proof assistant [START_REF] Vaynberg | Compositional verification of a baby virtual memory manager[END_REF]. In contrast to those work above, our goal is not to prove formally properties of a specific microkernel but to clarify what is assumed by microkernels about the hardware architecture and what are the constraints a microkernel must follow in order for memory isolation to be guaranteed at all times.

In [START_REF] Barthe | Formally verified implementation of an idealized model of virtualization[END_REF], an idealized model of a hypervisor was formalized in Coq and isolation properties were proved. While we also consider an abstract model, we are not treating isolation from the point of view of information flow but at the lower level of page table management (information access). We are thus led to a model that includes an MMU and that deals with page allocation.

In [START_REF] Marti | Formal verification of the heap manager of an operating system using separation logic[END_REF], the operations of allocation and deallocation of a microkernel were proved correct. However, those operations live in a higher layer of the operating system than the lowerlevel layer we assume here. Moreover our work show that the correct implementation of those operations is essential to ensure memory isolation. Guo and Zhang proposed in [START_REF] Guo | Verifying preemptive kernel code with preemption control support[END_REF] a verification framework for verifying preemption control operations in a preemptive kernel. While, in our case, we focus our verification effort on proving memory isolation between processes.

Outline: We first describe in Section II our formal model of a microkernel and our formal definition of the memory isolation. We then make explicit in Section III the consistency properties that are to be preserved in order for memory isolation to be always guaranteed. In Section IV, we present our proof methodology and discuss the difficulties met and their solutions. We finally conclude Section V.

II. FORMAL MODEL OF A MICROKERNEL

In this section, we first briefly recall some basic facts about microkernels and then describe our formal model for a microkernel and our formal definition of the memory isolation.

A. Background on MMU-based microkernels

The purpose of a microkernel is to manage several executing programs known as runnable processes. To ensure security (in particular memory isolation), processes cannot directly access the physical memory. All their accesses to memory use virtual addresses and go through the MMU that translates virtual addresses to physical addresses. We illustrate the internal operation of the MMU with one level of indirection (cf. Fig. 1 taken from [START_REF] Tanenbaum | Operating systems -design and implementation[END_REF]). This translation mechanism is implemented using page tables. These page tables are managed by the memory manager of the kernel. Each process has an address space large enough to store its code and data. The memory manager should ensure that all the physical pages allocated to a given process are referenced only in its page table. Using the virtual address, translate starts by finding the corresponding entry in page table. It then checks whether accessing to that virtual address is allowed, i.e. there is a mapped page in this entry, using the present bit. It also verifies whether this page is accessible or not using the kernel only bit and the kernel mode of the current state s. When a process tries to violate these protection rules, the MMU raises an exception which will be handled by the microkernel. Moreover, to provide preemptive scheduling, the microkernel must share CPU time between all the currently runnable processes giving the illusion of executing all processes at the same time. Finally, in order to perform some operations that do require a higher level of privileges (read data from a file, get access to more physical memory, etc.), a process may request the microkernel to perform it on its behalf. To that end, the microkernel provides a set of system calls. A process can then invoke a system call by triggering an interruption.

Since these mechanisms are clearly crucial to ensure memory isolation among processes. The memory manager and the scheduling mechanism used by the microkernel must be verified.

B. H monad

Gallina, the specification language of Coq, is a purely functional language and thus does not provide imperative features such as updatable state, undefined behaviors and halting. In such language, it is thus common to implement such features by using a monad [START_REF] Wadler | Comprehending monads[END_REF]. For our model, we have defined a monad that we call H monad and that provides states (as described below in Section II-C) and support for undefined behaviors and halting.

Our H monad is a kind of state monad where M (A) is the type of a computation that may have side effects and returns a result of type A:

M (A) = def S → result(A × S)
where S is the type of the state of the system and result(X) is the inductive type with three constructors: one to return a result of type A and the new state of type S, and two others to denote an undefined behavior and halting. In the following, we will use s to denote a state in S. In our model, we classify computations into three groups: a hardware component models the behavior of a piece of hadware; an instruction is code for an atomic CPU instruction; a subroutine is a piece of code that should not be interrupted.

C. State of the system

In real implementations of operating systems, the state of the system is complex and includes the internal state of each hardware device and all the kernel data structures. In our formal verification, we focus only on the part of the state that is relevant to prove the properties we are interested in. We split accordingly our formal state into its hardware and software parts, and the formal definition of the type of the state is a record whose fields are the functions listed under the following hardware state and software state.

Hardware state : The following information about hardware devices (mostly processor and memory) is necessary to reason about memory isolation.

• currentptp(s) is the number of the physical page containing the page table of the current process.

• kernel mode(s) is a boolean that will be true when the processor is executing in kernel mode and false in user mode. • data(s) is the physical memory; it contains in particular the links to the free-page list and the page tables of processes which are essential for the MMU address space translation. The hardware state contains more information, such as the position of the current instruction to execute, the stream of interruptions, etc. We will not detail them here since they are not necessary to understand the rest of this paper.

Software state : During execution, the system needs to store some information in physical memory and which must be accessible only in kernel mode. We modeled that information separately from the memory itself in order to simplify the proof of our property. Real implementations do ensure that it is kept separate by storing it in some memory which is reserved by the kernel and thus never available for allocation. Following, we provide some details concerning the most important fields :

• processes(s) is the list of runnable processes. Note that a process type is a record which contains information about a runnable process P in this list like the reference to its page table ptp(P ) and the address to the next instruction to execute. When we switch between processes the value of currentptp(s) should be updated with the value of ptp(P ) of the selected process P . • first free page(s) is the first page of the free-pages linked list containing all the pages that can be allocated. Therefore, a memory manager is required to determine which pages are available for allocation and which are not. In our model, it consists of using the available pages themselves to store the linked list of available pages. We illustrate this memory model in (Fig 2). On system startup, available physical pages are initialized in such a way that the value of the first byte of the page corresponds to the position of the next free page; the microkernel has only to keep in its state the position of the first page of that linked list. • code(s) denotes the sequences of system and process instructions. The main property we are interested in here is to ensure data security. The proof of isolation for the code would be similar. Just as for the hardware state, the software state contains some more information that will not be detailed in this paper, such as the system stack.

D. Memory isolation

As explained above, each process has its own page table which is located in memory. Our model for page-table entries follows closely the description given in Section II-A. Each entry of a page table corresponds to a virtual address and contains the corresponding physical-page number and some bits for access control such as the present bit and the kernel only bit. The former should have the value 1 if there is a mapped page in this entry and the latter should have the value 0 if the mapped page should only be accessible to the microkernel. Unfortunately, the MMU cannot ensure separation between process address spaces all by itself.

1 Instruction write : integer → integer → M (unit)

Input : val: the value to be written vaddr: the virtual address at which it should be written Action: 2 paddr ← translate(vaddr) ; 3 if paddr is not an exception then 4 write val at physical address paddr 5 end Figure 3. Writing a value in memory Indeed, if the page tables are not configured correctly then the translation function could translate a virtual address to a physical address which is also used by another process. For instance, we have formalized the hardware instruction write (Fig. 3) that writes a value val at some physical address paddr. This instruction needs the hardware function translate (Fig. 4) to compute the physical address paddr for the virtual address vaddr according to the page table of the current process. In such a case, even if the physical page is mapped in two processes page tables, the MMU will translate addresses without raising any exception and the current process will access and modify the content of that page. This clearly shows that the two processes are not properly isolated.

To ensure isolation then, we need to guarantee that all page tables are always soundly configured. That is the aim of our memory isolation property (Def. 1). Intuitively, we want to show that for any state s there is no interference between any two runnable processes: if P 1 and P 2 are two runnable processes then all the pages which are used by P 1 are different from all pages used by P 2 .

Definition 1 (Memory isolation property).

A state s is isolated iff for all P 1 , P 2 ∈ Processes(s) such that ptp(P 1 ) = ptp(P 2 ) and for all p ∈ UsedPages(P 1 ), p / ∈ UsedPages(P 2 ), where

• Processes(s) is the set of runnable processes in the state s, • ptp(P i ) is the number of the physical page containing the page table of the process P i , • UsedPages(P i ) is the list of all the pages referenced in the page table ptp(P i ) plus ptp(P i ) itself.

III. CONSISTENCY

In this section, we introduce consistency properties and motivate them with counterexamples that show how a simple breach of consistency would invalidate memory isolation. Various of these properties rely on the list of free-pages.

Definition 2. Given a state s, FreePagesLinkedList(s) is the linked list of all physical pages available for allocation.

A. Software consistency

All marked-free pages are really free: The following consistency property REALLY FREE ensures that all markedfree pages are never mapped in any runnable-process page table.

Definition 3. Given a state s, REALLY FREE(s) holds iff for all p ∈ FreePagesLinkedList(s), p / ∈ AllUsedPages(s) and p < nb pages, where nb pages is the number of pages in physical memory and AllUsedPages(s) is the list of pages used by all processes in Processes(s). By adding the property REALLY FREE in consistency we must verify that on each system step, all marked-free pages are not mapped in any runnable-process page table. For instance, without such a property, we cannot prove that the subroutine add pte (cf. Fig. 6) preserves isolation. Indeed, this subroutine allocates the first free page selected from FreePagesLinkedList(s), then adds it into the process page table. If this page was already used by another process (cf. Fig. 5), the execution of add pte would result in a state in which the page tables of two processes would reference the same page: consequently, the isolation property would no longer hold. No cycle in free-pages list: The following consistency property NOT CYCLIC means that no page appears more than once in the free-pages list. Definition 4. Given a state s, NOT CYCLIC(s) holds iff for all page p, nb occurrences(p, FreePagesLinkedList(s)) ≤ 1 where nb occurrences(p, l) is the number of occurrences of p in list l. As we have detailed above, free pages are referenced through a linked list in physical memory. If such a property did not hold, the subroutine add pte could allocate twice the same physical page (to the same process or a different one): consequently, isolation property would no longer hold. Fig. 7 illustrates such counterexample.

No duplication in process used pages: When defining memory isolation we have explained that all used pages of any process in the runnable-process list must be different from all used pages of all the other runnable processes. The following consistency property NODUPLIC PROCESSPAGES property (Def. 5) ensures that for any process, all its used pages appear only once in its page table.

Definition

5. The consistency property NODU-PLIC PROCESSPAGES holds of a state s iff for all process P ∈ Processes(s), there is no duplication in UsedPages(P ).

The need for this property arises when proving the isolation property of subroutine remove pte (Fig. 8). This subroutine removes the content of a page-table entry and frees the page p of that entry by adding it to the free-page list. After the execution of remove pte, p must be really free. However, if there were another entry which mapped the same physical page p, after remove pte p would be marked both used and free at the same time. Then another process might allocate p, and isolation property would no longer hold. Fig. 9 illustrates an inconsistent state produced after the execution of remove pte when a physical page is mapped twice by the current process.

The current page table is of a process: The following consistency property CURRPROCESS INPROCESSLIST (Def. 6) ensures that the number currentptp(s) of the physical page storing the page table of the current process is indeed the ptp of one of the runnable processes.

Definition

6. Given a state s, the property CURRPROCESS INPROCESSLIST(s) holds iff there exists P ∈ Processes(s) such that ptp(P ) = currentptp(s).

This property is required to preserve the isolation prop-

1 Subroutine remove pte : integer → M (unit)

Input : vaddr: virtual address to be removed Action: 2 index ← the entry position corresponding to vaddr; 3 if index is valid and there is a mapped page at index then 4

Remove the entry content and return the page p which was mapped in this entry;

5

At the first byte of p write the value of the first free page of s then return p ;

6

Update the first free page of s with the value p; 7 end Figure 8. Remove a page table entry content erty for some subroutines which depend on this part of the state, the current page table. For instance, when the scheduler switches between processes, it calls the subroutine save process (Fig. 10) to remove the first process (which is the currently running process) from the runnable-process list to then add it at the end of the list with the currentptp(s) value and the new current instruction. The isolation property requires that the used pages should be different, thus when we add a process to the process list, all its mapped pages must be different from other mapped pages. Consequently, to prove isolation, adding the current process to process list requires that it matches a process in Processes(s), precisely the first one which has been removed previously. This property do ensure that the current page table is the page table of a process in Processes(s).

B. Hardware consistency

Page 0 is never used or marked-free: Physical memory may contain several kinds of pages such as used pages, free pages and pages which are not available for allocation. The latter is very interesting to isolate some part of the memory from all processes during all possible executions, for instance to store the code of the microkernel and its data. Thus, this information must be stated in consistency properties. So we need to make sure that the pages which are not available for allocation are indeed never used by a process or considered free. In our model, we chose page 0 as a simple example of this kind of pages. Of course, it could readily be generalized to any set of memory locations which are unavailable for allocation.

Two specific consistency properties, FREE NOTZERO (Def. 8) and USED NOTZERO (Def. 7), serve to check that page 0 stays unavailable for allocation. In a generalization to any set of unavailable locations, those properties would check that used and free pages stays within the range of valid page numbers. Action: 2 remove the first process from the runnable-process list; 3 add the current process to the end of the runnable-process list;

Figure 10. Saving the current process to the process list iff for all process P ∈ Processes(s), for all page p ∈ UsedPages(P ) then 0 < p < nb pages.

Definition 8. Given a state s, FREE NOTZERO(s) holds iff for all p ∈ FreePagesLinkedList(s), p = 0.

Physical memory large enough:

The following consistency property ensures that the memory is large enough. Definition 9. Given a state s, MEMORY LENGTH(s) holds iff nb pages × page size ≤ length(data(s))

where length(data(s)) to denote the size (in bytes) of the physical memory and page size to denote the size of a page in memory.

Obviously, an undefined hardware behavior can cause vulnerabilities and hence render a proof of security impossible. Commonly, it is the programmer that should ensure that the code never invokes undefined hardware behaviour. Precisely here we cannot determine the result of accessing to a physical page which is not defined in memory. Consequently, we need to define some property that ensure that all available physical pages are valid and we prove that our model never causes this security issue.

C. Conclusion

To conclude, consistency is the conjunction of multiple properties that must be preserved in order for isolation to be preserved. Testing at runtime that these properties are preserved is not realistic since it would take too much time. Indeed, it would for instance require checking if all the entries of a set of tables match some condition on every system call. Instead, we characterize the consistency properties required for isolation and prove that they are always preserved.

IV. ISOLATION PROOF

A. Hoare logic on monad

In order to reason about our code, we define a Hoare logic [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] on top of our H monad. A similar approach was used in [START_REF] Cock | Secure microkernels, state monads and scalable refinement[END_REF], [START_REF] Swierstra | A hoare logic for the state monad[END_REF]. Properties of computations are specified by Hoare triples of the form {P } c {Q} where:

• P is a precondition, i.e. a unary predicate on the starting state; • c is a computation returning a result of type A, i.e. the computation is of type M (A); • Q is a postcondition, i.e. a binary predicate on the returned value and on the ending state. By definition, a triple {P } c {Q} holds iff: for all state s, if P holds for s then either c(s) denotes the halting of the system or it denotes a pair (a, s ) where a is a returned value and s is an ending state such that the postcondition Q holds for this pair. In the case of c(s) denoting an undefined behavior, the triple does not hold.

The weakest precondition for a computation c and a postcondition Q is the unary predicate on state wp(Q, c) such that:

• the triple {wp(Q, c)} c {Q} holds, and • for any precondition P such that {P } c {Q} holds we have, for all state s, P (s) implies wp(Q, c)(s).

B. Preservation of isolation and consistency

We have formally proved in Coq that all the instructions, subroutines and hardware components that we model preserve the isolation and the consistency properties. For the most basic computations used as building blocks for our instructions and subroutines, we first prove their weakest precondition triples, and then use it to prove their invariant triples that state preservation of isolation and consistency. Then we combine those basic invariant triples to obtain invariant triples for the more complex instructions, subroutines and hardware components. The following examples illustrate our approach and the difficulties we encountered.

Detailed example: writing in memory:

The intended behavior of write is to store a given value at a given virtual address in memory. First, this instruction invokes the hardware instruction translate. If there is a mapping that corresponds to the given virtual address vaddr, translate returns the physical address paddr, otherwise it returns an exception. In the first case, write then executes the instruction write phy (cf. Fig. 11) which stores a value v at the memory address paddr of the current process.

1 Instruction write phy : integer → integer → M (unit)

Input : v: value to be stored at paddr paddr: physical address Action : 2 p ← the page of paddr; 3 i ← the position of paddr in p; 4 update memory(v, i, p); Our aim is to ensure that the instruction write preserves isolation and consistency. So, we must prove the correctness of the Hoare triple write invariant.

Proposition (write invariant). If the isolation property I and the consistency property C hold for the state before the execution of write, then I and C also hold afterwards. Formally, we write: {I ∧ C} write(v, vaddr) {I ∧ C} translate is invoked first. It can return an exception. In that case, write ends and the final state will be identical to the initial state: isolation and consistency are then trivially preserved.

Let us then consider when translate succeeds. Since translate is invoked first, its precondition must be the same as the precondition of the instruction write. The instruction write phy is the last instruction invoked by write so its postcondition must be the same postcondition as write.

Since the whole instruction write is the sequence of those two functions translate and write phy, the postcondition of the first must match the precondition of the second. translate should preserve isolation and consistency, so its postcondition will include both these properties.

Another relevant point is that write phy uses the return value paddr of translate as a parameter, so we must define some property R that depends on this value and the state produced by translate. This property is required to prove that isolation and consistency hold after the execution of write phy. Therefore, the challenge here is to determine the property R then prove the Hoare triples for translate invariant (Lemma 1) and write phy invariant (Lemma 2).

Lemma 1 (translate invariant). If the isolation property I and the consistency property C hold for the state before the execution of translate, then I, C and R also hold afterwards. Formally, we write: {I ∧ C} translate(vaddr) {I ∧ C ∧ R} Lemma 2 (write phy invariant). If the isolation property I, the consistency property C and the property R hold for the state before the execution of write phy, then I and C also hold afterwards. Formally, we write:

{I ∧ C ∧ R} write phy(v, paddr) {I ∧ C}
After the execution of translate, the new state is equal to the previous state. So, it is straightforward to prove that isolation and consistency are preserved. On the other hand, we have to prove that R(paddr, s) holds afterwards (where paddr is the physical address returned by translate). For such needs, we use its weakest precondition triple.

Contrary to translate, write phy modifies the current state and does not return any value. Consequently, the postcondition will depend on the new state that we denote s . This instruction stores the value v in physical memory. Thus, only data(s) will be changed.

Therefore we have to prove that if isolation I, consistency C and R hold of the parameter paddr and the state before the execution of write phy then isolation and consistency hold afterwards. This proof requires eight cases, one for isolation, and one per consistency property. In the following we only sketch the proof of the case for isolation. This case amounts to the fact that if the current process writes a value in physical memory, it cannot modify a page table of a runnable process. The challenge is to prove that the position of the page p (cf. Fig. 11) is different from all positions of runnable-process page tables and mapped pages into these tables.

Let P 1 and P 2 be two different processes from Processes(s). The consistency property CURRPROCESS INPROCESSLIST(s) (Def. 6) ensures that the page table of the current process is a page table of a process in Processes(s). Consequently we have three cases (two of which are symmetric). The first case is when currentptp(s) is different from both ptp(P 1 ) and ptp(P 2 ). Isolation and consistency are trivially preserved in this case. The two other cases are respectively when currentptp(s) is equal to ptp(P 1 ) or, symmetrically, ptp(P 2 ). In those cases, we need the property R to ensure that the page p is a mapped page in the current-process page table and i is a position in this page. In addition we need the consistency property NODUPLIC PROCESSPAGES to ensure that the position of a mapped page is different from the position of the current page table and thus that the page table will not be modified. Also, we use the isolation property of the previous state to prove that this instruction can not modify any other runnable-process page table.

Other example: adding a new PTE: The proof sketch of write invariant above was set out to explore the most relevant points necessary to understand our approach to establish expected properties of our model. There are however more involved subroutines that need more effort to prove their expected properties because of their complexity. In this section, we will briefly discuss another example.

The expected behavior of the subroutine add pte (Fig. 6) is to add a new entry to the page table of the currentlyrunning process: it maps a new physical page at a given index in the page table of the currently-running process. More precisely, if there is no mapping yet at that index, it invokes a subroutine called alloc page. This subroutine allocates a new page then adds a new mapping corresponding to this page and to a given permission. The latter one requires a precondition ensuring that there is no mapping in the involved entry which is, notably, ensured by the second test in Fig. 6. The difficulty is that between this test and the second instruction which adds the mapping in pte, the subroutine alloc page changes the state. Consequently, we have to propagate this property by proving that if it holds at the state before the execution of alloc page then it holds afterwards. In our model, alloc page is used in several subroutines. Therefore, we have defined and proved a new invariant for alloc page which preserves isolation and consistency and propagates the necessary property.

V. CONCLUSIONS AND FUTURE WORK

One conclusion we can draw from this formalization is that many details about the architecture and the microkernel are to be taken into account in order to prove memory isolation between processes. This is thus a typical example of a proof that would be hard for a human to conduct without a proof assistant, because there would be too many details to keep in mind at all times. But with the help of the Coq proof assistant that keeps track rigorously of all the minutiae of the proof, one can be sure not to overlook any corner case.

Also we arrived at the current list of consistency properties listed in Section III after a few iterations. And each time we were extending this list, we had to go through all the invariant proofs again to prove that consistency was preserved. We benefited from the simple but useful mechanism called bullets which allows to structure proof script and thus easily find where to insert the additional cases to be dealt with.

Our formalization in Coq is available at: http://www.cristal.univ-lille.fr/˜nowakd/microkernel/ One possible future work is to use the insights we gained from this formalization to design kernels that are more amenable to formal proof. We are in particular interested in exokernels [START_REF] Engler | Exokernel: An operating system architecture for application-level resource management[END_REF] because they push much further the minimality principle [START_REF] Liedtke | On micro-kernel construction[END_REF] while still ensuring fundamental security properties that would be interesting to formally prove.

Figure 1 .

 1 Figure 1. Memory management unit (MMU)

Figure 2 .

 2 Figure 2. Memory model

4 if

 4 there is a mapped page in pte and (the kernel mode(s) = true or kernel only(pte) = 0) then 5 calculate the physical address and return it;

Figure 4 .

 4 Figure 4. Translating virtual addresses to physical addresses

Figure 5 .

 5 Figure 5. Counterexample for REALLY FREE

Figure 6 .

 6 Figure 6. Adding an entry in page table

Figure 7 .

 7 Figure 7. Counterexample for NOT CYCLIC

Definition 7 .Figure 9 .

 79 Figure 9. Counterexample for NODUPLIC PROCESSPAGES

Figure 11 .

 11 Figure 11. writing a value at a physical address

1

  Hardware component translate : integer → M (integer + exception) Input : vaddr: a virtual address Output: the corresponding physical address or an exception Action : 2 if the vaddr size is valid then 3 calculate the address of page table entry pte and the offset in this page corresponding to vaddr;

This work was partially supported by the Celtic-Plus Project ODSI C2014/2-12, CNRS Action Spécifique Sécurité, and IRCICA.