Software

  • Math-Components





    • The Mathematical Components library is a set of Coq libraries that cover the prerequisites for the mechanization of the proof of the Odd Order Theorem.



    • Major release using Hierarchy Builder to handle algebraic structures.



    • Alexey Solovyev (alexey.solovyev@inria.fr), Andrea Asperti (asperti@cs.unibo.it), Assia Mahboubi (assia.mahboubi@inria.fr), Cyril Cohen (cyril.cohen@inria.fr), Enrico Tassi (enrico.tassi@inria.fr), François Garillot (francois.garillot@inria.fr), Georges Gonthier (georges.gonthier@inria.fr), Ioana Pasca (ioana.pasca@inria.fr), Jeremy Avigad (jeremy.avigad@inria.fr), Laurence Rideau (laurence.rideau@inria.fr), Laurent Théry (laurent.thery@inria.fr), Russell O'Connor (r.oconnor@cs.ru.nl), Sidi Ould Biha (Sidi.Ould_Biha@inria.fr), Stéphane Le Roux (stephane.le.roux@ulb.ac.be), Yves Bertot (yves.bertot@inria.fr)



    • Assia Mahboubi (assia.mahboubi@inria.fr)


    • https://math-comp.github.io/
  • Coq




    • Coq is an interactive proof assistant based on the Calculus of (Co-)Inductive Constructions, extended with universe polymorphism. This type theory features inductive and co-inductive families, an impredicative sort and a hierarchy of predicative universes, making it a very expressive logic. The calculus allows to formalize both general mathematics and computer programs, ranging from theories of finite structures to abstract algebra and categories to programming language metatheory and compiler verification. Coq is organised as a (relatively small) kernel including efficient conversion tests on which are built a set of higher-level layers: a powerful proof engine and unification algorithm, various tactics/decision procedures, a transactional document model and, at the very top an integrated development environment (IDE).


    • Coq provides both a dependently-typed functional programming language and a logical formalism, which, altogether, support the formalisation of mathematical theories and the specification and certification of properties of programs. Coq also provides a large and extensible set of automatic or semi-automatic proof methods. Coq's programs are extractible to OCaml, Haskell, Scheme, …


    • Coq version 8.18 integrates changes to several parts of the system :
      kernel, specification language, type inference, notation, tactics, Ltac2 language,
      commands and options, command-line tools, CoqIDE, standard library,
      infrastructure and dependencies, extraction.
      See https://coq.inria.fr/refman/changes.html#version-8-18 for an overview of the new features and changes, along with the full list of contributors.


    • An overview of the new features and changes, along with the full list of contributors is available at https://coq.inria.fr/refman/changes.html#version-8-18 .



    • Yves Bertot (Yves.Bertot@inria.fr), Frédéric Besson (frederic.besson@inria.fr), Tej Chajed (tchajed@mit.edu), Cyril Cohen (cyril.cohen@inria.fr), Pierre Corbineau (pierre.corbineau@imag.fr), Pierre Courtieu, Maxime Dénès (maxime.denes@inria.fr), Jim Fehrle (jim.fehrle@gmail.com), Julien Forest (julien.forest@ensiie.fr), Emilio Jesús Gallego Arias (e@x80.org), Gaëtan Gilbert (gaetan.gilbert@inria.fr), Georges Gonthier (Georges.Gonthier@inria.fr), Benjamin Grégoire (Benjamin.Gregoire@inria.fr), Jason Gross (jgross@mit.edu), Hugo Herbelin (Hugo.Herbelin@inria.fr), Vincent Laporte (vincent.laporte@inria.fr), Olivier Laurent (olivier.laurent@ens-lyon.fr), Assia Mahboubi (Assia.Mahboubi@inria.fr), Kenji Maillard (kenji.maillard@inria.fr), Érik Martin-Dorel (erik.martin-dorel@irit.fr), Guillaume Melquiond (guillaume.melquiond@inria.fr), Pierre-Marie Pedrot (Pierre-Marie.Pedrot@inria.fr), Clément Pit-Claudel, Kazuhiko Sakaguchi (kazuhiko.sakaguchi@inria.fr), Vincent Semeria (vincent.semeria@gmail.com), Michael Soegtrop (michael.soegtrop@intel.com), Arnaud Spiwack, Matthieu Sozeau (Matthieu.Sozeau@inria.fr), Enrico Tassi (Enrico.Tassi@inria.fr), Laurent Théry (laurent.thery@inria.fr), Anton Trunov (anton.a.trunov@gmail.com), Li-Yao Xia, Theo Zimmermann (theo.zimmermann@inria.fr)



    • Matthieu Sozeau (matthieu.sozeau@inria.fr)


    • http://coq.inria.fr/
  • Ssreflect




    • Ssreflect is tactic language that helps writing concise and uniform tactic based proof scripts for the Coq system. It was designed during the proofs of the 4 Color Theorem and the Feit-Thompson theorem.


    • Ssreflect is a tactic language extension to the Coq system, developed by the Mathematical Components team.





    • Assia Mahboubi (assia.mahboubi@inria.fr), Cyril Cohen (cyril.cohen@inria.fr), Enrico Tassi (Enrico.Tassi@inria.fr), Georges Gonthier (georges.gonthier@inria.fr), Laurence Rideau (Laurence.Rideau@inria.fr), Laurent Théry (Laurent.Thery@inria.fr), Yves Bertot (Yves.Bertot@inria.fr)



    • Yves Bertot (Yves.Bertot@inria.fr)


    • http://math-comp.github.io/math-comp/
  • Easycrypt





    • EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs. EasyCrypt can also be used for reasoning about differential privacy.


    • The major release (2023.09) has been published. This release include the a new logic for bounding the expectation of function in a probabilistic program.


    • This version introduces a new logic (ehoare) allowing to bound the expectation of a function in a probabilistic program.

      • Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, et al.. High-Assurance Cryptography in the Spectre Era. S&P 2021 – IEEE Symposium of Security and Privacy, May 2021, Virtual, France. ⟨10.1109/SP40001.2021.00046⟩. ⟨hal-03352062⟩
      • Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS 2021 – ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩. ⟨hal-03469015⟩



    • Benjamin Grégoire (Benjamin.Gregoire@inria.fr), Gilles Barthe (Gilles.Barthe@inria.fr), Pierre-Yves Strub (pierre-yves.strub@inria.fr), Adrien Koutsos (adrien.koutsos@inria.fr)



    • Gilles Barthe (Gilles.Barthe@inria.fr)


    • https://github.com/EasyCrypt/easycrypt
  • Jasmin





    • The Jasmin programming language smoothly combines high-level and low-level constructs, so as to support “assembly in the head” programming. Programmers can control many low-level details that are performance-critical: instruction selection and scheduling, what registers to spill and when, etc. The language also features high-level abstractions (variables, functions, arrays, loops, etc.) to structure the source code and make it more amenable to formal verification. The Jasmin compiler produces predictable assembly and ensures that the use of high-level abstractions incurs no run-time penalty.

      The semantics is formally defined to allow rigorous reasoning about program behaviors. The compiler is formally verified for correctness (the proof is machine-checked by the Coq proof assistant). This ensures that many properties can be proved on a source program and still apply to the corresponding assembly program: safety, termination, functional correctness…

      Jasmin programs can be automatically checked for safety and termination (using a trusted static analyzer). The Jasmin workbench leverages the EasyCrypt toolset for formal verification. Jasmin programs can be extracted to corresponding EasyCrypt programs to prove functional correctness, cryptographic security, or security against side-channel attacks (constant-time).



    • On June 2023, a major release (2023.06.0) has been published.


    • 2023.06.0 is a major release of Jasmin. It contains a few noteworthy changes that follows. Local functions now use call and ret instructions. The ARMv7 (i.e., Cortex-M4) architecture is now experimentally supported. A few aspects of the safety checker can be finely controlled through annotations or command-line flags. Shift and rotation operators have a simpler semantics.

      As usual, it also brings in various fixes and improvements, such as bit rotation operators and automatic slicing of the input program.


      • Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, et al.. Typing High-Speed Cryptography against Spectre v1. SP 2023- IEEE Symposium on Security and Privacy, IEEE, May 2023, San Francisco, United States. pp.1592-1609, ⟨10.1109/SP46215.2023.10179418⟩. ⟨hal-04106448⟩
      • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, et al.. Formally verifying Kyber: Episode IV: Implementation correctness. CHES 2023 – Conference on Cryptographic Hardware and Embedded Systems, IACR, Sep 2023, Praha, Czech Republic. pp.164-193, ⟨10.46586/tches.v2023.i3.164-193⟩. ⟨hal-04218417⟩
      • Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya. Enforcing Fine-grained Constant-time Policies. CCS 2022 – 2022 ACM SIGSAC Conference on Computer and Communications Security, Nov 2022, Los Angeles CA, United States. pp.83-96, ⟨10.1145/3548606.3560689⟩. ⟨hal-03844366⟩
      • Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya. Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS 2021 – ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.462-476, ⟨10.1145/3460120.3484761⟩. ⟨hal-03430789⟩
      • Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, et al.. High-Assurance Cryptography in the Spectre Era. S&P 2021 – IEEE Symposium of Security and Privacy, May 2021, Virtual, France. ⟨10.1109/SP40001.2021.00046⟩. ⟨hal-03352062⟩
      • José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, et al.. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS 2019 – 26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.1607-1622, ⟨10.1145/3319535.3363211⟩. ⟨hal-02404581⟩
      • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, et al.. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. SP 2020 – 41st IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.965-982, ⟨10.1109/SP40000.2020.00028⟩. ⟨hal-02974993⟩
      • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, et al.. Jasmin: High-Assurance and High-Speed Cryptography. CCS 2017 – Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-17. ⟨hal-01649140⟩



    • Gilles Barthe (Gilles.Barthe@inria.fr), Benjamin Grégoire (Benjamin.Gregoire@inria.fr), Adrien Koutsos (adrien.koutsos@inria.fr), Vincent Laporte (vincent.laporte@inria.fr), Jean-Christophe Léchenet (jean-christophe.lechenet@inria.fr), Swarn Priya (swarn.priya@inria.fr), Santiago Arranz Olmos (santiago.arranz-olmos@mpi-sp.org)


    • The IMDEA Software Institute, Ecole Polytechnique, Universidade do Minho, Universidade do Porto, Max Planck Institute for Security and Privacy


    • Jean-Christophe Léchenet (jean-christophe.lechenet@inria.fr)


    • https://github.com/jasmin-lang/jasmin
  • MaskVerif





    • MaskVerif is a tool to verify the security of implementations protected against side channel attacks,
      in particular differential power analysis.
      It allows to check different security notions in the probing model:
      – Probing security
      – Non Interference
      – Strong Non Interference.
      The tool is able to analyse software implementations and hardware implementations (written in Verilog).
      It can prove the different security notions in presence of glitch or transition.







    • Benjamin Grégoire (benjamin.gregoire@inria.fr)


    • https://sites.google.com/view/maskverif/home
  • MaskComp





    • MaskComp is a compiler generating masked implementations protected against side channel attacks based on differential power analysis.
      It takes a unmasked program in a syntax close to C and generates a new C protected program.
      We do not claim that the generated C program will be secure after compilation (the C compiler may break protection), but
      it provides a good support for generating masked implementation.







    • Benjamin Grégoire (benjamin.gregoire@inria.fr)


    • https://sites.google.com/site/maskingcompiler/home
  • AutoGnP





    • autoGnP is an automated tool for analyzing the security of padding-based public-key encryption schemes (i.e. schemes built from trapdoor permutations and hash functions). This years we extended the tool to be able to deal with schemes based on cyclic groups and bilinear maps.





    • Benjamin Grégoire (Benjamin.Gregoire@inria.fr), Gilles Barthe (Gilles.Barthe@inria.fr), Pierre-Yves Strub (pierre-yves.strub@inria.fr)



    • Gilles Barthe (Gilles.Barthe@inria.fr)


    • https://github.com/ZooCrypt/AutoGnP
  • coq-elpi




    • Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq terms into lambdaProlog using the Higher-Order Abstract Syntax approach (HOAS) and a way to read terms back. In addition to that it exports to ELPI a set of Coq primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in lambdaProlog. E.g. {{nat}} is expanded to the type name of natural numbers, or {{A -> B}} to the representation of a product by unfolding the -> notation. Finally it provides a way to define new vernacular commands and new tactics.


    • Coq plugin embedding ELPI


    • – Separation of parsing/execution for modern UIs.
      – Application of type-checking to solve type class instances using an ELPI program.
      – Application of coercion to insert explicit type casts using an ELPI program.


    • – parsing/execution separation

      • Enrico Tassi. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. ITP 2019 – 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩. ⟨hal-01897468v2⟩
      • Enrico Tassi. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect). 2018. ⟨hal-01637063⟩



    • Enrico Tassi (Enrico.Tassi@inria.fr), Davide Fissore (davide.fissore@inria.fr)



    • Enrico Tassi (enrico.tassi@inria.fr)



  • ELPI




    • The programming language has the following features

      – Native support for variable binding and substitution, via a Higher Order Abstract Syntax (HOAS) embedding of the object language. The programmer does not need to care about technical devices to handle bound variables, like De Bruijn indices.

      – Native support for hypothetical context. When moving under a binder one can attach to the bound variable extra information that is collected when the variable gets out of scope. For example when writing a type-checker the programmer needs not to care about managing the typing context.

      – Native support for higher-order unification variables, again via HOAS. Unification variables of the meta-language (lambdaProlog) can be reused to represent the unification variables of the object language. The programmer does not need to care about the unification-variable assignment map and cannot assign to a unification variable a term containing variables out of scope, or build a circular assignment.

      – Native support for syntactic constraints and their meta-level handling rules. The generative semantics of Prolog can be disabled by turning a goal into a syntactic constraint (suspended goal). A syntactic constraint is resumed as soon as relevant variables get assigned. Syntactic constraints can be manipulated by constraint handling rules (CHR).

      – Native support for backtracking, to ease implementation of search.

      – The constraint store is extensible. The host application can declare non-syntactic constraints and uses custom constraint solvers to check their consistency.

      – Clauses are graftable. The user is free to extend an existing program by inserting/removing clauses, both at runtime (using implication) and at "compilation" time by accumulating files.

      Most of these features come with lambdaProlog. Constraints and propagation rules are novel in ELPI.



    • ELPI implements a variant of lambdaProlog enriched with Constraint Handling Rules, a programming language well suited to manipulate syntax trees with binders and unification variables.

      ELPI is a research project aimed at providing a programming platform for the so called elaborator component of an interactive theorem prover.

      ELPI is designed to be embedded into larger applications written in OCaml as an extension language. It comes with an API to drive the interpreter and with an FFI for defining built-in predicates and data types, as well as quotations and similar goodies that come in handy to adapt the language to the host application.



    • – Time complexity improvement of separate compilation/linking of program units, which is now pseudo linear.
      – The runtime was made re-entrant, allowing multiple Elpi instances to live in the same process.
      – New deep-indexing data structure based on discrimination trees.


    • – Faster separate compilation/linking

      • Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. Practical and sound equality tests, automatically — Deriving eqType instances for Jasmin’s data types with Coq-Elpi. CPP ’23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston MA USA, France. pp.167-181, ⟨10.1145/3573105.3575683⟩. ⟨hal-03800154⟩
      • Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. ELPI: fast, Embeddable, λProlog Interpreter. Proceedings of LPAR, Nov 2015, Suva, Fiji. ⟨hal-01176856⟩
      • Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. Implementing Type Theory in Higher Order Constraint Logic Programming. Mathematical Structures in Computer Science, 2019, 29 (8), pp.1125-1150. ⟨hal-01410567v3⟩
      • Enrico Tassi. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. ITP 2019 – 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩. ⟨hal-01897468v2⟩



    • Enrico Tassi (Enrico.Tassi@inria.fr), Claudio Sacerdoti Coen (claudio.sacerdoticoen@unibo.it)



    • Enrico Tassi (enrico.tassi@inria.fr)


    • https://github.com/lpcic/elpi/
  • Semantics





    • A didactical Coq development to introduce various semantics styles. Shows how to derive an interpreter, a compiler, a verifier, or a program analyser from formal descriptions, and how to prove their consistency.

      This is a library for the Coq system, where the description of a toy programming language is presented. The value of this library is that it can be re-used in classrooms to teach programming language semantics or the Coq system. The topics covered include introductory notions to domain theory, pre and post-conditions, abstract interpretation, compilation, and the proofs of consistency between all these points of view on the same programming language. Standalone tools for the object programming language can be derived from this development.




    • This version now contains an example of small compiler and a partial correctness proof (completeness).



    • Christine Paulin (Christine.Paulin@lri.fr), Yves Bertot (Yves.Bertot@inria.fr)



    • Yves Bertot (Yves.Bertot@sophia.inria.fr)


    • https://github.com/coq-community/semantics
  • CoqInterval





    • CoqInterval is a library for the proof assistant Coq.

      It provides several tactics for proving theorems on enclosures of real-valued expressions. The proofs are performed by an interval kernel which relies on a computable formalization of floating-point arithmetic in Coq.

      The Marelle team developed a formalization of rigorous polynomial approximation using Taylor models in Coq. In 2014, this library has been included in CoqInterval.






    • Assia Mahboubi (assia.mahboubi@inria.fr), Érik Martin-Dorel (erik.martin-dorel@irit.fr), Guillaume Melquiond (guillaume.melquiond@inria.fr), Jean-Michel Muller (jean-michel.muller@inria.fr), Laurence Rideau (laurence.rideau@inria.fr), Laurent Théry (laurent.thery@inria.fr), Micaela Mayero (mayero@lipn.univ-paris13.fr), Mioara Joldes (joldes@laas.fr), Nicolas Brisebarre (nicolas.brisebarre@inria.fr), Thomas Sibut-Pinote (thomas.sibut-pinote@inria.fr)



    • Guillaume Melquiond (guillaume.melquiond@inria.fr)


    • https://coqinterval.gitlabpages.inria.fr/
  • VsCoq





    • VsCoq is an extension for Visual Studio Code (VS Code) and VSCodium which provides support for the Coq Proof Assistant.

      VsCoq is distributed in two flavours:

      – VsCoq Legacy (required for Coq < 8.18, compatible with Coq >= 8.7) is based on the original VsCoq implementation by C.J. Bell. It uses the legacy XML protocol spoken by CoqIDE.

      – VsCoq (recommended for Coq >= 8.18) is a full reimplementation around a language server which natively speaks the LSP protocol.



    • The first version (2.0.1) of VsCoq based on the LSP protocol has been released on September, 2023.


    • We have mainly been working on stability and bug fixes, in this release you’ll find :

      – Some improvements to performance on large files.
      – Fixing document state invalidation bugs.
      – Goal view improvements.






    • Laurent Théry (Laurent.Thery@inria.fr)


    • https://github.com/coq-community/vscoq

 

Comments are closed.