On Tue, 17 Sep 2013, Lars Hupel wrote:
The reason why I didn't consider "external" issues is that I was under
the impression that the integrity of the downloaded artifacts is checked
against `Admin/components/components.sha1`, but apparently that is not
the case. Is there a reason for that?
First of all there is a bootstrap problem: "isabelle components" needs to
work without any sophisticated things available yet. It is mainly a
little bit of bash with a little bit of perl. The assumption of perl with
libwww is already stronger than I would like to see. Today I usually
prefer system programming in Isabelle/Scala, but that is not available for
download of components yet.
More generally there is also the principle of keeping things as simple as
possible, but not simpler. Making big infrastructure for secure
downloads, integrity checks etc. will introduce new problems due to that
very infrastructure. That is an inevitable consequence of all engineering
-- you can basically never win in this escalation of machinery. (We have
already a bit more infrastructure at TUM than active maintainers for it.)
There is also a security concern here: A (random) repository snapshot
can be easily obtained via HTTPS, but downloading the components happens
via (untrusted) HTTP by default, without further integrity checks.
There is no security about anything of Isabelle sources, Isabelle
components, Isabelle downloads, not even for official releases. The
network at TUM is wide open and insecure. I know that is ridicous for a
system that is targeted to produce proven formal material, but I prefer to
tell the plain truth over obscurity.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
