Stream: Coq devs & plugin devs

Topic: envvar for micromega cache


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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,

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:37):

I don't know

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:42):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 14 2022 at 13:33):

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

view this post on Zulip Ali Caglayan (Apr 14 2022 at 13:34):

And if csdp is installed then all of them will.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 13:39):

simple is nice

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 13:39):

KISA :)

view this post on Zulip Ali Caglayan (Apr 14 2022 at 13:41):

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

view this post on Zulip 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))))

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 14 2022 at 13:48):

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

view this post on Zulip Ali Caglayan (Apr 14 2022 at 13:48):

There are various bugs/ output/ etc also using it

view this post on Zulip Ali Caglayan (Apr 14 2022 at 13:48):

Or at least they were before

view this post on Zulip 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

view this post on Zulip 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,

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 14:26):

and see what hits we get

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 14:32):

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 14:33):

and will make sandboxed rules fail

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 14:33):

in fact, it is not sound, right?

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 14:33):

don't we have a race condition looming here?

view this post on Zulip Ali Caglayan (Apr 14 2022 at 14:36):

Currently there are no guarantees.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 14:37):

Ah ok I missed that

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 14:37):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 14 2022 at 15:10):

Yes would maybe be nice to allow a read only cache


Last updated: Feb 05 2023 at 23:30 UTC