lean4web
lean4web copied to clipboard
Potential Bug: Unintended File Access via `/api` Endpoints
Using any of the /api endpoints of the Express server, it is possible to access nearly all files within the project's directory. Below are some examples:
- https://live.lean-lang.org/api/examples/mathlib-demo/build.sh
- https://live.lean-lang.org/api/examples/mathlib-demo/.lake/packages/mathlib/README.md
- https://live.lean-lang.org/api/examples/mathlib-demo/.lake/packages/mathlib/.github/workflows/daily.yml
- https://live.lean-lang.org/api/examples/mathlib-demo/.lake/packages/mathlib/Mathlib/Logic/Basic.lean
While I do not believe this presents a security risk, it seems unlikely that this behavior was intended. Would appreciate any clarification on whether this is expected or if further restrictions should be applied.
I believe we do need to access any Lean files of the project (for the examples) and the lake-manifest.json. I wouldn't mind restricting the access point beyond the files which are actually needed!