Add proof-script-evaluate-elisp-comment-regexp security hole.

2 files changed, 31 insertions, 2 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 2bd15a77..7db11cba 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -725,6 +725,20 @@ assistant, for example, to compile a completed file."
   :type '(repeat function)
   :group 'proof-script)
 
+(defcustom proof-script-evaluate-elisp-comment-regexp "ELISP: -- \\(.*\\) --"
+  "Matches text within a comment telling Proof General to evaluate some code.
+This allows Emacs Lisp to be executed during scripting.
+\(It's also a fantastic backdoor security risk).
+
+If the regexp matches text inside a comment, there should be
+one subexpression match string, which will contain elisp code
+to be evaluated.
+
+Elisp errors will be trapped when evaluating; set
+`proof-general-debug' to be informed when this happens."
+  :type 'regexp
+  :group 'proof-script)
+
 ;;
 ;; Proof script indentation
 ;;
@@ -1395,6 +1409,7 @@ settings."
   :type '(choice nil regexp)
   :group 'proof-shell)
 
+
 (defcustom proof-shell-match-pgip-cmd nil
   "Regexp used to match PGIP command from proof assistant.
 The matching string will be parsed as XML and then processed by
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 47ddd9bb..5eaa6c2a 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1348,13 +1348,27 @@ Argument SPAN has just been processed."
 		    (+ (length comment-start) (span-start span))
 		    (- (span-end span)
 		       (max 1 (length comment-end)))))
-	(id        (proof-next-element-id 'comment)))
+	(id        (proof-next-element-id 'comment))
+	str)
     (pg-add-element "comment" id bodyspan)
     (span-set-property span 'id (intern id))
-    (span-set-property span 'idiom 'comment)))
+    (span-set-property span 'idiom 'comment)
     ;; this tries to extract last output, which is wrong for comments.
     ;; (pg-set-span-helphighlights span)
 
+    ;; possibly evaluate some arbitrary Elisp.  SECURITY RISK!
+    (save-match-data
+      (setq str (buffer-substring-no-properties (span-start span)
+						(span-end span)))
+      (if (proof-string-match-safe proof-script-evaluate-elisp-comment-regexp str)
+	  (condition-case nil
+	      (eval (car (read-from-string (match-string-no-properties 1 str))))
+	    (t (proof-debug
+		(concat
+		 "lisp error when obeying proof-shell-evaluate-elisp-comment-regexp: \n"
+		 (print1-to-string (match-string-no-properties 1))
+		 "\n"))))))))
+
 
 (defun proof-done-advancing-save (span)
   "A subroutine of `proof-done-advancing'.  Add info for save span SPAN."