The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

Well, there is indeed *one* public SHA1 collision of some *ad-hoc* files.
In real life, we're still far from being able to easily tweak the content
of a legitimate file while retaining its SHA1 fingerprint. But agreed,
we should start switching to others hash algorithms, just to be sure.
I've just put online a list of SHA-512 fingerprints for the files we 
distributes
(once again signed with by pgp key):

https://coq.inria.fr/distrib/SHA512SUMS
https://coq.inria.fr/distrib/SHA512SUMS.asc

Best regards
Pierre Letouzey

----- Mail original -----
> Hi Pierre,
> 
> Let me take advantage of this email to remind that sha1 are not anymore a
> way to guarantee the integration of a file: https://shattered.io
> I have reported this issue on the bug tracker but without any reply so far:
> https://coq.inria.fr/bugs/show_bug.cgi?id=5544
> 
> Cheers,
> 
> Théo
> 
> On mar. 22 août 2017 23:44 Pierre Letouzey 
> <pierre.letouzey AT inria.fr>
>  wrote:
> 
> >
> > Dear all,
> >
> > Good news, the Inria security team have ended its investigation of
> > coq.inria.fr,
> > and it confirmed that the integrity of the server (and its files) has not
> > been
> > compromised. The initial alert was due to a crafted bug report put on our
> > bugzilla, with some html attachment pointing to islamist messages,
> > pretending
> > to have hacked our site. But this bug report was created by a plain 
> > regular
> > bugzilla account created just before, with no further exploit. So this was
> > little
> > more than a bug spam, and yes, we're many here to consider that the admin
> > and
> > security team at Inria have quite overreacted. These matters are taken 
> > very
> > seriously nowadays...
> >
> > All the services provided by coq.inria.fr should be back to normal quite
> > soon
> > now, in particular the bugzilla is now operational again, without data
> > loss.
> > Please note that bug attachments of type text/html are now disallowed
> > (but such files could be placed in a .tgz or .zip if they are truly
> > meaningful
> > for a bug report).
> >
> > By the way, even if the Coq files available for download on
> > coq.inria.fr/distrib
> > have not been impacted by this incident, let me remind that I maintain a
> > gpg-signed
> > list of all the SHA1 fingerprints of the files we distribute:
> >
> > https://coq.inria.fr/distrib/SHA1SUMS
> > https://coq.inria.fr/distrib/SHA1SUMS.asc
> >
> > If in doubt, please refer to this list after checking for its signature.
> > Moreover, each recent Windows and Mac packages should be internally signed
> > as well.
> >
> > Sorry again for the inconvenience, quite independent from our will...
> >
> > Pierre Letouzey, for the Coq dev team
> >
> >
> >
> > ----- Mail original -----
> > >
> > > Dear all,
> > >
> > > The server behind our website coq.inria.fr has been put offline early
> > today
> > > by the Inria sysadmin staff and is awaiting further investigations.
> > > For the moment, we have very little information about what appended,
> > > we've just been told that a component of the website has been 
> > > compromised
> > > by intruders (bugzilla ? wiki ?) during the night. Unfortunately, these
> > > investigations by the Inria admins may take several days (next Tuesday
> > > is holiday here). We requested that at least the static part of the
> > website
> > > (especially downloads and documentation) be made available as soon as
> > > possible,
> > > but we still do not know yet when this will happen. Of course, we'll 
> > > keep
> > > you informed as soon as we know more about this attack and its
> > consequences.
> > >
> > > Most sorry for the inconvenience...
> > >
> > > Pierre Letouzey, for the Coq dev team
> > >
> > >
> >
>