Magali Bardet
email: magali.bardet@univ-rouen.fr

Manon Bertin
email: manon.bertin@etu.univ-rouen.fr

Improvement of algebraic attacks for solving superdetermined MinRank instances

Keywords:

The MinRank (MR) problem is a computational problem that arises in many cryptographic applications. In Verbel et al. [24], the authors introduced a new way to solve superdetermined instances of the MinRank problem, starting from the bilinear Kipnis-Shamir (KS) modeling. They use linear algebra on specific Macaulay matrices, considering only multiples of the initial equations by one block of variables, the so called "kernel" variables. Later, Bardet et al. [7] introduced a new Support Minors modeling (SM), that consider the Plücker coordinates associated to the kernel variables, i.e. the maximal minors of the Kernel matrix in the KS modeling.

In this paper, we give a complete algebraic explanation of the link between the (KS) and (SM) modelings (for any instance). We then show that superdetermined MinRank instances can be seen as easy instances of the SM modeling. In particular, we show that performing computation at the smallest possible degree (the "first degree fall") and the smallest possible number of variables is not always the best strategy. We give complexity estimates of the attack for generic random instances.

We apply those results to the DAGS cryptosystem, that was submitted to the first round of the NIST standardization process. We show

Introduction

The MinRank Problem

The MinRank problem was first mentioned in [START_REF] Buss | The computational complexity of some problems of linear algebra[END_REF] where its NP-completeness was also proven. It is a central problem in algebraic cryptanalysis, starting with the Kipnis and Shamir modeling [START_REF] Kipnis | Cryptanalysis of the HFE public key cryptosystem by relinearization[END_REF] for the HFE encryption scheme. The MinRank problem is very simple to state: Problem 1 (Homogeneous MinRank problem).

Input: a target rank r ∈ N and K matrices M 1 , . . . , M K ∈ F m×n q . Output: field elements x 1 , x 2 , . . . , x K ∈ F q , not all zero, such that

Rank M x def = K i=1 x i M i r.
It plays a central role in public key cryptography. Many multivariate schemes are strongly related to the hardness of this problem, as in [START_REF] Patarin | Hidden fields equations (HFE) and isomorphisms of polynomials (IP): two new families of asymmetric algorithms[END_REF][START_REF] Kipnis | Cryptanalysis of the HFE public key cryptosystem by relinearization[END_REF][START_REF] Petzoldt | Design principles for HFEv-based multivariate signature schemes[END_REF][START_REF] Porras | ZHFE, a new multivariate public key encryption scheme[END_REF]. The 3rd round NIST post-quantum competition finalist Rainbow [14], or alternate GeMSS [13] suffered attacks based on the MinRank problem [START_REF] Beullens | Improved cryptanalysis of UOV and Rainbow[END_REF][START_REF] Beullens | Breaking Rainbow takes a weekend on a laptop[END_REF][START_REF] Tao | Efficient key recovery for all HFE signature variants[END_REF][START_REF] Baena | Improving support-minors rank attacks: applications to GeMSS and Rainbow[END_REF].

In code-based cryptography, the MinRank problem is exactly the decoding problem for matrix codes in rank metric. The two submissions ROLLO and RQC [START_REF] Aragon | Second round submission to the NIST post-quantum cryptography call[END_REF][START_REF] Aguilar Melchor | Rank quasi cyclic (RQC). Second Round submission to NIST Post-Quantum Cryptography call[END_REF], from the 2nd round of the NIST post-quantum competition, have been attacked using algebraic cryptanalysis in [START_REF] Bardet | An algebraic attack on rank metric code-based cryptosystems[END_REF][START_REF] Bardet | Improvements of algebraic attacks for solving the rank decoding and minrank problems[END_REF]. Their security analysis relies on the decoding problem for F q m -linear rank-metric codes, which can actually be reduced to the MinRank problem. This is of great importance for cryptographic purposes to design algorithms that solve efficiently algebraic modeling for the MinRank problem, and to understand their complexity.

Algebraic modeling

There has been a lot of recent progress in the algebraic modeling and solving of the MinRank problem. We start by recalling the first modeling, namely the Kipnis-Shamir (KS) modeling. Note that it implicitely assumes that the n-r first columns of the small-rank matrix M x we are looking for are linearly dependent from the last r ones. In this paper, we will assume that we are looking for a matrix M x of rank exactly r (this can be achieved by looking for increasing ranks, starting from r = 1), and that the last r columns of M x are linearly independent (it is true up to a permutation of the columns, and for random matrices it is true with high probability). We will see later that this last assumption is not mandatory.

Modeling 1 (Kipnis-Shamir Modeling [START_REF] Kipnis | Cryptanalysis of the HFE public key cryptosystem by relinearization[END_REF]). Consider a MinRank instance (M 1 , . . . , M K ) ∈ F m×n q with target rank r. Then, the MR problem can be solved by finding x 1 , . . . , x K ∈ F K q , and C = (c i,j ) ∈ F r×(n-r) q such that K i=1

x i M i I n-r C = 0 m×(n-r) .

(KS)

The m(n-r) equations are bilinear in the K linear variables x = (x 1 , . . . , x K ) and the r(nr) entries of the formal matrix C = (c i,j ) i,j , refered to as the kernel variables.

It is clear that a matrix has rank ≤ r if and only if its right kernel has dimension at least nr, so that any solution of the MinRank problem is a solution of (KS).

The complexity of solving a generic bilinear system has been studied in [START_REF] Faugère | Computing loci of rank defects of linear matrices using Gröbner bases and applications to cryptology[END_REF][START_REF] Faugère | Gröbner bases of bihomogeneous ideals generated by polynomials of bidegree (1,1): Algorithms and complexity[END_REF], and gives an upper bound for the KS system, but this estimate wildly overestimates the experimental results.

The matrix M x has rank ≤ r if and only if all its minors of size r + 1 are zero. This modeling has been presented and analysed in [START_REF] Faugère | On the complexity of the generalized minrank problem[END_REF][START_REF] Faugère | Computing loci of rank defects of linear matrices using Gröbner bases and applications to cryptology[END_REF]. Under the assumption that the last r columns of M x are linearly independent, it is sufficient to consider minors involving columns in sets T = {t}∪{n-r +1..n} with 1 ≤ t ≤ nr, as it means that the last r columns generate the column vector space. The notation |M| J,T represents the determinant of the submatrix of M where we keep only rows in J and columns in T .

Modeling 2 (Minors Modeling). Let (M 1 , . . . , M K ) ∈ F m×n q be a MinRank instance with target rank r. Then, the MR problem can be solved by finding

x 1 , . . . , x K ∈ F K q such that |M x | J,T = 0, ∀J ⊂ {1..m}, #J = r + 1, T = {t} ∪ {n -r + 1..n} ⊂ {1..n} (Minors)
Recently, a new modeling has been introduced in [START_REF] Bardet | Improvements of algebraic attacks for solving the rank decoding and minrank problems[END_REF], that is at the moment the most efficient one from the complexity point of view. It uses two ideas, that we will separate in two modelings: the first idea is that (KS) means that the vector space with generator matrix M x is orthogonal to the one with generator matrix I n-r C ⊤ . It is then straightforward to see that any row of M x belongs to the dual space with generator matrix -C I r . This leads to: Modeling 3 (Support Minor Modeling-C [START_REF] Bardet | Improvements of algebraic attacks for solving the rank decoding and minrank problems[END_REF]). Let (M 1 , . . . , M K ) ∈ F m×n q be a MinRank instance with target rank r. Then, the MR problem can be solved by finding x 1 , . . . , x K ∈ F K q , and C = (c i,j ) 1≤i≤r,1≤j≤n-r ∈ F r×(n-r) q such that r i -C I r * ,T = 0, ∀T ⊂ {1..n}, #T = r + 1, and r i row of M x .

