lean4web icon indicating copy to clipboard operation
lean4web copied to clipboard

Potential Bug: Unintended File Access via `/api` Endpoints

Open tautastic opened this issue 11 months ago • 1 comments

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.

tautastic avatar Mar 08 '25 10:03 tautastic

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!

joneugster avatar Mar 08 '25 10:03 joneugster