On Sat, Feb 18, 2023 at 5:16 PM David A. Wheeler <dwhee...@dwheeler.com> wrote:
> > > > On Feb 18, 2023, at 4:08 PM, Mario Carneiro <di.g...@gmail.com> wrote: > > In case it wasn't clear (and it probably wasn't), in a future world in > which the default mechanism is some super fancy client side renderer it is > still possible to offer a fallback "static site" of HTML pages which is > nevertheless not generated in advance and is being served dynamically > server-side. This has a relatively small generation cost even if we don't > stick a CDN in front of it, but if we do then I think that's a viable > approach to having all the HTML pages with basically zero preprocessing, > just a smarter server. I would really love it if the only thing the site > build needs to do is download and load the latest set.mm . > > I understand, that's just a typical dynamically-generated data file and/or > HTML with possibly front-end JavaScript. Bog standard stuff. Of course, > there are pluses & minuses with that approach. In the 2010s almost everyone > switched to that model, today there's a big press back to > statically-regenerated sites where practical (with Jekyll, etc.) because > attackers routinely pop systems that do dynamic response. > > There are big concerns if you hook up a program written in C to input sent > by an attacker. Rigorous input filtering would definitely help, but using > something like metamath-knife as a basis instead of metamath-exe might be > better. So doing this would involve a nontrivial amount of software, > *along* with analysis to ensure that it was unlikely to lead to a > vulnerability. Statically generating files is a much simpler path from > where we are. That's not to say we must go that way, but it'd take more > effort to do full dynamic generation *with* confidence in its security. > While yes I agree that this would be much better done with metamath-knife than metamath-exe, I don't think there is a major concern here, or at least we can mostly mitigate the issues since this flow is extremely light on input from the attacker. Basically the only thing you can specify is the theorem you want to see. But for sure I'm not interested in doing this by building on metamath-exe, there are some great frameworks for writing these kind of servers in rust that should already handle most of the issues. The main thing to be concerned about is DOS attacks, and having a 'real' server like nginx in front helps with that. But our threat model is pretty much nonexistent to begin with; almost all the server data and code is public domain in the first place and even if the server is taken down it's not a critical service. I think a much more critical problem for the project is giving a perception of being an old unfriendly software used by few. > I don't think this is a very competitive option though, since you would > have to load all of set.mm. > > It's more competitive than you might think. Igor's prover loads the whole > database in a few seconds. I was talking about the data cost. Even if you have a highly optimized mm verifier, you can't get around the fact that you need to send some 30 MB over the wire before you can do anything. That's big even by modern bloated web page standards. If the user doesn't have a great connection then that might dwarf the cost of processing. -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvKVCOmYtuGjvK8WRA8nO5GxGbc1R-QNfAedYmsUzU2Qg%40mail.gmail.com.