(SM-C)

The m n r+1 equations are bi-homogeneous with bi-degree (1, r) in the K linear variables x = (x 1 , . . . , x K ) and the r(nr) entries of the formal matrix C = (c i,j ) i,j , refered to as the kernel variables.

Note that in (SM-C), the entries of C appear only as maximal minors of (-C I r ). This leads to the second idea from [START_REF] Bardet | Improvements of algebraic attacks for solving the rank decoding and minrank problems[END_REF], which consists in using the Plücker coordinates: we replace each |(-C I r )| * ,T , that is a polynomial of degree #T = r in the entries of C, by a new variable c T using the injective Plücker map, see [11, p.6].

p : {W ⊂ F n q : dim(W) = r} → P N (F q ) (N = n r -1) C → (c T ) T ⊂{1..n},#T =r .
Modeling 4 (Support Minor Modeling-c T [START_REF] Bardet | Improvements of algebraic attacks for solving the rank decoding and minrank problems[END_REF]). Let (M 1 , . . . , M K ) ∈ F m×n q be a MinRank instance with target rank r. Then, the MR problem can be solved by finding x 1 , . . . , x K ∈ F K q , and (c T ) T ⊂{1..n},#T =r ⊂ F

( n r ) q such that t∈T (M x ) i,t c T \{t} = 0, ∀T ⊂ {1..n}, #T = r + 1, and i ∈ {1..m} . (SM)
The m n r+1 equations are bilinear in the K linear variables x = (x 1 , . . . , x K ) and the n r minor variables c T , for all T ⊂ {1..n}, #T = r. The benefit of introducing such coordinates to describe a vector space rather than a matrix describing a basis is that contrarily to the matrix representation, a vector space W has unique Plücker coordinates associated to it. This is not the case of the matrix representation of a vector space: if the rows of a matrix C generate the vector space, then the rows of AC generate the same vector space for any invertible A ∈ GL(r, F q ). For our algebraic system, this brings the benefit of reducing the number of solutions of the system: there are several solutions C to the algebraic system (SM-C), that correspond to one unique solution to (SM). As already pointed out in [START_REF] Bardet | Improvements of algebraic attacks for solving the rank decoding and minrank problems[END_REF], it is also extremely beneficial for the computation to replace polynomials |(-C I r | * ,T with r! terms of degree r in the entries of C by single variables c T 's in F q . We will use (SM-C) for the theoretical analysis of the link between the various modelings, and (SM) for the computational solving.

Contributions

As a first contribution, we show that the first three systems are related, more precisely Proposition 1. The set of equations (KS) is included in the set of equations (SM-C), and the ideals generated by the SM-C and KS equations are equal. Equations Minors (Minors modeling) are included in the ideal generated by KS.

This proposition applies to any instance, without particular hypothesis. Note that Eq. (Minors) contain only the linear variables, hence the ideals cannot be equal. This proposition is not only interesting on the theoretical point of view, but it also allows to understand different computational strategies and to select the best one. A discussion is provided in Remark 1.

In [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF], Verbel et al. analyse degree falls occuring during a Gröbner basis computation of (KS), and show that for overdetermined systems this can occur before degree r +2, which is the general case. As a second contribution, we show that these degree falls are in fact equations from SM-C. Using the Plücker coordinates in (SM) allows to drastically reduce the size of the considered matrices. Moreover, we give example to show that minimising the degree and number of equations is not always the best strategy for optimising the solving complexity.

Finally, we revisit the DAGS cryptosystem [START_REF] Banegas | DAGS : Key encapsulation for dyadic GS codes[END_REF], that was a 1st round candidate to the NIST post-quantum standardization process, and was attacked by Barelli and Couvreur [8]. We show that the attack is in fact a MinRank attack, and describe the structure of this non-random superdetermined Min-Rank instance. This precise understanding of the problem makes it possible to choose the right parameters for an optimal attack.

Notation and preliminaries

Vectors are denoted by lower case boldface letters such as x, e and matrices by upper case letters C, M. The all-zero vector of length ℓ is denoted by 0 ℓ . The j-th coordinate of a vector x is denoted by x j and the submatrix of a matrix C formed from the rows in I and columns in J by C I,J . When I (resp. J) represents all the rows (resp. columns), we may use the notation C * ,J (resp. C I, * ). We simplify C i, * = C {i}, * (resp. C * ,j = C * ,{j} ) for the i-th row of C (resp. j-th column of C) and c i,j = C {i},{j} for the entry in row i and column j. Finally, |C| is the determinant of a matrix C, |C| I,J is the determinant of the submatrix C I,J and |C| * ,J the one of C * ,J . The transpose of a matrix C is C ⊤ . The all-one vector of size n is denoted by

1 n = (1, . . .

, 1).

To simplify the presentation, we restrict ourselves to a field of characteristic 2, but the results are valid for any characteristic, the only difference being the occurrence of a ± sign before each formula.

For any matrix A of size q × r with r ≤ q, and any set J ⊂ {1..q} of size r + 1, we define the vector V J (A) of length q whose jst entry is 0 if j / ∈ J and |A| J\{j}, * for j ∈ J. For A of size r × q with r ≤ q we define

V J (A) def = V J (A ⊤ ).
Using Laplace expansion along a column, it is clear that for any vector a of length q we have

V J (A)a ⊤ = a ⊤ A J, * . (1)
We denote by vec row (A) (resp. vec col (A)) the vertical vector formed by concatenating successives rows (resp. cols) of A. We have the formula

vec row (AXY) = (A ⊗ Y ⊤ )vec row (X) (2)
vec col (AXY) = (Y ⊤ ⊗ A)vec col (X)
where

A ⊗ B def = (a i,j B) i,j
is the Kronecker product of two matrices A = (a i,j ) i,j and B.

For a system F = {f 1 , . . . , f M } of bilinear equations in two sets of variables x = (x j ) 1≤j≤nx and y = (y ℓ ) 1≤ℓ≤ny , it is usual to consider the associated Jacobian matrices:

Jac x (F ) = ∂f i ∂x j i=1..M,j=1..nx , Jac y (F ) = ∂f i ∂y ℓ i=1..M,ℓ=1..ny .
For homogeneous bilinear systems they satisfy the particular relation:

Jac x (F )x ⊤ = f 1 . . . f M ⊤
and any vector in the left kernel of a Jacobian matrix is a syzygy of the system. Moreover, Jac x is a matrix whose entries are linear form in the variables y, and Cramer's rule show that the left kernel of Jac x contains vectors V T (Jac x (F ) T, * ) using the notation from (1) for all T ⊂ {1..M} of size n y + 1. Generically those vectors generate the left kernel. For affine systems, we consider the jacobian matrix associated to the homogeneous part of highest degree of the system, and any syzygy for this part, that is not a syzygy of the entire system leads to a degree fall.

Relations between the various modelings

This section applies to any MinRank instance without any specific hypothesis.

The KS modeling consists in bilinear equations in two blocks of variables x and C, whereas the SM-C modeling contains equations of degree 1 in x and r in C, the variables C appearing only as maximal minors of -C I r .

In the case of the KS modeling, it has been noticed in [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF], and later [START_REF] Bardet | Improvements of algebraic attacks for solving the rank decoding and minrank problems[END_REF]Lemma1] that the jacobian matrices have a very particular shape: if we write

M x = M (1) x M (2) x with M (1)
x of size m×(n-r) and M

(2)

x of size m×r, and in the same way we write each

M i = M (1) i M (2) i
, then the homogeneous part of highest degree of the system is M

(2)

