[isabelle-dev] Broken component: jdk7u40

[Makarius]

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