Sounds like really nice progress David, very impressive, hope the covid is light and passes off quickly for you :)
As a tiny thing I noticed on the front page it it says "Constructs mathematics from scratch, starting from ZFC set theory axioms. Over 23,000 proofs." Whereas maybe there are about 43k proofs now? On Sunday, July 24, 2022 at 11:59:24 PM UTC+1 David A. Wheeler wrote: > All: > > I've made some improvements to the us.metamath.org website infrastructure. > Details, including upcoming plans, are below. Comments welcome! > > --- David A. Wheeler > > ==================== > > The most obvious change is that while you can continue to use the old > "http:" > URLs, all such requests are immediately upgraded to secure "https:" > requests. > Once you're using http requests, all relative requests continue to use > https. > The TLS (security) certificates used by https are provided > by Let's Encrypt, and they are automatically updated. > > I've made some other improvements (mostly to security); all should be > invisible: > * We now use Debian 11 not Debian 10 (this upgrade improved security & > performance somewhat) > * The system now *automatically* downloads & installs security updates, so > any vulnerabilities > publicly found will be quickly addressed without waiting for me or anyone > else. > * We now have a simple intrusion prevention system enabled (fail2ban - > it's primarily there > to counter simplistic mass attacks). > * I've enabled a basic firewall to make life slightly harder on attackers > by ensuring that > only specific identified services are visible. > * I've slightly hardened the kernel configuration against attack > (e.g., by enabling source address verification & ignoring source routing) > * I've slightly hardened the web server (nginx) against attack > (e.g., by only allowing the HTTP requests GET, HEAD, and OPTIONS). > > There's always some additional security hardening you can do, but I'm > hoping that > these steps will be adequate to keep the site relatively secure. > > I've made a larger but subtler change by switching to an "Infrastructure > as Code" approach. > That is, the *entire* server is defined by a set of scripts here: > https://github.com/metamath/metamath-website-scripts > We can at any time destroy the current virtual server & recreate it > automatically > with those scripts. This eliminates the "I wonder how this server is > configured" mystery, > and more importantly, it means we can always rebuild the server from > scratch whenever we want > (making the server like cattle instead of like a pet). Anyone can review > those scripts and > propose improvements, which if accepted will improve the system. > > Currently us.metamath.org is just the web server. I plan to eventually > *also* make it > the system that regenerates the website, 1/day. That is taking longer to > implement. > For one, I got COVID-19 this week, so I've been asleep most of this week > instead of > being useful :-(. Another is that Norm set up us2.metamath.org the way he > wanted over > a long period of time, so it's taking me quite some time to figure out how > to redo it. > He assumed that storage space was unlimited, but while we *can* get lots > of storage, it > costs more money; I would rather not keep unused extra copies that would > cost more money. > The cheapest linode plan has enough space for the website & 1 copy being > generated, not several. > The scripts were also just very complicated, which I think made sense to > him > because he built it over time. However, since we're transitioning to a > different > system anyway, I want to have a much less complicated system that we can > maintain it into the future. > I think the result will be much simpler & cleaner, but it's taking me a > while to figure out > what Norm's scripts did so I can extract just the parts we need. > > Once the us.metamath.org site can regenerate the webpages, we can have > the other mirrors sync > from *that* system instead (us instead of us2). > I think it'd be good to continue to support mirrors, we've > been doing it for a long time & I see no reason to stop. > However, I think the mirrors should be copying from a site that is *not* > depending on anyone's basement :-). > I'm not sure how that sync'ing should take place. Currently it uses rsync, > which isn't secured; > we *could* continue to support that but I think it's a lousy idea today. > The easy answer would be rsync+ssh, which would be fine and works basically > identically to rsync except it adds encryption. If someone wants an > alternative > approach, we could probably support alternatives. That said, first we need > to generate data worth synchronizing :-). -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fc16b33d-e226-4e6e-99ef-db668f4db491n%40googlegroups.com.