x C, and its Jacobian matrices are, if we take the variables and equations in row/column order:

Jac x i vec row x i M (2) i C = vec row M (2) i C = I m ⊗ C ⊤ vec row M (2) i Jac x vec row M (2) x C = I m ⊗ C ⊤ vec row M (2) 1 . . . vec row M (2) K Jac vec col (C) vec col M (2) x C = I n-r ⊗ M (2) x (3)
The jacobian matrix in C admits a left kernel that contains the following vectors:

e i ⊗ V J (M (2) x ) for any J ⊂ {1..p}, #J = r + 1, 1 ≤ i ≤ n -r, (4)
where e i is the ith row of I n-r . As a consequence, the ideal generated by the (KS) equations contains the equations

(e i ⊗ V J (M (2) x ))vec col (M x I n-r C ) = (e i ⊗ V J (M (2) x ))vec col (M x 1) = V J (M (2)
x )M (1) x e i ⊤ ( thanks to (2))

= |M x | J,{i}∪{n-r+1..n} ( thanks to (1)).

Those are precisely the (Minors) equations. The jacobian matrix in x admits a left kernel that contains the vectors

e ℓ ⊗ V J (C) for any J ⊂ {1..n -r}, #J = r + 1, 1 ≤ ℓ ≤ m. (5)
The ideal generated by the (KS) equations contains the equations

(e ℓ ⊗ V J (C))vec row (M (1) x ) = e ℓ M (1) x V J (C) ⊤ = V J (C)(M (1) x ℓ, * ) ⊤ = (M (1)
x ℓ, * )

⊤ C ⊤ J, * = M (1) x ℓ, * C * ,J
.

They are exactly the (SM-C) equations for J ⊂ {1..n -r}. They have a degree r in the kernel variables c i,j .

In [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF], the authors propose to solve (any) instances of KS by considering particular elements in the left kernel of the Jacobian matrix in x for some degree 1 ≤ d ≤ r -1. This is done by considering all combination of the polynomials with coefficients The key remark is that the equations they consider are

e ℓ ⊗ V J (C T, * ) (6
(e ℓ ⊗ V J (C T, * ))vec row (M x I n-r C ) = e ℓ M x I n-r C V J (C T, * ) ⊤ = r ℓ -C I r * ,T ′ for T ′ = J ∪({n-r + 1..n} \ (T + n-r)) ⊂ {1.
.n} of size r + 1. The equations have indeed a degree d in the kernel variables c i,j .

Note that for d = 0, for T ′ = {ℓ}∪{n-r+1..n} the equation r ℓ -C I r * ,T ′ is the ℓth KS equation, and we get all SM equations. As a consequence, we have proven Proposition 1.

Remark 1. In the light of the previous results, we can understand more precisely the behavior of a generic Gröbner basis (GB) algorithm with a graded monomial ordering and a Normal selection strategy run on (KS) or (SM-C). As (SM-C) contains (KS) directly into the system, computing a GB on (SM-C) will also compute all equations that would be computed by (KS). On the other hand, when computing a GB for (KS), the algorithm will produce all equations (SM-C) by multiplying by monomials in C, hence we can expect many syzygies during a GB computation on (SM-C).

This encourages to compute with (SM-C), but to look only at multiple of the equations by the x i 's variables, which is the strategy proposed in [START_REF] Bardet | Improvements of algebraic attacks for solving the rank decoding and minrank problems[END_REF]. Adding to this the change of variable that consider any minor of C as a variable removes the hardness of computing with high degree polynomials (as the new variables have degree 1 instead of a polynomial of degree d with d! coefficients for the minor).

Complexity of solving superdetermined systems

Superdetermined MinRank instances are defined in [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF] as MinRank instances where K < rm. In the light of the previous section, it is now clear that [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF] considers for any 0 ≤ d ≤ r the equations

E(d) def = E J,T,ℓ def = e ℓ M x I n-r C V J (C T, * ) ⊤ : ∀J⊂{1..n-r},#J=d+1, ∀T ⊂{1..r},#T =d, ∀ℓ∈{1..m} . ( 7
)
and search for linear combination that will produce degree falls. We can rewrite the equations

E J,T,ℓ = r ℓ C I r * ,T ′ with T ′ = J ∪ ({n -r + 1..n} \ (T + n -r)) ⊂ {1..n} = K i=1 j∈J (M (1)
i ) ℓ,j x i |C| T,J\{j} + K i=1 s / ∈T (M (2)
i ) ℓ,s x i |C| T ∪{s},J .

We have a total of r d=0 m n-r d+1 r d = m n r+1 equations in r d=0 K n-r d r d = K n r variables described by

