diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-04 14:50:52 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-04 15:27:16 -0400 |
commit | 1364389f19e55984cc52589b3af42322c300e00f (patch) | |
tree | ac33b345bfe9877698a5c1344c589ef3feeb2713 /src/parser/options | |
parent | 00d068f91c675edbe63c2f8c1dae283f300dd4cc (diff) |
For security, add --no-filesystem-access option, which disables SMT-LIB script access to filesystem.
Diffstat (limited to 'src/parser/options')
-rw-r--r-- | src/parser/options | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/parser/options b/src/parser/options index f277b231d..c80914596 100644 --- a/src/parser/options +++ b/src/parser/options @@ -14,8 +14,18 @@ option memoryMap --mmap bool option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking disable ALL semantic checks, including type checks -# this is just to support security in the online version +# this is to support security in the online version, and in other similar contexts # (--no-include-file disables filesystem access in TPTP and SMT2 parsers) -undocumented-option canIncludeFile /--no-include-file bool :default true +# the name --no-include-file is legacy: it also now limits any filesystem access +# (read or write) for example by using --dump-to (or the equivalent set-option) or +# set-option :regular-output-channel/:diagnostic-output-channel. However, the main +# driver is still permitted to read the input file given on the command-line if any. +# creation/use of temp files are still permitted (but the paths aren't given by the +# user). Also note this is only safe for the version invoked through the main driver, +# there are ways via the API to get the CVC4 library to open a file for reading or +# writing and thus leak information from an existing file, or overwrite an existing +# file with malicious content. +undocumented-option filesystemAccess /--no-filesystem-access bool :default true +undocumented-alias --no-include-file = --no-filesystem-access endmodule |