illustration of data storage and cloud storage around the Eiffel tower

Inria Joint Center

Nouvelles et reportages

Dans l’actualité | reddit r/tezos

We just saw a result from INRIA (Institution which developed Ocaml and partners with Tezos ) audit. The Tezos Devs changed the library from TWEETNACL to HACL which is developed by INRIA itself.

Dans l’actualité | Franzis Kuskiefer Blog

In this second blog post I describe the process of integrating code from HACL*, a researchy crypto library, into NSS, a production library shipping to millions of people, running on a plethora of platforms. In short, how to ship (some…

Dans l’actualité | Franzis Kuskiefer Blog

HACL* (High-Assurance Cryptographic Library) is a formally verified cryptographic library in F*, developed by the Prosecco team at INRIA Paris in collaboration with Microsoft Research, as part of Project Everest. HACL* was inspired by discussions at the HACS workshop and…

Dans l’actualité | Mozilla Security Blog

Traditionally, software is produced in this way: write some code, maybe do some code review, run unit-tests, and then hope it is correct. Hard experience shows that it is very hard for programmers to write bug-free software. These bugs are…

Dans l’actualité | Microsoft Story Labs

At any point in time on any day of the week, Microsoft’s cloud computing operations are under attack: The company detects a whopping 1.5 million attempts a day to compromise its systems. Microsoft isn’t just fending off those attacks. It’s…

Dans l’actualité | F* for the Masses

The work we do these days on F* is often in service of Project Everest. The goal of Everest is to verify and deploy a drop-in replacement for the HTTPS stack, the protocol using which you are probably reading this…

Dans l’actualité | Quanta Magazine

In the summer of 2015 a team of hackers attempted to take control of an unmanned military helicopter known as Little Bird. The helicopter, which is similar to the piloted version long-favored for U.S. special operations missions, was stationed at…

Prix | Computer-Aided Verification (CAV)

Samin Ishtiaq will be receiving the 2016 CAV Award for the development of Separation Logic and for demonstrating its applicability in the automated verification of programs that mutate data structures. He is winning this award alongside Josh Berdine, a former…