V(d) def ={x i |C| T,J } i=1..K,#J=d,#T =d , V(r + 1) = ∅.
The system can be solved by linearization by constructing the associated Macaulay matrix: its rows are indexed by J, T, ℓ (with #J = d + 1, #T = d) and its columns by i, J ′ , T ′ (with #J ′ = d = #T ′ ), and the coefficient in row (J, T, ℓ) and column (i, J ′ , T ′ ) corresponds to the coefficient of E J,T,ℓ in the monomial x i |C| T ′ ,J ′ . We can sort the columns by decreasing degree, i.e. consider first monomials in V(r), up to V(0) that are the K variables x i , see Fig.

m n -r d + 1 r d K n -r d + 1 r d + 1 V(r) V(r -1) . . . V(d + 1) V(d) . . . V(1) V(0) E(r) E(r -1)
. . .

E(d)

. . .

E(0)

Figure 1: Shape of the Macaulay matrix associated to Eq. ( 7). The columns correspond to equations in V(d), the rows to equations E(d). Gray cells correspond to non-zero part of the matrix.

which is Corollary 5 in [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF], and the first part of the Macaulay matrix with columns in V(d + 1) is, up to a good choice of the ordering of rows and columns, a block of diagonal matrices B J as described in [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF]. The best complexity estimates comes from the (SM) modeling, when considering the minors |C| T,J as new variables. Eq. ( 7) contains m n r+1 equations in K variables x i and n r variables that are minors of (-C I r ). Hence the system can be solved whenever m n r+1 K n r by linearization, i.e. m(nr) K(r + 1). After linearization, we get with overwhelming probability #V(0) -1 = m -1 linear equations in the x i 's only.

As always, it is possible to improve computation by puncturing the matrix M x (taking only sufficiently many columns so that we keep an overdetermined system), or by hybrid approach (performing an exhaustive search on some columns of C, at the cost of q ar operation in F q for a columns). It is also possible, as in [7, Eq. ( 23) p. 19], to compute equations at higher degree b in x i . For instance, at b = 2 we can multiply all equations in (SM) by x i 's variables, and we get for each set E(d) of equations:

m n r + 1 K - n r + 2 m + 1 2 equations, n r K + 1 2 monomials. (8)
For instance, Table 1 compares the (SM) system with previous results from [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF]. For r = 5, the ratio between equations and monomials in (SM) is smaller than 1, so that we cannot expect to solve by linearization directly. Computing at b = 2 would produce 14400 equations in 13860 variables of m n K r m(n-r) K(r+1) n eq n vars n rows in [ degree less than or equal to 7 in (x, C). Note that the last entry for r = 6 would theoretically require to go up to b = 5 with matrices of size 427350. However, [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF] suggest that we can have a closer look at the shape of the equations and maybe find a better complexity for some very overdetermined instances.

Hence . In [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF], the authors determine the first degree fall in KS by looking for the smallest d for which we have more equations in E(d) than variables in V(d + 1). This produces Rank(E(d)) -#V(d + 1) degree fall, but it is not clear how to end the computation. If there is more equations than variables, i.e.

m n -r d + 1 r d K n -r d + 1 r d + 1 + K n -r d r d - 1
then with overwhelming probability, the linear system is full rank (its kernel has dimension 1 as the system is homogeneous in x) and a non-zero element in the kernel of the Macaulay matrix gives a value for each variable x i |C| T,J . It is then straightforward to deduce x i /x i 0 from two values x i |C| T,J and

x i 0 |C| T,J . On the other hand, if

K n -r d + 1 r d + 1 ≤ m n -r d + 1 r d and m n -r d + 1 r d < K n -r d + 1 r d + 1 + K n -r d r d - 1
then it is necessary to add new equations to end the computation. It can be done by consider equations of "higher degree". If each minor of C is taken as a variable, it doesn't add a computational burden. We can solve as soon as we can get sufficiently many blocks of equations E(d) such that we get more equations than columns. Experimental results are presented Table 2 on the same parameters as [24, Table 2]. instance for a MinRank problem with 12 × 12 matrices and a target rank r = 4, the authors in [START_REF] Verbel | On the complexity of "superdetermined" Minrank instances[END_REF] solve at degree d = 4 in 58s, whereas it is more interesting to consider equations in E(3..4) that have degree up to 5, without considering equations of degree 2..3. Note that if we puncture too much the matrices, for instance by taking only n = 8 columns, then we do not have any more an overdetermined SM system, and solving it now require to produce more equations, for instance by considering b = 2. In this case, we get a system of 5880 equations in 5460 and we can solve, but this will be more costly than solving with n = 9.

Remark 2. There is an asymetry between m and n in the modelings. It is always possible to exchange m and n by considering the transpose of the matrices, but it is not clear in general which problem will be easier (m > n or m < n). For instance, for K = 10, r = 2 we can have the following behaviors: for m = 6, n = 7 the Macaulay matrix up to d = r has size 210 × 210, whereas for m = 7, n = 6 it is not possible to solve at b = 1 (the Macaulay matrix has dimension 140 × 150). We need to go to b = 2 and solve a matrix of size 980 × 825. On the contrary, for m = 10, n = 6, the Macaulay matrix has dimension 160 × 140 (d = 1..2), whereas for m = 6, n = 10, the Macaulay matrix for d = r has size 336 × 280. However, as the number of equations is a multiple of m, the best solution is often with m ≥ n.

Application to DAGS

DAGS scheme [START_REF] Banegas | DAGS : Key encapsulation for dyadic GS codes[END_REF] is a key encapsulation mechanism (KEM) based on quasidyadic alternant codes that was submitted to the first round of the NIST standardization process for a quantum resistant public key algorithm. It suffered from an algebraic attack [START_REF] Barelli | An efficient structural attack on NIST submission DAGS[END_REF] that efficiently recovers the private key, and was improved in [START_REF] Bardet | Practical algebraic attack on DAGS[END_REF]. Here, we show that the DAGS algebraic modeling is in fact a MinRank problem. However, the previous complexity results do not apply, as those MinRank instances have a structure, that can be used to understand more precisely the complexity.

Principle of the attack

We recall some elements of the scheme. DAGS is based on the McEliece scheme and uses Quasi-Dyadic Generalized Srivastava codes, which are a subfamily of alternant codes. The structure of such codes is what allowed DAGS to be attacked [START_REF] Barelli | An efficient structural attack on NIST submission DAGS[END_REF][START_REF] Bardet | Practical algebraic attack on DAGS[END_REF].

The idea of the key-recovery attack leading to the modeling presented here is to find a subcode of the public code. The attack was proposed in two versions: a combinatorial one that uses brute force to find the subcode, and an algebraic one that relies on solving a polynomial system. The complexity of the combinatorial version is easy to compute, however the numbers of calculations remains too high to be done in practice. On the contrary, the algebraic attack is more efficient but its complexity is harder to estimate.

We focus on the second version and explain the principle. We begin by computing the invariant subcode of the public code of the scheme. Then, we search for a subcode of this invariant code by solving a bilinear system built from public parts of the scheme. Finally, we can recover the support and multiplier of the original alternant code.

In the next subsection, we explain how the system we want to solve is built.

Original Modeling

Let C pub be the DAGS public code, H pub be the public key of the scheme, which is a parity-check matrix of C pub , and let G pub be its generator matrix.

We refer to [START_REF] Macwilliams | The Theory of Error-Correcting Codes[END_REF]Chap. 12] for the definition of alternant codes. DAGS codes are quasi-dyadic alternant codes over F q m , with q a power of 2 and m = 2. To build the system we need to understand the construction of quasi-dyadic alternant codes, that are alternant codes for which the support x and the multiplier y have a particular structure. Definition 1. Let γ 1 and n = 2 γ n 0 . The support x ∈ F n q m of a quasidyadic alternant code of order 2 γ is constructed from (b 1 , . . . , b γ ) ∈ F γ q m that are linearly independent over F 2 , and τ = (τ 1 , . . . , τ n 0 ) ∈ F n 0 q m as

x def = τ ⊗ 1 2 γ + 1 n 0 ⊗ g,
where g def = (g) g∈G is a vector of all 2 γ elements of the group G = b 1 , . . . , b γ F 2 which is the vector space generated by the elements (b i ) over F 2 .

The elements τ i are randomy drawn from F q m such that the cosets τ i + G are pairwise disjoint.

For instance for γ = 2, we can choose g

= (0, b 1 , b 2 , b 1 +b 2 ) = b 1 (0, 1, 0, 1)+ b 2 (0, 0, 1, 1). For γ = 3 we take g = (0, b 1 , b 2 , b 1 + b 2 , b 3 , b 1 + b 3 , b 2 + b 3 , b 1 + b 2 + b 3 ) = b 1 (0, 1,
0, 1, 0, 1, 0, 1) + b 2 (0, 0, 1, 1, 0, 0, 1, 1) + b 3 (0, 0, 0, 0, 1, 1, 1, 1). In general, one possible order for g is given by g = γ i=1 b i e i where

e i def = (0 2 i-1 , 1 2 i-1 , 0 2 i-1 , 1 2 i-1 , . . . ) = 1 2 γ-i ⊗ (0, 1) ⊗ 1 2 i-1 .
The group G acts by translation on F q m , and its action induces a permutation of the code C pub . This is what allows the DAGS system to have reduced public keys: the public matrix G pub is formed by blocks of size 2 γ where each row of the block is deduced from the first row by one of the permutation induced by G.

The attack in [START_REF] Barelli | An efficient structural attack on NIST submission DAGS[END_REF] introduces the invariant subcode C pub G with respect to G of C pub , which is defined as Definition 2. The invariant code of C pub is defined by:

C pub G = {c ∈ C pub |∀(i, j) ∈ {0..n 0 -1} × {1..2 γ }, c i2 γ +j = c i2 γ +1 } .
The invariant subcode has dimension k 0 = k/2 γ where k is the dimension of C pub . Its generator matrix G inv is easy to compute from G pub : each block of 2 γ rows of G pub gives one row of G inv by summation. The entries of G pub are then repeated by blocks of size 2 γ , so that we can define a matrix

G ∈ F k 0 ×n 0 q m satisfying G inv = G ⊗ 1 2 γ .
We introduce the component-wise product called Schur product:

Definition 3. The Schur product of two codes A and B ⊆ F n q corresponds to the code generated by all the component-wise products of one codeword from A and one codeword of B:

A ⋆ B = a ⋆ b | a ∈ A , b ∈ B Fq
The attack in [START_REF] Barelli | An efficient structural attack on NIST submission DAGS[END_REF] amounts to find D, an unknown subcode of C pub G such that x is orthogonal to D ⋆ C pub ⊥ . This leads to following system with 2 unknowns, D and x:

G D⋆C pub ⊥ • x ⊤ = 0 (9)
Algebraically, a generator matrix for D ⋆ C pub ⊥ can be written with high probability as

I k 0 -c U • G inv ⋆ H pub (10)
with c the codimension of D in the invariant subcode C pub G . If we can not express the system like that, we just need to take another generator matrix for the invariant subcode of C pub . This finally leads to the original modeling:

I k 0 -c U G inv ⋆ H pub x ⊤ = 0 ( 11
)
where U is a matrix of unknowns of size (k 0c) × c, G inv = G ⊗ 1 2 γ and G is a public invariant matrix of size k 0 × n 0 , H pub is the public parity-check matrix, and x = τ ⊗ 1 2 γ + γ i=1 b i 1 n 0 ⊗ e i ∈ F n q m is a vector of unknowns τ = (τ 1 , . . . , τ n 0 ) and (b 1 , . . . , b γ ). Remark 3. As explained in [START_REF] Barelli | An efficient structural attack on NIST submission DAGS[END_REF], any affine map x → ax + b for a ∈ F * q m , b ∈ F q m preserves the quasi-dyadic structure of the code, and leaves the code invariant, so that it is always possible to search among all possible x for the ones that satisfy b 1 = 1 and τ n 0 = 0. Moreover, the vector x q , hence Tr(x) def = x + x q are also solution of the system [START_REF] Bruns | Determinantal Rings, lncs[END_REF], so that Tr(b 2 ) -1 Tr(x) is a solution with τ n 0 = 0, b 1 = 0 and b 2 = 1 (as Tr(a) = 0 for a ∈ F q when m = 2). Remark 4. As explained in [START_REF] Bardet | Practical algebraic attack on DAGS[END_REF], there is a lot of redundancy among the equations. We avoid that by considering only one out of every 2 γ rows in H pub .

Modeling Update

A simple (but fastidious, see Appendix A) computation allows to write the system as a MinRank instance with matrices of size

(n 0 -k 0 ) × k 0 , when G = (I k 0 G) is taken in systematic form: k 0 i=1 τ i M i + n 0 -k 0 j=1 τ j+k 0 M j+k 0 + γ b=2 b i H i I k 0 -c U ⊤ = 0 (12)
with M i = 0 i-1 (G {i}, * ) ⊤ 0 k 0 -i ∀1 ≤ i ≤ k 0

M j+k 0 =   0 j-1 (G * ,{j} ) ⊤ 0 n 0 -k 0 -j   ∀1 ≤ j ≤ n 0 -k 0 H i = H pub (I n 0 ⊗ e i ⊤ ) * ,{1..k 0 } ∀2 ≤ i ≤ γ
It is clear that the matrices M i from DAGS instances are not random, and in practice we have more degree falls than expected. On the other hand, the part concerning the variables b i with matrices H i seems to behave like a random system. Note also that experimentally we find that the system always produces 3 solutions. However, this is small enough to be able to recover the good one from the kernel of the Macaulay matrix, as only one belong to the finite field F q . Note that it is always possible to use shortened codes on a 0 positions, that amounts to consider codes with parameters (n 0a 0 , k 0a 0 ).

The first sets of parameters were given in the specifications of the scheme. They are shown in Table3. Experimental results in [START_REF] Bardet | Practical algebraic attack on DAGS[END_REF] give a solution of the system DAGS_3 in degree 4 with linear algebra on a matrix of size 725, 895× 671, 071. It is improved by shortening the system up to k 0a 0c = 4 with a matrix of size 103, 973 × 97, 980 and a computation lasting 70 seconds. All results presented here allows to choose to shorten the system to k 0 -a 0 -c = 5 instead of 4, as for 4 the system does not leads directly to linear equations, and it reduces the computation to linear algebra on a matrix of size 2772 by 4284 that last only few seconds.

Conclusion

We have presented the link between the different modelings for the MinRank problem. This allows a more accurate understanding of the best strategy to solve MinRank instances.

We have shown that superdetermined MinRank instances are instances for which (SM) solves at b = 1, and that the maximal degree in the computations is not the best parameter to use to optimize the computation.

We have also presented the DAGS attack as a particular superdetermined MinRank one, and how the accurate study of the involved matrices allows to find the best strategy.

  ) for any d ∈ {1..r}, J ⊂ {1..n -r}, #J = d + 1, T ⊂ {1..r}, #T = d and ℓ ∈ {1..m}. The authors in [24, Theorem 2] construct a matrix B J whose left kernel contains elements related to the left kernel of the Jacobian matrix in x.

