@Emilio Jesús Gallego Arias, regarding https://github.com/coq/coq/pull/15918 I don't particularly think specifying the cache file with env vars is any more vulnerable than opening a specific file as done today.
Of course, I am not a security expert, but it seems to me to be doing the same thing. Granted, there are performance issues in that PR currently, but that is orthogonal to the security concerns.
@Ali Caglayan I don't know, we need to check the standard guide for env var poisoning,
likely we need to restrict any directory traversal, the situation is clearly different after the patch
as of today the file is fixed, after the patch, some env var could point the cache to /etc/shadow
for example
I think that forbidding any slash in the name should work, but we need to google the guide, it is not a good idea to create our own security practices
it is not a big deal, my comment is just meant as a reminder
Emilio Jesús Gallego Arias said:
as of today the file is fixed, after the patch, some env var could point the cache to
/etc/shadow
for example
Wouldn't this require somebody giving root permissions to coq/micromega? That already seems like something damaging to any program with file access.
Emilio Jesús Gallego Arias said:
I think that forbidding any slash in the name should work, but we need to google the guide, it is not a good idea to create our own security practices
This seems fragile and wrong to me. We might genuinely need a slash in the name, not to mention Windows users may use backslashes.
I don't know
As I mentioned, I prefer not to have to think about this, but find and apply the standard security practice in these scenarios
well, if you run as root any symlink is also a problem. I mean, a.vo may be a symlink to /foo no?
Yup, root is bad, realistically all this can be used for is to trash some file in the user dir, still a bit dangerous
I did a review on some info I found online, so indeed, ensuring only the filename + auto prefix is taken into account after env var sanitization seems ok to me
auto prefix I mean that if we pass MICROMEGA_CACHE_FILE=foo
then Coq will read from foo.cache
and write to foo.cache.new
so a) no directories allowed, b) auto-prefix
Enrico Tassi said:
well, if you run as root any symlink is also a problem. I mean, a.vo may be a symlink to /foo no?
good point! I don't now if that a security problem, likely is, and Coq should check that output file is not a symlink before writing to it, what do other compilers do?
We are talking of course about very minor security problems, but security is always better be safe than sorry
Emilio Jesús Gallego Arias said:
auto prefix I mean that if we pass
MICROMEGA_CACHE_FILE=foo
then Coq will read fromfoo.cache
and write tofoo.cache.new
This seems more sensible to me then.
@Emilio Jesús Gallego Arias The reason I have now decided not to go down this route is because the cache does work as long as we don't list it as a dependency for any rules.
We can implicitly add a dependency by making a special alias for the rule that copies the cache, and then rely on that alias when building the rules.
Most of the micromega tests will finish fine without any cache file anyway.
And if csdp is installed then all of them will.
So the cache file isn't a build dependency but a side effect we use to speed up build times.
In the future, we can design a caching system that works better with pure build rules, but for now I am following the advice of not changing things too much.
The goal of the test-suite PR is to get the test-suite in a usable state w.r.t to dune. We will not perfectly turn it into a pure build system first try.
If you think that's better then it is fine. Tho after a quick peek to the rule, it seemed quite messy to me
simple is nice
KISA :)
Hmm the last rebase I did went a bit wrong (fixed now)
This is the rule:
(rule
(alias runtest)
; The universe dep ensures we always run this rule
(deps (universe) .csdp.cache.test-suite)
(action (progn
; It is important we don't add .csdp.cache as a target or else dune will scrub
; its write permissions
(no-infer (copy .csdp.cache.test-suite .csdp.cache))
(run chmod +w .csdp.cache))))
In theory, we could remove the cache completely and make everybody running the test-suite use csdp to run these tests
But that seems dumb if we have a cache that avoids that. Also running those tests without cache takes forever.
Another thing I noticed is that it is not only the micromega tests using this cache
There are various bugs/ output/ etc also using it
Or at least they were before
So if we want other files to have access to this cache, we should keep .csdp.test-suite as a master copy somewhere and plop this rule into each test directory that needs it
We also observed that generating the cache from scratch is nowhere near as large as it currently is. I have no idea how the micromega maintainers were generating this cache before. So I will not touch it too much. That includes adding those env vars,
Seems like an interesting experiment to perform is to have a mode where the cache is always associated to a .v file
and see what hits we get
for now we can survive with that rule but it is hacky
and will make sandboxed rules fail
in fact, it is not sound, right?
what guarantees that the rule has to be run before the bertot.v rule for example?
don't we have a race condition looming here?
Currently there are no guarantees.
But as I said above, we can use an alias for the cache copy and then depend on that alias
Ah ok I missed that
https://martinfowler.com/bliki/TwoHardThings.html
Another thing that puzzled me however is that the cache doesn't work when it is readonly. If we are not writing anything to the cache, why does micromega fall back on csdp?
I am guessing it attempts to write something and when it fails acts like no cache exists.
Yes would maybe be nice to allow a read only cache
Last updated: Nov 29 2023 at 18:01 UTC