8 files changed, 54 insertions, 3 deletions
diff --git a/src/parser/options b/src/parser/options
index b3e69a992..e16f963f4 100644
--- a/src/parser/options
+++ b/src/parser/options
@@ -17,4 +17,8 @@ option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT
 option szsCompliant --szs-compliant bool :default false
  temporary support for szs ontolotogy, print if conjecture is found
 
+# this is just to support security in the online version
+# (--no-include-file disables filesystem access in TPTP and SMT2 parsers)
+undocumented-option canIncludeFile /--no-include-file bool :default true
+
 endmodule
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 370bdfcf0..fa2a1e744 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -47,7 +47,8 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
   d_done(false),
   d_checksEnabled(true),
   d_strictMode(strictMode),
-  d_parseOnly(parseOnly) {
+  d_parseOnly(parseOnly),
+  d_canIncludeFile(true) {
   d_input->setParser(*this);
 }
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 4f943a0b5..b4e79b427 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -158,6 +158,12 @@ class CVC4_PUBLIC Parser {
   /** Are we only parsing? */
   bool d_parseOnly;
 
+  /**
+   * Can we include files?  (Set to false for security purposes in
+   * e.g. the online version.)
+   */
+  bool d_canIncludeFile;
+
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
@@ -252,6 +258,10 @@ public:
 
   bool strictModeEnabled() { return d_strictMode; }
 
+  bool allowIncludeFile() { d_canIncludeFile = true; }
+  bool disallowIncludeFile() { d_canIncludeFile = false; }
+  bool canIncludeFile() const { return d_canIncludeFile; }
+
   /**
    * Returns a variable, given a name.
    *
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index e1e4053ac..684a495b6 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -54,6 +54,7 @@ void ParserBuilder::init(ExprManager* exprManager,
   d_exprManager = exprManager;
   d_checksEnabled = true;
   d_strictMode = false;
+  d_canIncludeFile = true;
   d_mmap = false;
   d_parseOnly = false;
 }
@@ -106,6 +107,12 @@ Parser* ParserBuilder::build()
     parser->disableChecks();
   }
 
+  if( d_canIncludeFile ) {
+    parser->allowIncludeFile();
+  } else {
+    parser->disallowIncludeFile();
+  }
+
   return parser;
 }
 
@@ -151,7 +158,8 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) {
       .withMmap(options[options::memoryMap])
       .withChecks(options[options::semanticChecks])
       .withStrictMode(options[options::strictParsing])
-      .withParseOnly(options[options::parseOnly]);
+      .withParseOnly(options[options::parseOnly])
+      .withIncludeFile(options[options::canIncludeFile]);
   }
 
 ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
@@ -159,6 +167,11 @@ ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
   return *this;
 }
 
+ParserBuilder& ParserBuilder::withIncludeFile(bool flag) {
+  d_canIncludeFile = flag;
+  return *this;
+}
+
 ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) {
   d_inputType = STREAM_INPUT;
   d_streamInput = &input;
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 607547beb..9779bf37b 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -71,6 +71,9 @@ class CVC4_PUBLIC ParserBuilder {
   /** Should we parse in strict mode? */
   bool d_strictMode;
 
+  /** Should we allow include-file commands? */
+  bool d_canIncludeFile;
+
   /** Should we memory-map a file input? */
   bool d_mmap;
 
@@ -149,6 +152,13 @@ public:
    */
   ParserBuilder& withStrictMode(bool flag = true);
 
+  /**
+   * Should the include-file commands be enabled?
+   *
+   * (Default: yes)
+   */
+  ParserBuilder& withIncludeFile(bool flag = true);
+
   /** Set the parser to use the given stream for its input. */
   ParserBuilder& withStreamInput(std::istream& input);
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 29bc8d40f..5abaa0163 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -197,7 +197,10 @@ parseCommand returns [CVC4::Command* cmd = NULL]
      * the RPAREN_TOK is properly eaten and we are in a good state to read
      * the included file's tokens. */
   | LPAREN_TOK INCLUDE_TOK str[name] RPAREN_TOK
-    { if(PARSER_STATE->strictModeEnabled()) {
+    { if(!PARSER_STATE->canIncludeFile()) {
+        PARSER_STATE->parseError("include-file feature was disabled for this run.");
+      }
+      if(PARSER_STATE->strictModeEnabled()) {
         PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
       }
       PARSER_STATE->includeFile(name);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index be4907e8e..42324fe1e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -242,6 +242,11 @@ static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 }
 
 void Smt2::includeFile(const std::string& filename) {
+  // security for online version
+  if(!canIncludeFile()) {
+    parseError("include-file feature was disabled for this run.");
+  }
+
   // Get the lexer
   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index ab4ea14c4..93c2168b1 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -128,6 +128,11 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){
 
 
 void Tptp::includeFile(std::string fileName){
+  // security for online version
+  if(!canIncludeFile()) {
+    parseError("include-file feature was disabled for this run.");
+  }
+
   // Get the lexer
   AntlrInput * ai = static_cast<AntlrInput *>(getInput());
   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();