1 .

 1 Then finding linear combination of the equations that produce degree falls can be done by computing the echelon form of the Macaulay matrix. For a set of rows in E(d), we have m n-and we get generically a degree fall under the condition

  , for a fixed d ∈ {0..r}, the set E(d) contains m n-V(d) of bidegree (1, d) and K n-r d+1 r d+1 variables V(d + 1) of bidegree (1, d + 1)

Proposition 2 .Table 3 :

 23 For the DAGS modeling, the Macaulay matrix associated to the set of equations E(d) has sizeN rows × N cols = (n 0k 0 ) k 0 -c d+1 c d × (n 0 -Security Level q n 0 k 0 γ c k 0a 0c Matrix size Rank Time DAGS_1 (128) 2 5 52 DAGS original sets of parameters k 0 -1 + c + γ -1) k 0 -c d+1 c d+1 , but its rank is Rank(E(d)) = min N rows , k 0c d + 1 (n 0k 0 )

Table 1 :

 1 Size of matrices on (SM) for a MinRank instance with K = 10 matrices of size m × n, for various r. n can be decreased by puncturing the matrices to get a speedup. The results have been verified experimentally on random instances.

	24]

Table 2 :

 2 Experimental size of matrices on SM for a MinRank with K = 12 matrices of size 12 × 12, for various r. It is possible to puncture the codes, by considering only n = κ + r columns of the matrices. We consider only systems for which SM solves at b = 1. The second row gives the size of a submatrix of blocks E(d) for some d that solves the problem faster.

	r κ	d	size	time	[24]
	4 8 0..4 9504 × 5940	5.6 s	58 s
		3..4 4032 × 3528	2.4 s
	7 0..4 5544 × 3960	2.1 s	38 s
	6 0..4 3024 × 2520 0.74 s 21 s
		2..4 2232 × 2220 0.52 s
	5 0..4 1512 × 1512 0.23 s 13 s
	5 7 0..5 11088 × 9504 11 s 756 s
		2..4 9660 × 9072	9.6 s
	6 0..5 5544 × 5544	3.1 s 367s

Acknowledgements

This work has been supported by the French ANR project CBCRYPT (ANR-17-CE39-0007).

A Appendix

We want to reduce [START_REF] Bruns | Determinantal Rings, lncs[END_REF] to a MinRank problem [START_REF] Buss | The computational complexity of some problems of linear algebra[END_REF]. We start from [START_REF] Bruns | Determinantal Rings, lncs[END_REF]:

Using the fact that

Now we can use the relations (A⊗a)⋆(b⊗x) = (A⋆b)⊗(a⋆x), τ ⋆I = Diag(τ ) and A ⊗ a = A(I ⊗ a) to simplify

We can now define Hi = H pub (I n 0 ⊗ e i ⊤ ) and H = H pub (I n 0 ⊗ 1 2 γ ⊤ ) and we get the system

We now simplify the products using the remark that H is the parity-check matrix corresponding to G = (I k 0 G): H = (G ⊤ I n 0 -k 0 ), and that Hi = (H i 0 n 0 -k 0 ) contains columns of zeros on the last n 0k 0 positions. This gives [START_REF] Buss | The computational complexity of some problems of linear algebra[END_REF].

