Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Safe(er) evalulation of Lisp code in agda-mode #6537

Open
wants to merge 45 commits into
base: master
Choose a base branch
from

Conversation

phikal
Copy link
Contributor

@phikal phikal commented Mar 16, 2023

Based on #6536, these changes address address an old comment:

;; Note that the following function is a security risk, since it
;; evaluates code without first inspecting it. The code (supposedly)
;; comes from the Agda backend, but there could be bugs in the backend
;; which can be exploited by an attacker which manages to trick

Instead of just directly passing Lisp code to Emacs to evaluate, a few simple checks are made to ensure the commands are of the expected data types (I hope I am forgiven for using Common Lisp types here). Furthermore, the arguments are not evaluated, and instead just passed to functions that we just "checked" are safe.

New commands that Agda can invoke now have to be tagged with a declare statement:

 (defun agda2-status-action (status)
   "Display the string STATUS in the current buffer's mode line.
 \(precondition: the current buffer has to use the Agda mode as the
 major mode)."
+  (declare (agda2-command string))
   (setq agda2-buffer-external-status status)

@phikal
Copy link
Contributor Author

phikal commented Mar 16, 2023

The background for these changes can be found in PR #6123 and was proposed in #5917.

@jespercockx
Copy link
Member

According to #6123 (comment), this should only be merged AFTER #6536

@plt-amy plt-amy modified the milestones: 2.6.4, 2.6.5, 2.6.4.1 Jul 21, 2023
@andreasabel andreasabel modified the milestones: 2.6.4.1, 2.6.5 Nov 30, 2023
@phikal phikal force-pushed the safe-eval branch 2 times, most recently from df21bf5 to 9d49cba Compare February 20, 2024 17:07
* agda2-mode.el (agda2-infer-type-maybe-toplevel): Sharp-quote 'agda2-infer-type'.
(agda2-solveAll-action): Sharp-quite 'agda2-solve-action'.
(agda2-compute-normalised-maybe-toplevel): Sharp quote
'agda2-compute-normalised' and 'agda2-compute-normalised-toplevel'.

Sharp-quoting functions indicates that a symbol should have a bound
function slot, and that the byte compiler should check if this is the
case, otherwise emit a warning.
It is not necessary to use 'eval' to invoke a function with an
argument list of unknown length.
This change builds on c7492c0,
dropping the need for any queue (of string or a buffer), by inserting
the process output directly into the process buffer and operating on
thereon.  We avoid the overhead of consing lists and strings, while
simplifying the logic by relying more on Lisp primitives.
Since the process output can be chunked inconveniently (e.g. breaking
mid-line), we need to make sure that we can recognise and handle these
situations.  This includes making sure we don't mis-`read' part of a
command, then run into a type error later on, but also restoring the
previous state, so that we can hope to correctly parse the data upon
receiving the next output chunk.
Since this is a buffer local variable, we need to make sure that we
are manipulating and accessing it in the right buffer.
By using 'forward-line' it was possible for some commands to not get
parsed properly, leaving 'agda2-mode' in an inconsistent state.
@jespercockx
Copy link
Member

This is currently unreviewable due to the large number of commits. Also, the test suite seems to be failing.

@jespercockx jespercockx modified the milestones: 2.7.0, icebox, later Jul 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants