---------- Forwarded message ---------
Von: Marc Nieper-Wißkirchen <xxxxxx@nieper-wisskirchen.de>
Date: Mi., 3. Juli 2019 um 15:53 Uhr
Subject: Re: Undefined behavior
To: John Cowan <xxxxxx@ccil.org>


Am Mi., 3. Juli 2019 um 14:43 Uhr schrieb John Cowan <xxxxxx@ccil.org>:


On Wed, Jul 3, 2019 at 1:50 AM Marc Nieper-Wißkirchen <xxxxxx@nieper-wisskirchen.de> wrote:

I think one has to be a bit more careful: Various procedures included in the SRFI 172 libraries can trigger the "it is an error" condition when, say, being passed incompatible values. Evaluating Scheme code that "it is an error" is no more safe than C code that causes "undefined behavior", which means it is not all safe:

While this comparison is correct in principle, it is mostly not true in practice.  I know of no Scheme compiler whatever that generates unsafe code *by default*, whereas C compilers almost always do.  Indeed, the only currently working C compiler I know that does generate safe code is Vacietis <https://github.com/vsedach/Vacietis>, which compiles C into Common Lisp.  Of course, the resulting code must not itself be compiled unsafely, but Common Lisp has the same culture of safety-by-default as Scheme.  I will mention the question of "is an error" in the next draft, however.

My point is the following: If we advertise SRFI 172 as a safe way to use `eval' with user supplied expressions, we should not ship something, which we call a portable implementation.

And even if every Scheme implementation known is safe "by default", it would still be a problem for those implementations that offer an "unsafe" mode for the sake of speed. Code emulating a sandbox through SRFI 172 has no way to decide whether it is used in an environment where every "it is an error" is safe or not.

Things like "(car 1)" are easily checked, but I am wondering about more subtle things like that it is an error to invoke the continuation of an <init> in a letrec*-expression more than once. Is it clear that all Schemes behave well when running code that violates this requirement?

Regardless of what has been discussed until this point, there is another problem: R7RS-Schemes are allowed to extend the domain of the standard procedures, which can make them unsafe for the use of SRFI 172. For example, a Scheme may have mutable parameter objects like those of SRFI 39. If any parameter objects (like `current-output-port') were exposed in such an implementation, "safe" code running under SRFI 172 could influence code outside the sandbox. (Now, `current-output-port' is not exported by SRFI 172; I mentioned it because it serves as an example what can happen when the domains of R7RS-small procedures are extended and the implementation of SRFI 172 doesn't know about it.)

There are other subtle ways to escape the sandbox, for example through promises. R7RS-small promises (corrected in SRFI 155) do the evaluation in the dynamic environment where the value is needed for the first time and not in the dynamic environment, in which the promise was created. Now assume one wants to run code in a sandbox that is supposed to return a promise (e.g. a SRFI 41 stream). When the code outside the sandbox later forces the promise, code originally coming from the sandbox suddenly sees the environment outside the sandbox:

(define (hopefully-safe-eval expr) (parameterize ((current-output-port (open-output-string))) (eval expr (environment '(srfi 172)))))
(force (hopefully-safe-eval '(delay (begin (display "I am evil!") (newline) 'evil))))

What we see is that while forcing a promise returned from the sandbox should be safe (it is a purely functional thing), but it isn't.

This could be amended by exporting SRFI 155 promises instead of R7RS-small ones (probably a good idea) or by noting that returning promises is, contrary to expectations, not safe (not such a good idea). But even if it is amended in either way, how can we sure that there are no further loopholes? Malicious users are creative and implementing fool-proof sandboxes is hard. I don't believe that a simple implementation of SRFI 172 will be safe in practice, which is what should count.

Marc

bitbucket.org/cowan/r7rs-wg1-infra/src/default/ItIsAnError.md is a list of explicit "is an error" references in R7RS-small, but of course it is not exhaustive.


John Cowan          http://vrici.lojban.org/~cowan        xxxxxx@ccil.org
Some people open all the Windows; wise wives welcome the spring by moving
the Unix.  --Advertisement for Unix Book Units (U.K.)
(see https://9p.io/who/dmr/unix3image.gif)



--
Prof. Dr. Marc Nieper-Wißkirchen
 
Universität Augsburg
Institut für Mathematik
Universitätsstraße 14
86159 Augsburg
 
Tel: 0821/598-2146
Fax: 0821/598-2090
 
E-Mail: xxxxxx@math.uni-augsburg.de
Web: www.math.uni-augsburg.de/alg/mitarbeiter/mnieper/


--
Prof. Dr. Marc Nieper-Wißkirchen
 
Universität Augsburg
Institut für Mathematik
Universitätsstraße 14
86159 Augsburg
 
Tel: 0821/598-2146
Fax: 0821/598-2090
 
E-Mail: xxxxxx@math.uni-augsburg.de
Web: www.math.uni-augsburg.de/alg/mitarbeiter/mnieper/