[13] Casanova, A., Faugère, J., Macario-Rat, G., Patarin, J., Perret, L., Ryckeghem, J.:

GeMSS


FAIRness and Immunogenetics

Mogens Thomsen 1 , Laurence Mabile 1 , Romain David 2 , Anne Cambon-Thomsen 1 and the RDA ShaRC Interest Group 1 1 CERPOP, Université de Toulouse, Inserm, UPS, Toulouse. 2 ERINHA AISBL,101 Rue de Tolbiac, Paris, France For many decades, the immunogenetics community has been among the frontrunners in sharing data and samples, ensuring a great scientific progress in this domain. International histocompatibility workshops and scientific meetings in immunogenetics societies as EFI and ASHI have largely contributed to this progress.

In collaboration with Ubiquity press, the Open Journal of Bioresources (OJB) was created in 2014. Bioresources include not only data but also biological collections. OJB is a peer-reviewed open access journal with short papers describing bioresources dedicated to human biomedical research, providing the authors with a citable informative reference and a DOI (Digital Object Identifier). This is part of the recognition and rewarding of such important work. Finally, the citation of bioresources In journals should follow the format CoBRA as described by [START_REF] Bravo | Developing a guideline to standardize the citation of bioresources in journal articles (CoBRA)[END_REF].

In many other fields it has now been recognised that research data sharing is crucial. The Research Data Alliance (RDA) was launched in 2013 and its European branch is active in implementation of open science policy promoted by the European Commission and many institutions. The goal is to build a social and technical infrastructure to enable open sharing and re-use of data.

However, among the obstacles for sharing is the lack of recognition of the work necessary in order to make data available. To address this question, we established the "Sharing Rewards and Credit Interest Group" (ShaRC IG) in the framework of RDA in 2017 to improve academic crediting and rewarding mechanisms for scientists who strive to organise their data for potential reuse. This implies that data and related materials comply with international standards and respect the FAIR principles:

Findable / Accessible / Interoperable / Reusable. Such data can be read by machines, which is an enormous advantage with big data. In practice, making data FAIR requires considerable time, energy and expertise and it is not always clear who should contribute to the process. As a result, except in specific communities routinely dealing with big data (e.g. nuclear physics, astronomy or genetics), the FAIR principles are not considered a priority and are not implemented rigorously across disciplines & countries. Specific projects such as FAIRplus, an Innovative Medicine Initiative (IMI) EU supported project are dedicated to implementing FAIR principles in the biomedical domain.

In the era of open science it becomes essential to include sharing practices and activities in the evaluation system of scientific outputs as well as in the training of young investigators. Involving the scientific communities and professional actors is necessary to achieve a realistic, equitable and implementable scheme. Many historical or recent discoveries in immunogenetics have been based on exchange and sharing. Hence exploring criteria, practices and mechanisms that underpin sharing practices in such a community is of general value for the whole scientific and medical world. A case study involving the immunogenetics community could be organised as part of the ShaRC interest group, including questionnaires, specific sessions and comments on possible recommendations. One of the issues to carefully consider before implementing data and sample sharing is the adequate protection of personal data in line with the General data protection regulation (GDPR). General recommendations for such issues are an integral part of the RDA guidelines devoted to COVID-19 data sharing, a pressing domain worldwide.

The FAIRification process has been schematised by [START_REF] David | FAIRness Literacy: The Achilles' Heel of Applying FAIR Principles[END_REF]. There are 4 main phases and each of them needs to be approved by the community. The "preparing" and "training" phases are necessary before the pre-FAIRification phase taking into account important parameters. After the final steps 'check' and 'adjust', the data are ready for being machine-read and reused. The process of FAIRfication needs the help of data management professionals and this should be part of institutional strategies. It would be pertinent to consider including training on FAIR principles and steps towards FAIRification in immunogenetics training and we suggest that the EFI education committee considers the issue.

.

CONCLUSION

Open science and data/sample sharing are key elements in the progress of scientific knowledge. It is essential to include sharing practices and activities in the evaluation system of scientific outputs. In Immunogenetics, many historical or more recent discoveries were fostered because of sharing practices. The re-use of big data requires implementation of FAIR principles to be efficient. FAIRification needs to be adapted to each community. A case study involving the Immunogenetics community could be organised in collaboration with the SHaRC IG. For further information, contact anne.cambon-thomsen@univ-tlse3.fr.


Marius Bozga
email: fbozga@imag.fr

Oded Maler
email: maler@imag.fr

Amir Pnueli

Sergio Yovine
email: yovineg@imag.fr

Some Progress in the Symbolic Veri cation of Timed Automata ?

In this paper we discuss the practical di culty of analyzing the behavior of timed automata and report some results obtained using an experimental bdd-based extension of kronos. We have treated examples originating from timing analysis of asynchronous boolean networks and CMOS circuits with delay uncertainties and the results outperform those obtained by previous implementations of timed automata veri cation tools.

Introduction

The computational burden associated with the veri cation of discrete systems consists in representing and calculating the set of reachable states of a transition system, usually described as a product of small interacting systems. Timed systems were introduced in order to provide a more detailed level of modeling in which it is possible to re ne a statement such as \a is followed by b" into \a is followed by b within t time units". Timed formalisms for describing systems (timed automata AD94], D89], timed Petri nets BD91], timed transition systems HMP92a] or real-time process algebras NS92]) and for specifying behaviors (real-time temporal logics AH92], timed regular expressions ACM96]) allow the intuitive expression of real-life phenomena. Among these is the hard fact that it takes some time between the initiation and a completion of a change and that quantitative timing information may matter in the future evolution of a system.

In fact, after playing with timed models for some time, one starts wondering about the underlying assumptions that make \classical" untimed reasoning valid and useful. What class of real-timed systems is hiding behind each and every untimed automaton? How are discrete transitions embedded in the real time axis? Without getting too much into the details one can suggest two kinds of answers:

Asynchronous answer: we assume that changes in various system components may take arbitrary amount of time to be accomplished. From this perspective an untimed system can be viewed as a timed system with trivial 0; 1] bounds on the duration of a transition. Clearly, such an abstraction will create much more executions than a real system would.

Synchronous answer: certain assumptions are made and certain precautions are taken in order to ensure that most of the timing information can be ignored. This is the principle underlying clocked realization of sequential machines: we are not interested in the intermediate states of the next-state logic, nor whether one state variable has changed before the other. What is important is that everybody has stabilized until the next time their values are sampled.

When one is not satis ed with the type of answers suggested by the abstract untimed models or with the performance of clocked systems, timed models seem to be the next logical step (see also BS94]). It has been shown elsewhere ( D89], L89], MP95]) how a very general model of non-clocked circuits with delays can be translated into timed automata, on which one can ask all sorts of interesting timing questions ( ACD93], HNSY94] AMP95]). The only problem with these models is the amount of time (and space) that might elapse between posing the question and obtaining the answer. Indeed, it is the performance bottleneck that prevents the transfer of timing veri cation technology from theory to practice. In this paper we describe some attempts to push forward the performance limitations of current timed automata veri cation tools by augmenting the tool kronos DOTY96] with an additional bdd-based capability.

The rest of the paper is organized as follows: in Section 2 we discuss, via generic examples, the computational di culty of timed automata analysis methods and present an alternative data-structure, ndd which is used to analyze the examples in this paper. ndds are essentially nothing more than bdds over the bits of discretized clocks. In Section 3 we show the performance of the ndd implementation on benchmark examples coming from asynchronous boolean networks and compare them with other implementations, while in Section 4 we apply ndds to realistic (but small) examples of MOS circuits with up to 5 inputs and 16 transistors, in order to answer a question motivated by noise problems. We assume that the reader is familiar with the basic de nitions of timed automata and with bdds.

