[isabelle-dev] Use HTTPS for components

[Lawrence Paulson]

I’m not sure that digitally signed components are really something to work on now. Are we really concerned about malicious attacks against our servers?
Larry

> On 13 Jul 2016, at 00:56, Gerwin Klein <Gerwin.Klein at nicta.com.au> wrote:
> 
> I agree, we should do that.
> 
> Ideally, we should actually sign those components. The downloading/receiving/checking side is not too hard to automate, but it would require entering the private key keyphrase when you are signing (providing) a new component.
> 
> Cheers,
> Gerwin
> 
>> On 13 Jul 2016, at 08:28, Lars Hupel <hupel at in.tum.de> wrote:
>> 
>> Dear Isabelle developers,
>> 
>> all of the critical Isabelle infrastructure (even website mirrors) is
>> reachable via HTTPS. For Jenkins, it's not so important. For executable
>> code, it is very important. Hence I would like to propose a simple
>> change in the global "etc/settings":
>> 
>> -ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
>> +ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"
>> 
>> Because we don't sign components, we should at least make them available
>> over HTTPS. This is the bare minimum according to security best practices.
>> 
>> Potential disadvantage: Fetching from HTTPS using Perl's libwww requires
>> an addon package ("LWP-Protocol-https").
>> 
>> Potential remedy: Switch to curl for fetching components
>> - readily available everywhere
>> - less Perl required
>> 
>> (Note that it appears that that specific Perl addon is not available
>> under Cygwin.)
>> 
>> I don't think we should let shortcomings of some Perl module dictate a
>> lack of security.
>> 
>> Cheers
>> Lars
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> ________________________________
> 
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev