Programme

Tous les exposés ont lieu en salle A008.

Exposés pléniers :

• Vincent Laporte : High-Assurance Implementations of Cryptography
  
  Implementations of cryptographic primitives (modular exponentiation of large numbers, scalar multiplication on elliptic curves, etc.) face a unique combination of challenges: they must be correct, amenable to auditing, optimized for a wide range of architectures, secure in spite of side-channel attacks, etc. As these goals tend to conflict one against each other, common practice usually focuses on some of them, at the expense of the others. At one end of the spectrum, some implementations are highly efficient but provide little correctness guaranty. At the other end, some formally verified artifacts enjoy machine-checked proofs of correctness and security but tend to execute too slowly.
  The field of high-assurance cryptography aims at providing cryptographic implementations that feature high-efficiency together with strong guaranties of correctness and security. This talk will present one line of work in this field: the Jasmin workbench. At its heart, the Jasmin programming language is designed to allow cryptography practitioners to implement efficient primitives that are amenable to formal verification. Indeed various tools allow to automatically or interactively prove a range of properties such as safety, constant-time security, functional correctness, cryptographic security. These tools operate at the level of source code. This is sound as the Jasmin compiler is certified, i.e., formally proved to be correct.
  In addition to an overview of the Jasmin infrastructure, this talk will discuss recent achievements as well as open questions.
  
  
• Guillaume Moroz : Efficient approximation of polynomials
  
  In modern numerical computations, real numbers are approximated with floating-point numbers, of the form $s 2^e$, where $s$ and $e$ are integers with a fixed precision. This representation is compact and can represent numbers with small and large magnitudes. In this talk, we will generalize this idea to approximate univariate polynomial functions with piecewise polynomials of the form $s(X) X^e$ where $s$ is a polynomial of fixed degree and $e$ is an integer. Using tools such as the Newton polygon, this representation can be computed efficiently both in theory and in practice. Moreover, it can be used to efficiently evaluate and find roots approximations of a high-degree polynomial.
  
  
• Jean-Michel Muller : Obtaining error bounds that are certain, sharp… and whose proof is trustable: the curse of long and boring proofs
  
  We are interested in obtaining very sharp (indeed: asymptotically optimal) and certain (i.e., no « + O(u^k) » terms) error bounds for floating-point algorithms of medium size (say, less than around 20 operations). Unfortunately, this seems to imply that the proofs of these algorithms become long and tedious, so that almost nobody reads them in detail: the consequence is that it is not unlikely that they contain errors, that can remain unnoticed for years. We illustrate this problem with examples taken from computer arithmetic: addition and multiplication of « double word » numbers, and evaluation of the hypotenuse (sqrt(x^2+y^2)) function. We discuss what computer algebra and formal proof bring to us, and the medium-term implication on the very notion of « publishing a proof » in an article.
  
  

---

• 09h00 Vincent Laporte : High-Assurance Implementations of Cryptography
• 10h00 Coffee break
• 11h00 Youssef Fakhreddine : Using loop transformations for precision tuning in iterative programs
• 11h30 Orégane Desrentes : Exact Fused Dot Product Add Operators
• 12h00 Tom Hubrecht : A correctly rounded power function in double precision

• 14h30 Guillaume Melquiond : Gappa, 20 ans après
• 15h00 Sylvain Chevillard : Sur l’optimalité d’une implémentation particulière de la fonction sinus
• 15h30 Joris Picot : Error in ulps of the multiplication or division by a correctly-rounded function or constant in binary floating-point arithmetic
• 16h00 Coffee break

• 17h00 Assemblée Générale du GT Arith

---

• 09h00 Guillaume Moroz : Efficient approximation of polynomials
• 10h00 Coffee break
• 10h30 Bastien Laboureix : Connexité des hyperplans arithmétiques
• 11h00 Leo Pradels : Pattern-Aware Pruning for Pipelined CNN Acceleration