2 The Di culty of Timing Analysis Consider a system which can generate events out of a set T = f 1 ; : : : ; n g, such that every two consecutive occurrences of i must be separated by l i time units, while every occurrence of i must be followed by another one within u i units. Such a system can be modeled by the simple one-state timed automaton A depicted in Figure 1-a having n clocks and n transitions. Calculating the set of reachable clock con gurations is needed in order to determine which Tsequences are realizable by the system. An illustration of the calculation of the set of reachable clock con gurations for n = 2 is given in Figure 2. At the beginning, Time progresses until it reaches the smallest lower-bound (in this case, l 1 ). Since then, until the rst upper-bound is encountered (in this case, u 1 ) the transition 1 can be taken while resetting C 1 to zero. After crossing the lower bound l 2 , transition 2 can be, as well, taken, and so on. Although it might look simple for two clocks, this set can become rather complex in more dimensions! V i C i < u i : : : In general, the sets of reachable clock con gurations obtained this way can be expressed as a union of zones, that is, convex polyhedra generated by half-spaces of the form C i < k or C i ? C j < k for k in some nite subset of the integers. 3Zones admit an e cient representation using di erence-bounds matrices (dbm, D89]) on which it is easy to calculate intersection and the progress of time. As it often happens in computational geometrical problems, the di culty comes from the need to manipulate non-convex sets. In this case the representation is not canonical and a lot of work is needed in order to determine whether all the reachable states have already been encountered. It may turn out, for example, that a union of zones stored in memory is, in fact, convex and can be replaced by a single zone, but testing this possibility at every iteration is costly. Some authors ( H93], AIKY95] B96], WD94]) try to use various sorts of approximations, e.g. to use convex hulls instead of unions, but these over-approximations often tend to become too large and hence not useful.

C i l i =C i := 0 v i = 0 v i = 1 i : C i < u i C i < u i C i l i =C i := 0 C i l i =C i := 0 (a) (b)
The problem aggravates when the untimed state-space is non-trivial. Consider the two-state automaton B of Figure 1-(b). Such automaton represents a boolean input signal whose only constraint is that every two changes in its value are separated by some time t 2 l i ; u i ). An array of such automata is an unavoidable component in any model for analyzing the behavior of circuits under all possible inputs. When two such automata work in parallel, the reachable clock congurations are \distributed" among the discrete states f00; 01; 10; 11g as shown in Figure 3. This raises several problems: there might be a lot of redundancy if we represent reachable con gurations for every state separately because two states might share zones. In addition, if we use symbolic methods ( BCM + 93],

McM93]) to overcome the discrete state-explosion problem, how should they be combined4 with the dbm representation? Finally, the convergence of the set of reachable con gurations into a convex zone is usually slower than in the case of a one-state automaton.

In order to overcome these problems we have devised and implemented an alternative representation scheme for sets of clock con gurations, the Numerical Decision Diagrams (ndd, ABK + 97]) and tested its performance on these and other examples. This scheme has some major advantages over dbms (canonicity, natural combination with discrete symbolic representations) but, of course, has its own disadvantages, most notably, the sensitivity to time granularity.

The idea behind ndds is trivial. Suppose that each clock can take values in the range 0; k), and consider a discretization of time such that the possible clock values are K = f0; : : :; k ? 1g. Each clock can be treated as a bounded integer variable and any of its possible values can be encoded in binary using log k bits. Consequently, any subset of K n can be viewed as a subset of f0; 1g nlog k and represented by a bdd over n log k boolean variables. Given a xed variable ordering, this representation is canonical regardless of convexity, and it o ers bdd-based boolean operations as well as the calculation of the passage of time by simple arithmetical operations. For dense time models, two discretization schemes has been proposed in GPV94]. They are based on taking a rational constant , depending on the number of clocks such that by cutting space and time into a -grid, one obtains a discrete-time automaton which is equivalent (for all interesting purposes) to the given dense-time automaton. These two schemes require = 1=(n + 1) and = (1=2n) respectively, and involve some distortion of the passage of time or of the reset operator in order to preserve the properties of the original dense-time system (a more detailed description appears in GPV94] and ABK + 97]). We have observed, however, that the special class of automata obtained from circuits [START_REF] Lewis | Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty[END_REF]), where all the clock conditions are of the form C l or C < u, admits a slightly simpler and coarser region graph (see also HMP92]). For these automata, a discretization with = 1=n, where the passage of time is simply the addition of to all the clocks, is su cient.

Consequently, although all the reported experiments have been performed with respect to the discrete time interpretation, they can be viewed as if we used a dense time interpretation with all the constants divided by n. Approximations are used anyway in order to tackle the complexity of timing analysis ( AIKY95], H93], WD94], B96]), and we believe that playing with the granularity of time might prove to be an alternative approximation strategy.

Note that the ndd-based method is di erent from calculating the region graph of the timed automaton and then trying to encode its transition relation using some choice of boolean state variables (see also AK96] CC95]). We build a uniform discretized state-space which happens to contain one or more concrete representative of every region, and on which the passage of time is calculated by adding a time unit to every clock variable simultaneously.

We have implemented ndd-based veri cation algorithms for timed automata by using a system developed at Verimag for representing and manipulating communicating automata augmented with bounded integer variables BFK96].

This system takes such automata and translates them into bdds using one of several publicly-available bdd packages. We have used the CUDD package S95] of Colorado University. The experimental results are reported in the following sections.

Asynchronous Boolean Circuits

With the ndd representation we were able to calculate within 12 hours all reachable states of the automaton A (Figure 1-a) with 18 clocks and transitions, while a dbm-based implementation could not treat more than 5 clocks. The relative weakness of dbm in this apparently-trivial example is due to the fact that the set of reachable con gurations of this automaton converges nally to the whole clock space, by accumulating more and more zones. We were able to treat products of up to 9 B automata (Figure 1-b). The results5 are illustrated in Figure 3.

It should be noted, for the fairness of the comparison, that we have used the discrete time interpretation and have chosen clock values in the range f0,.. . ,15g { ndds are much more sensitive to the granularity of time than dbms. A more complicated example is the family of circuits depicted in Figure 5.

For every i 2 f0; : : :; n ? 1g we let the XOR of x i and x i?1 pass through a non-deterministic inertial delay bu er (the exact de nitions and the translation procedure from circuits to timed automata are described in MP95]). Every such gate is modeled by the four-state timed automaton appearing in Figure 6. The states are encoded using two Boolean variables v i and v i , the former denoting the value observed at the exit of the delay element while the latter represents the \hidden" value of the XOR. When both variables are equal we say that the state is stable and that it is excited otherwise.

XOR XOR XOR l 0 ; u 0 l 1 ; u 1 0 1 n ? 1 l n?1 ; u n?1 Fig. 5. A cascade of XOR gates with delays.

v i?1 = 1l i C i < u i =C i := 0 v i?1 = 0l i C i < u i =C i := 0 v i?1 = 0l i C i < u i v i?1 = 0l i C i < u i v i?1 = 0 v i?1 = 1Ĉ i < u i v i?1 = 0=C i := 0 v i?1 = 1=C i := 0 v i?1 = 1 ^Ci < u i v i?1 = 0 ^Ci < u i v i = 0; v i = 1 v i = 0; v i = 0 v i = 1; v i = 1 v i = 1; v i = 0 v i?1 = 0 v i?1 = 1Ĉ i < u i
Fig. 6. The automaton for every XOR gate, i 2 f0; : : : ; n ? 1g.

