Suggestions for funding us.metamath.org and transitioning off of us2.metamath.org?

[David A. Wheeler]

Currently the public metamath web pages are generated on us2.metamath.org,
a computer in Norm's home, and then transferred to us.metamath.org (hosted by Linode)
where most people see the results.

Susan Cass, Norm's partner, is currently paying for Linode hosting
and providing a home for us2.metamath.org. However, she'd like someone else to
pay for Linode hosting, and wants to transfer the work elsewhere
(so she doesn't need to be responsible for it).
She'd like that done preferably by mid-June 2022 or so. I think that's perfectly reasonable.

I'll find out the cost of the Linode server, and I'm willing to help fund it.
I may not be able to pay for it all, depend on its costs.
If others are willing to contribute financially please let me/us know.

In addition, does anyone have suggestions for how to replace us2.metamath.org
to generate the website? I think it should be a cloud service so we aren't dependent on someone's home.
One obvious option is to also move site generation to us.metamath.org on Linode.
Then the site can be re-created each day, & then moved over to its public display,
on the same machine. I don't know if that would significantly increase our Linode bill;
does someone else know? If there are other reasonable options, please reply!

There are many other ways to distribute information, but I think it's nice to have
simple static HTML files, so I don't think we need to rewrite it all use dynamic generation.
In any case, I think it'd be safer to switch computers first, and then consider massive
changes to approach as a separate step.

--- David A. Wheeler

[Scott Fenton]

I’m willing to contribute financially to a Metamath server. We might want to consider hosting on a cloud service so we only pay big when there’s high traffic. I don’t know enough about traffic to us.metamath.org to know if that makes sense, though.

> On Mar 18, 2022, at 8:02 PM, David A. Wheeler <dr.david....@gmail.com> wrote:
>
> Currently the public metamath web pages are generated on us2.metamath.org,

> --
> You received this message because you are subscribed to the Google Groups "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0B163B4E-D5C8-4455-9599-C5FF768CAC62%40dwheeler.com.

[Jim Kingdon]

Assuming we stick with the current linode set up, running us2 on the
same linode is perhaps simplest. Whether that changes the cost, as far
as I could tell from glancing at https://www.linode.com/pricing/ ,
depends on how close we are to the limits for RAM, storage, etc. Perhaps
linode has an admin page which shows where we stand, and/or logging into
us2 and observing the job run can help estimate?

I'm potentially in for some sort of monthly donation. Any ideas on
whether something like https://opencollective.com/ is overkill for
managing the money? At first glance it would appear to make it easier to
do things like make it possible for all the donors to see what is being
spent on what and the like, but I've never set one up so I don't know
whether it is a lot of hassle (compared with something more informal,
which I suppose is the alternative).

As for dynamic versus static, I suppose it is to some extent a tradeoff
between RAM/CPU on the dynamic side, versus storage on the static side,
but even if I was sure how those tradeoffs might work out (I'm not),
seems like we should not expect a change of that magnitude to happen
quickly (just in terms of the software development involved - whether
that is entirely new code to generate the pages, or even just a way to
add enough duck tape to make the existing code to function dynamically,
assuming that's even feasible).

Another approach - which I suppose has at least some of the same issues
in terms of writing new code or at least scripts, investigation, etc,
would be pushing static HTML to Github Pages (
https://docs.github.com/en/pages for those not familiar). I suppose this
would involve taking the job which now runs on us2 and having it push
the pages to a git repository which is for the purpose of holding the
generated HTML. I know our generated HTML is pretty big (am I
remembering 2Gbyte correctly and if so has it changed since then?) and
perhaps there are limitations of github pages (or similar services)
which mean this wouldn't work, and I think it falls in the same bucket
as a dynamic site, in terms of being a change in approach.

[Cris Perdue]

David's "obvious option" seems like a great way to start:

> One obvious option is to also move site generation to us.metamath.org on Linode.
> Then the site can be re-created each day, & then moved over to its public display,
> on the same machine. 

Yes indeed. I would say just perform the process that way a couple of times, then look at any extra charges that occur. Judging from Linode's price list, I would expect maybe a slight charge for the CPU time used by build steps, but that's about all.  If the builds need more resources, e.g. more RAM or SSD, then the monthly rate might go up. But in such a case you will see that either the build will get very slow or you will get a complaint that the system has run out of storage (SSD).

You would probably want to "move" the site by renaming rather than copying, hopefully just renaming one top-level directory.  A couple of renames can be done in a tiny fraction of a second, and with an absolute minimum number of intermediate states.  A copy on the other hand has almost limitless numbers of intermediate states that can occur if it is interrupted, runs out of space, or whatever, and can take a quite noticeable amount of time. Any of this is liable to leave the public site in some inconsistent and/or undesirable state.

-Cris

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/61f986f0-aab4-5ca2-35e2-cac3fa09f987%40panix.com.

[Mingli Yuan]

I would like to raise an issue of cybersecurity if any one wants to take charge of any server.

We heard of the news that the linux code repository was hacked before.

That means we need to patch the server routinely and upgrade the OS at least.

Do we have md5 check of files in release?

Mingli

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAOoe%3DWKhv6K7bTOJRtL00QQVRFWJhTOHhGHs8yS-qApbm9Cp-A%40mail.gmail.com.

[Mázsa Péter]

On 3/19/22, Mingli Yuan <mingl...@gmail.com> wrote:
> I would like to raise an issue of cybersecurity if any one wants to take
> charge of any server.
> We heard of the news that the linux code repository was hacked before.
> That means we need to patch the server routinely and upgrade the OS at
> least.

https://serverpilot.io/features/#security
does this for you (combined with a digitalocean server)

On 3/19/22, Jim Kingdon <kin...@panix.com> wrote:
> Another approach - which I suppose has at least some of the same issues
> in terms of writing new code or at least scripts, investigation, etc,
> would be pushing static HTML to Github Pages (
> https://docs.github.com/en/pages for those not familiar). I suppose this
> would involve taking the job which now runs on us2 and having it push
> the pages to a git repository which is for the purpose of holding the
> generated HTML. I know our generated HTML is pretty big (am I
> remembering 2Gbyte correctly and if so has it changed since then?) and
> perhaps there are limitations of github pages (or similar services)

This limit is 1 GB:
https://docs.github.com/en/pages/getting-started-with-github-pages/about-github-pages#usage-limits


P.

[Cris Perdue]

Hi Dear (Meta)math heads,

On Sat, Mar 19, 2022 at 3:47 AM Mázsa Péter <pe...@mazsa.com> wrote:

On 3/19/22, Mingli Yuan <mingl...@gmail.com> wrote:
> I would like to raise an issue of cybersecurity if any one wants to take
> charge of any server.
> We heard of the news that the linux code repository was hacked before.
> That means we need to patch the server routinely and upgrade the OS at
> least.

https://serverpilot.io/features/#security
does this for you (combined with a digitalocean server)

Please try not to worry too much about the details of different services.  I have no doubt Linode will be a more than adequate platform. And I say this as someone with quite a bit of real-world experience running and managing mission-critical Linux servers.

It is good to document operational practices including security practices, and I'll bet David and whoever helps him will be glad to do that. Norm made a good start toward that.

About OS upgrades, Linode has a pretty slick system for upgrading your kernel. You just select your new kernel from a list in their web interface and ask it to reboot your server. The Linux package managers do a great job making it easy to update installed packages.

-Cris

[Alexander van der Vekens]

I’m also willing to contribute financially to a Metamath server.

[Mázsa Péter]

I’m also willing to contribute financially to the serverpilot.io
service for a sever, because
"(...) The number one thing that I loathed about managing my own VPS, was
security. A fully-fledged Linux instance, exposed to the public
Internet 24/7, is a big responsibility(1). There are plenty of
attack(2) vectors: SSH credentials(3) compromise; inadequate firewall
setup(4); HTTP or other DDoS'ing(5); web application-level
vulnerabilities (SQL injection(6), XSS(7), CSRF(8), etc); and
un-patched system-level vulnerabilities (Log4j(9), Heartbleed(10),
Shellshock(11), etc). Unless you're an experienced full-time security
specialist, *and* you're someone with time to spare (and I'm neither
of those things), there's no way you'll ever be on top of all that. (...)"(12)

(1) https://www.cyberciti.biz/tips/linux-security.html
(2) https://access.redhat.com/documentation/en-us/red_hat_enterprise_linux/6/html/security_guide/sect-security_guide-common_exploits_and_attacks
(3) https://cloudsecurityalliance.org/blog/2014/03/05/youre-already-compromised-exposing-ssh-as-an-attack-vector/
(4) https://www.cyberciti.biz/faq/howto-configure-setup-firewall-with-ufw-on-ubuntu-linux/
(5) https://www.ubuntufree.com/how-to-stop-a-ddos-attack-on-ubuntu/
(6) https://xkcd.com/327/
(7) https://owasp.org/www-community/attacks/xss/
(8) https://encyclopedia.kaspersky.com/glossary/cross-site-request-forgery-csrf-xsrf/
(9) https://hackernoon.com/0-day-log4shell-is-serious-but-its-just-the-tip-of-the-iceberg
(10) https://www.cisa.gov/uscert/ncas/alerts/TA14-098A
(11) https://securityintelligence.com/articles/shellshock-vulnerability-in-depth/
(12) https://greenash.net.au/thoughts/2022/03/i-dont-need-a-vps-anymore/

P.

On 3/23/22, 'Alexander van der Vekens' via Metamath

> --
> You received this message because you are subscribed to the Google Groups
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to metamath+u...@googlegroups.com.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/metamath/c4f114b0-5a22-4e80-8b03-f6bbf384a489n%40googlegroups.com.
>

[Mázsa Péter]

Cris, we can use it with Linode as well:
1. https://serverpilot.io/docs/how-to-create-a-server-on-linode/
2. https://serverpilot.io/docs/how-to-use-linode-longview/
3. https://serverpilot.io/docs/how-to-connect-a-server-to-serverpilot/

P.

[Cris Perdue]

Hello Péter,

Oh dear. We could have a huge discussion about Linux security in general and ServerPilot in particular, but let's not do that. Just now I have glanced at your items (1), (2), and (12) in your list of 12. Numbers 1 and 2 are pretty standard and reasonable lists of things to watch out for in Linux security. Number 12 is the one you quote, and of turns out to be of particular interest to me.

The author of (12) has transitioned to Netlify. I use Netlify, and I love it!  And yes, I would much rather have my own website on Netlify than have to manage my own virtual private server, though the author of (12) over-dramatizes the issues a bit.

In fact, when you guys were first looking at transitioning to a new setup, one of my thoughts was, "Oh, cool, maybe I can propose that they just move their production service to Netlify!". But no. As best I can tell (and recall), the full Metamath website blows out all the limits that Netlify places on numbers of files and probably total size. Metamath.org is a humungous website by most standards.  You know, all those thousands and thousands and thousands of theorems, plus lots of other stuff. ;-) I don't see any option out there that would serve your needs as well as a virtual private server, or perhaps two or three of them.

I have watched how both Norm and David have approached system management, and like I said before, I saw no no problems at all with David's (or Norm's) judgment. FWIW, the three of us discussed server setup off-list and did some experiments with system and web server configuration, e.g. moving to nginx as the web server.

Maybe I haven't said it, but I have lots and lots of experience with Linux, with a few years of complete responsibility for mission-critical public-facing 24/7 systems. My last industrial job became working on tools for data center monitoring at Google.  It was _not_ a security job, but we were constantly exposed to the workings of Google data centers and it seemed like we interacted with site reliability engineers almost every day. Google uses Linux for everything from desktops to data center servers.

What I have seen of ServerPilot does not excite me, meaning to say I doubt it would wind up improving or simplifying your operations. But others might view it differently. My main advice would be to support the people (David, eh?) taking responsibility, while encouraging them to document their system management practices, which is also of very real importance.

Best regards,

Cris

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJJTU5oT_FrBty4JhSD5%3D4bEi%3D8buV2dz9Vof6TyNBCYx2WjEA%40mail.gmail.com.