Stream: Coq devs & plugin devs

Topic: envvar for micromega cache

Ali Caglayan (Apr 12 2022 at 20:32):

@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.

Ali Caglayan (Apr 12 2022 at 20:32):

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.

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:33):

@Ali Caglayan I don't know, we need to check the standard guide for env var poisoning,

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:33):

likely we need to restrict any directory traversal, the situation is clearly different after the patch

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:33):

as of today the file is fixed, after the patch, some env var could point the cache to /etc/shadow for example

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:34):

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

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:34):

it is not a big deal, my comment is just meant as a reminder

Ali Caglayan (Apr 12 2022 at 20:35):

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.

Ali Caglayan (Apr 12 2022 at 20:36):

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.

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:37):

I don't know

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:37):

As I mentioned, I prefer not to have to think about this, but find and apply the standard security practice in these scenarios

Enrico Tassi (Apr 12 2022 at 20:38):

well, if you run as root any symlink is also a problem. I mean, a.vo may be a symlink to /foo no?

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:40):

Yup, root is bad, realistically all this can be used for is to trash some file in the user dir, still a bit dangerous

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:40):

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

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:41):

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

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:42):

so a) no directories allowed, b) auto-prefix

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:42):

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?

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:43):

We are talking of course about very minor security problems, but security is always better be safe than sorry

Emilio Jesús Gallego Arias (Apr 12 2022 at 20:43):

https://security.stackexchange.com/questions/163661/should-programs-check-for-symlinks-before-creating-files

Ali Caglayan (Apr 12 2022 at 20:48):

Emilio Jesús Gallego Arias said:

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

This seems more sensible to me then.

Ali Caglayan (Apr 14 2022 at 13:31):

@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.

Ali Caglayan (Apr 14 2022 at 13:31):

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.

Ali Caglayan (Apr 14 2022 at 13:33):

Most of the micromega tests will finish fine without any cache file anyway.

Ali Caglayan (Apr 14 2022 at 13:34):

And if csdp is installed then all of them will.

Ali Caglayan (Apr 14 2022 at 13:34):

So the cache file isn't a build dependency but a side effect we use to speed up build times.

Ali Caglayan (Apr 14 2022 at 13:35):

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.

Ali Caglayan (Apr 14 2022 at 13:35):

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.

Emilio Jesús Gallego Arias (Apr 14 2022 at 13:39):

If you think that's better then it is fine. Tho after a quick peek to the rule, it seemed quite messy to me

Emilio Jesús Gallego Arias (Apr 14 2022 at 13:39):

simple is nice

Emilio Jesús Gallego Arias (Apr 14 2022 at 13:39):

KISA :)

Ali Caglayan (Apr 14 2022 at 13:41):

Hmm the last rebase I did went a bit wrong (fixed now)

Ali Caglayan (Apr 14 2022 at 13:46):

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))))

Ali Caglayan (Apr 14 2022 at 13:47):

In theory, we could remove the cache completely and make everybody running the test-suite use csdp to run these tests

Ali Caglayan (Apr 14 2022 at 13:47):

But that seems dumb if we have a cache that avoids that. Also running those tests without cache takes forever.

Ali Caglayan (Apr 14 2022 at 13:48):

Another thing I noticed is that it is not only the micromega tests using this cache

Ali Caglayan (Apr 14 2022 at 13:48):

There are various bugs/ output/ etc also using it

Ali Caglayan (Apr 14 2022 at 13:48):

Or at least they were before

Ali Caglayan (Apr 14 2022 at 13:49):

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

Ali Caglayan (Apr 14 2022 at 13:53):

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,

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:26):

Seems like an interesting experiment to perform is to have a mode where the cache is always associated to a .v file

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:26):

and see what hits we get

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:32):

for now we can survive with that rule but it is hacky

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:33):

and will make sandboxed rules fail

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:33):

in fact, it is not sound, right?

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:33):

what guarantees that the rule has to be run before the bertot.v rule for example?

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:33):

don't we have a race condition looming here?

Ali Caglayan (Apr 14 2022 at 14:36):

Currently there are no guarantees.

Ali Caglayan (Apr 14 2022 at 14:36):

But as I said above, we can use an alias for the cache copy and then depend on that alias

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:37):

Ah ok I missed that

Emilio Jesús Gallego Arias (Apr 14 2022 at 14:37):

https://martinfowler.com/bliki/TwoHardThings.html

Ali Caglayan (Apr 14 2022 at 14:50):

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?

Ali Caglayan (Apr 14 2022 at 14:51):

I am guessing it attempts to write something and when it fails acts like no cache exists.

Emilio Jesús Gallego Arias (Apr 14 2022 at 15:10):

Yes would maybe be nice to allow a read only cache

Last updated: Jun 04 2023 at 19:30 UTC