When n such automata are composed together we obtain a timed automaton C with 4 n discrete states and n clocks, which we let range in f0; : : :; 7g. Note that the feed-back loops make this class of automata rather hard to analyze as all the variables depend on each other. We have managed to calculate all the states reachable from the unstable state (1; 1; : : :; 1) for a cascade of up to 10 components in less than 2 hours. These results outperformed those of the dbm implementation which could handle only up to 6 gates, using the clock minimization techniques described in DY96]. Note that in both implementations it was easier to treat the more logically-involved XOR network C than the n \independent" inputs of B. This can be explained by the fact that in timed systems, independence of components is an illusion as there is a common shared variable, Time, observed and manipulated by all the components. This explains why the bdd results were more modest than initially expected. Nevertheless, the ability to analyze such a non-trivial circuit is remarkable and we could verify that under certain l and u parameters, the stable state (0; 0; : : :; 0) is never reached.

Concerning variable-ordering, we have found it most e cient to arrange the variables by component such that every discrete variable is followed by the bits of its associated clock with the most signi cant bit rst.

MOS Circuits

The next example, motivated by problems related to noise and power consumption, illustrates some pragmatic trade-o s between accuracy and e ciency as well as the e ect of other simplifying assumptions on veri cation performance.

Consider a 4-AND gate implemented by the MOS circuit of Figure 7. We assume that the system is governed by a clock with a period u X and that the inputs are static, or more precisely: each of the inputs can change its value at most once in the sub-interval 0; l X ) and remain constant in the sub-interval l X ; u X ). Concerning the transistors, we assume that they change their states t pico-seconds after the change of their inputs where t 2 l P ; u P ) for the P-MOS elements (A,B,I and J) and t 2 l N ; u N ) for the N-MOS elements (C,D,L and K).

A 4-state timed automaton, similar to the one of Figure 6 can be constructed to model every such transistor.

Although such a circuit is supposed to work in a synchronous environment, some practical problems motivate us to look at what happens on a smaller time scale. A particular question one might want to ask is: \what is the maximal (over all legal input patterns) number of transitions that may take place simultaneously?" By a transition we mean the opening or closing of a transistor, which is the main energy consumer. When two many transitions occur simultaneously, it might create noise a ecting the behavior of the chip.

While this question might be answered manually for a small circuit, it is not at all clear how to do it for a 8-AND made of 28 transistors, not to mention a 16-AND with 60 transistors, where the internal elements can \change their mind" several times within a clock cycle. It should be emphasized that unlike commonly-used SPICE simulations, where the simulation is done once for each input pattern, here the results of the calculations cover all possible legal input patterns and all delay uncertainties.

We have transformed the 4-AND circuit into 16 timed automata: 12 for the transistors and 4 for the inputs (the latter share the same clock in the range 0 to u X ), and attempted to calculate the set of reachable clock con gurations.

We have kept (l N ; u N ) = (8; 16) throughout the experiments. By taking (l P ; u P ) = (10; 20) and dividing all the constants by lcmf10; 20; 8; 16g = 2 we had to code all the transistor clocks using 4 bits. Changing l P from 10 to 8, the lcm becomes 4 and we could use only 3 bits for the clocks. Another factor which in uenced performance was the partition of the central clock period into active and non-active phases. Not surprisingly, the results were much better for (l X ; u X ) = (20; 60) than for (l X ; u X ) = (40; 60).

We have constructed an auxiliary automaton for counting the number of transitions taking place at the same time and could test whether there is an input pattern generating more than a given number of simultaneous transitions. For example, concerning the 4-AND circuit, under the parameters (l P ; u P ) = (8; 20) and (l X ; u X ) = (40; 56) we asked whether 9 simultaneous transitions are possible starting from the initial stable state where all the inputs are 0. The system gave (in 1:15 hours) a positive answer and provided the following witness sequence: (X2 "; 0) ! (fA #; D "g; 8) ! (X1 "; 88) ! (X2 #; 96) ! (fB #; C "g; 100) ! (D #; 104) ! (I "; 108) ! (A "; 112) ! (fX1 #; X2 "; X3 "; X4 "g; 120) ! (fA #; B "; C #; D "; E #; F #; G "; H "; I #g; 128)

where each pair of the form (S; t) indicates the occurrence of the event (or set of events) S after t pico-seconds since the beginning. The results of the experiments with 3-AND, 4-AND and 5-AND circuits are given in Table 4. 6We have also detected the possibilities of short-cuts (a wire connected to both 0 and 1) as we did in MY96] for a simpler example of a MOS circuit Table 1. A summary of the MOS results. The lines denoted by \reach" correspond to the calculation of the reachable states. The lines of the form \seq#n" correspond to the time it takes to answer whether there exist a sequence of n simultaneous transitions { a positive answer is indicated by ( ) and MO denotes memory over ow.

using the dbm version of kronos. While some of the assumptions we made in the modeling of transistors deviate from the physical reality (for example, we have adopted a \lazy evaluation" approach concerning transistors whose input becomes \ oating", that is, they maintain their previous status), we believe that the approach presented here can be integrated into the design methodology of MOS circuits. Once a suspicious input pattern has been detected by a tool like ours, a full-edged SPICE simulation, focused around that pattern, can be invoked in order to determine whether or not the alarm is false.

Additional Examples

Other experimental results will be reported elsewhere due to lack of space. They include Fischer's mutual exclusion protocol which has become a traditional benchmark for timed automata veri cation tools ( DOY94], WD94], LPY95], B96]). We managed to calculate the reachable states for 14 such processes. We have also veri ed (in few minutes) the manufacturing example due to A. Puri, described in DY95], where timed automata are used as an abstraction of hybrid systems.

Conclusions

We have suggested, implemented and tested an alternative method for e cient veri cation of timed automata. The essence of this method is a canonical repre-sentation of discretized sets of clocks con gurations using bdds. This method can take advantage of the symbolic representation of the untimed state-space. We were able to treat some examples that could not be treated by state-of-the-art dbm-based tools. Looking more closely at the \bit-structure" of the clock-space allows us to make an informed choice concerning the trade-o between model accuracy and computational hardness, as was demonstrated in the CMOS casestudy.

Notwithstanding the achievements, this is still not the breakthrough in timed veri cation. The main reason, as mentioned in this paper, is the hidden dependency between \syntactically-independent" components, which makes the bdds of the clock part of a system rather big.

Fig. 1 .

 1 Fig. 1. (a) A one-state automaton A with n transitions and n clocks. (b) A two-state automaton B for representing a set of input signals satisfying upper and lower bounds on the distance between two switching points.

Fig. 2 .

 2 Fig. 2. The initial sets of reachable clock con gurations of the automaton in Figure 1-(a) starting from (0; 0).

Fig. 3 .

 3 Fig. 3. The initial sets of reachable clock con gurations of the automaton in Figure 1-(b) starting from the discrete state 00 and the clock con guration (0; 0).

Fig. 4 .

 4 Fig. 4. Comparative performance of ndds and dbms for the automata A and B.

  Fig. 7. A MOS realization of the 4-AND function.

We ignore intentionally some technicalities concerning strictness of inequalities.

This problem has been addressed by Wong-Toi andDill WD94], who combined dbms and bdds and recently byBalarin B96] who encoded matrices using bdds. Both used the representations for approximate reachability analysis.

Unless otherwise stated, all the results reported here were obtained using a SUN Ultra-Sparc 1 with 256MB of memory.

The results for the 5-AND circuit (17 clocks!) were obtained on a 200MHz Pen-tiumPro with 512MB of memory.

Acknowledgement: We have bene tted from the CMOS know-how of Israel

Wagner and Ken McMillan.

? This research was supported in part by the European Community projects HYBRID EC-US-043 and INTAS-94-697. Verimag is a joint laboratory of cnrs and ujf.