For security, add --no-filesystem-access option, which disables SMT-LIB script access...

diff --git a/src/parser/options b/src/parser/options
index f277b231dcbb8e55ff36dac471b1181c805e5066..c80914596c05d15aa7093b74d71bb52389e8d0fe 100644 (file)
--- 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

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index cb8c0d4f602d51008badeb0f4d200bd6c360a240..7d0a0c4b9bf4a120b0e8244cb0147481f7b4ff25 100644 (file)
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -154,7 +154,7 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) {
       .withChecks(options[options::semanticChecks])
       .withStrictMode(options[options::strictParsing])
       .withParseOnly(options[options::parseOnly])
-      .withIncludeFile(options[options::canIncludeFile]);
+      .withIncludeFile(options[options::filesystemAccess]);
   }
 
 ParserBuilder& ParserBuilder::withStrictMode(bool flag) {

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 49f2c79432f1ee3458b4345721dcdc20589d8f6e..058a00f32ebc89f984915b6cddb7ed9d7160d546 100644 (file)
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -334,6 +334,8 @@ inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) {
     throw OptionException(std::string("Bad file name for --dump-to"));
   } else if(optarg == "-") {
     outStream = &DumpOutC::dump_cout;
+  } else if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
   } else {
     errno = 0;
     outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
@@ -357,6 +359,8 @@ inline void setRegularOutputChannel(std::string option, std::string optarg, SmtE
     outStream = &std::cout;
   } else if(optarg == "stderr") {
     outStream = &std::cerr;
+  } else if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
   } else {
     errno = 0;
     outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
@@ -377,6 +381,8 @@ inline void setDiagnosticOutputChannel(std::string option, std::string optarg, S
     outStream = &std::cout;
   } else if(optarg == "stderr") {
     outStream = &std::cerr;
+  } else if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
   } else {
     errno = 0;
     outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
@@ -415,6 +421,8 @@ inline std::ostream* checkReplayLogFilename(std::string option, std::string opta
     throw OptionException(std::string("Bad file name for --replay-log"));
   } else if(optarg == "-") {
     return &std::cout;
+  } else if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
   } else {
     errno = 0;
     std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);