From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 4 Apr 2014 18:50:52 +0000 (-0400)
Subject: For security, add --no-filesystem-access option, which disables SMT-LIB script access... 
X-Git-Tag: cvc5-1.0.0~6983
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1364389f19e55984cc52589b3af42322c300e00f;p=cvc5.git

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

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
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index cb8c0d4f6..7d0a0c4b9 100644
--- 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 49f2c7943..058a00f32 100644
--- 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);