Redirect/Extraction should validate file names to avoid (over)writing to arbitrary files

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4953
From: @andres-erbsen
Reported version: 8.5
CC: @cpitclaudel, @gares, @ichung, @gares

[coqbot]

Comment author: @andres-erbsen

Created attachment 741
proof-of-concept example of how Redirect can be abused

Stepping through (or compiling) a .v file should not execute arbitrary code. To maintain this invariant, stepping through a .v file should not write arbitrary files -- all mainstream operating systems have user-writable files (and sometimes entire directories) from which code is routinely executed.

Redirect "file" VernacCommand. violates that rule, and should be fixed. Perhaps it should only allow writing files in the directory of the .v file, and require that the name of the file being written starts with the name of the .v file.

All enforced restrictions should hold even when dealing with strings that contain \0 bytes. The attached example abuses the mishandling of \0 bytes to write a file without the ".out" extension. However, just fixing the \0-byte handling is not sufficient -- for example, it is totally reasonable for a user to have a ~/.bashrc that executes all files in ~/.bashrc.d.

Attached file: redirect_bashrc.v (text/x-verilog, 129 bytes)
Description: proof-of-concept example of how Redirect can be abused

[coqbot]

Comment author: @ichung

Other vernacular commands can also cause files to be written to bad locations.

The command [Print Universes "file".] can clobber any user-writable file with a graph of the current universe constraints.

The command [Extraction "file" term.] can also clobber any user-writable file ending in .ml, .mli, .hs, .scm, or (using the \0 byte bug) any file; the contents are limited by what the extraction engine can be made to produce.

Either the [Cd] command (as in Andres' proof-of-concept) or absolute paths can cause these commands (and [Redirect]) to write to files in arbitrary directories.

[coqbot]

Comment author: @JasonGross

CC'ing Clément and Enrico, who committed and pushed the commit for [Redirect]

[coqbot]

Comment author: @cpitclaudel

The "\0" part is indeed a concern. Maybe I should have considered this when I proposed this feature. Hat tip for finding it.

stepping through a .v file should not write arbitrary files

Indeed, it shouldn't: that's why the ".out" part was originally added.

all mainstream operating systems have user-writable files (and sometimes entire directories) from which code is routinely executed.

I'll believe you on this one :) But do you have a concrete example? I was under the impression that GNU/Linux required the executable bit to be set, and that MS Windows required one of a few specific extensions.

for example, it is totally reasonable for a user to have a ~/.bashrc that executes all files in ~/.bashrc.d

Is it really? It doesn't sound too reasonable to execute arbitrary data files :/ Executing all the executable ones is a pretty common pattern, though. But we never produce executable files, do we?

I'd be fine with Redirect always writing to, say, /tmp (or the platform-local equivalent). I'm also fine with putting more constraints on the file name (though since company-coq uses these for temporary data, that won't be the most pleasant). We could also force the file to be new.

[coqbot]

Comment author: @gares

Hum, I'm quite unsure coqc/coqtop do (or even should) provide the kind of service you suppose they offer. Getting a syntactically valid .v file from the net and compiling it is not safe, as downloading a, say, .pl file and running it trough the perl interpreter. Or downloading a .tgz, unpacking it, and running ./configure && make.

I guess these functionalities could be made more robust to unintentional errors (i.e. overwriting exiting files). But making these things "unexploitable" is a different story, and coqc declares no such guarantee.

coqchk offers a service closer to what you have in mind: take
a potentially evil .vo file and (re)check the proofs it contains. coqchk
writes no files, and validates the binary format of .vo files... Still it can saturate your memory...

So I can hardly see how this (class of) bugs can be considered critical to coqc/coqtop.

[coqbot]

Comment author: @andres-erbsen

Hmm. It is indeed a question what guarantees coqc and coqide should provide regardless of the content of the file being processed. When filing this bug, I classified them similarly to gcc and emacs, both of which take care to maintain controlled behavior even in case of malicious input files (e.g. https://www.gnu.org/software/emacs/manual/html_node/elisp/File-Local-Variables.html). The existence of "Redirect" and extraction to file indeed places the coq tools somewhat towards the world of scripting languages (as in the perl analogy). It is not intuitive or obvious, though -- the documentation describes coqtop as a compiler, and the backward-forward user interface of coqide definitely hints at reversibility.

Another program that exists in this gray area is tex. It is not even a that bad comparison -- one of the primary intended uses of both coqide and tex is describing mathematical constructions. According to https://tex.stackexchange.com/questions/262625/security-latex-injection-hack, "By default latex can not execute system code or write files beginning . or write out of the current directory, so the security risks are minimal.". I think adding a similar restriction to coq would not limit the usefulness of the vernac commands in question (just use a real scripting language to move the output into the right place later), but would reduce the risk from bad .v files significantly. Perhaps placing all files written from a.v into the directory a.v.out would make more sense than putting them in the current directory, though.